{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T23:00:44Z","timestamp":1773615644573,"version":"3.50.1"},"reference-count":43,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.3103\/s0146411622070070","type":"journal-article","created":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T09:03:26Z","timestamp":1676797406000},"page":"669-687","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System"],"prefix":"10.3103","volume":"56","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9387-6735","authenticated-orcid":false,"given":"D. A.","family":"Kondratyev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2023,2,19]]},"reference":[{"key":"7523_CR1","doi-asserted-by":"publisher","first-page":"407","DOI":"10.3103\/S0146411614070141","volume":"48","author":"I.V. Maryasov","year":"2014","unstructured":"Maryasov, I.V., Nepomniaschy, V.A., Promsky, A.V., and Kondratyev, D.A., Automatic C program verification based on mixed axiomatic semantics, Autom. Control Comput. Sci., 2014, vol. 48, no. 7, pp. 407\u2013414.\u00a0https:\/\/doi.org\/10.3103\/S0146411614070141","journal-title":"Autom. Control Comput. Sci."},{"key":"7523_CR2","doi-asserted-by":"publisher","first-page":"445","DOI":"10.3103\/S0146411615070123","volume":"49","author":"D.A. Kondratyev","year":"2015","unstructured":"Kondratyev, D.A. and Promsky, A.V., Developing a self-applicable verification system. Theory and practice, Autom. Control Comput. Sci., 2015, vol. 49, no. 7, pp. 445\u2013452.\u00a0https:\/\/doi.org\/10.3103\/S0146411615070123","journal-title":"Autom. Control Comput. Sci."},{"key":"7523_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-74313-4_17","volume-title":"Implementing the symbolic method of verification in the C-light project, Perspectives of System Informatics. PSI 2017","author":"D. Kondratyev","year":"2018","unstructured":"Kondratyev, D., Implementing the symbolic method of verification in the C-light project, Perspectives of System Informatics. PSI 2017,Petrenko, A. and Voronkov, A., Eds., Lecture Notes in Computer Science, vol. 10742, Cham: Springer, 2018, pp. 227\u2013240.\u00a0https:\/\/doi.org\/10.1007\/978-3-319-74313-4_17"},{"key":"7523_CR4","doi-asserted-by":"publisher","first-page":"653","DOI":"10.3103\/S0146411619070101","volume":"53","author":"D.A. Kondratyev","year":"2019","unstructured":"Kondratyev, D.A., Maryasov, I.V., and Nepomniaschy, V.A., The automation of C program verification by the symbolic method of loop invariant elimination, Autom. Control Comput. Sci., 2019, vol. 53, no. 7, pp. 653\u2013662.\u00a0https:\/\/doi.org\/10.3103\/S0146411619070101","journal-title":"Autom. Control Comput. Sci."},{"key":"7523_CR5","doi-asserted-by":"publisher","first-page":"728","DOI":"10.3103\/S0146411620070093","volume":"54","author":"D.A. Kondratyev","year":"2020","unstructured":"Kondratyev, D.A. and Promsky, A.V., The complex approach of the C-lightVer system to the automated error localization in C-programs, Autom. Control Comput. Sci., 2020, vol. 54, no. 7, pp. 728\u2013739.\u00a0https:\/\/doi.org\/10.3103\/S0146411620070093","journal-title":"Autom. Control Comput. Sci."},{"key":"7523_CR6","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R., An axiomatic basis for computer programming, Commun. ACM, 1969, vol.\u00a012, no. 10, pp. 576\u2013580.\u00a0https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"7523_CR7","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1007\/s00165-019-00501-3","volume":"31","author":"K.R. Apt","year":"2019","unstructured":"Apt, K.R. and Olderog, E.-R., Fifty years of Hoare\u2019s logic, Formal Aspects Comput., 2019, vol. 31, no. 6, pp.\u00a0751\u2013807.\u00a0https:\/\/doi.org\/10.1007\/s00165-019-00501-3","journal-title":"Formal Aspects Comput."},{"key":"7523_CR8","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R. and Huisman, M., Deductive software verification: From pen-and-paper proofs to industrial tools, Computing and Software Science, Steffen, B. and Woeginger, G., Eds., Lecture Notes in Computer Science, vol.\u00a010000, Springer, 2019, pp. 345\u2013373.\u00a0https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"7523_CR9","doi-asserted-by":"publisher","DOI":"10.1145\/3477355.3477359","volume-title":"Assessing the success and impact of Hoare\u2019s logic, Theories of Programming: The Life and Works of Tony Hoare","author":"K.R. Apt","year":"2021","unstructured":"Apt, K.R. and Olderog, E.-R., Assessing the success and impact of Hoare\u2019s logic, Theories of Programming: The Life and Works of Tony Hoare, Jones, C.B. and Misra, J., Eds., New York: Association for Computing Machinery, 2021, pp. 41\u201376.\u00a0https:\/\/doi.org\/10.1145\/3477355.3477359"},{"key":"7523_CR10","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1023\/A:1021045909505","volume":"28","author":"V.A. Nepomniaschy","year":"2002","unstructured":"Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., and Promskii, A.V., Towards verification of C programs. C-light language and its formal semantics, Program. Comput. Software, 2002, vol. 28, no. 6, pp. 314\u2013323.https:\/\/doi.org\/10.1023\/A:1021045909505","journal-title":"Program. Comput. Software"},{"key":"7523_CR11","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1023\/B:PACS.0000004134.24714.e5","volume":"29","author":"V.A. Nepomniaschy","year":"2003","unstructured":"Nepomniaschy, V.A., Anureev, I.S., and Promskii, A.V., Towards verification of C programs: Axiomatic semantics of the C-kernel language, Program. Comput. Software, 2003, vol. 29, no. 6, pp. 338\u2013350.\u00a0https:\/\/doi.org\/10.1023\/B:PACS.0000004134.24714.e5","journal-title":"Program. Comput. Software"},{"key":"7523_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11086-005-0001-0","volume":"31","author":"V.A. Nepomniaschy","year":"2005","unstructured":"Nepomniaschy, V.A., Symbolic method of verification of definite iterations over altered data structures, Program. Comput. Software, 2005, vol. 31, no. 1, pp. 1\u20139.\u00a0https:\/\/doi.org\/10.1007\/s11086-005-0001-0","journal-title":"Program. Comput. Software"},{"key":"7523_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10843-2_30","volume-title":"Automatic construction of verification condition generators from Hoare logics, Automata, Languages, and Programming. ICALP 1981","author":"M. Moriconi","year":"1981","unstructured":"Moriconi, M. and Schwartz, R.L., Automatic construction of verification condition generators from Hoare logics, Automata, Languages, and Programming. ICALP 1981, Even,\u00a0S. and Kariv, O., Eds., Lecture Notes in Computer Science, vol. 115, Springer, 1981, pp. 363\u2013377.\u00a0https:\/\/doi.org\/10.1007\/3-540-10843-2_30"},{"key":"7523_CR14","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1007\/s00165-019-00490-3","volume":"31","author":"J.S. Moore","year":"2019","unstructured":"Moore, J.S., Milestones from the Pure Lisp theorem prover to ACL2, Formal Aspects Comput., 2019, vol. 31, no.\u00a06, pp. 699\u2013732.\u00a0https:\/\/doi.org\/10.1007\/s00165-019-00490-3","journal-title":"Formal Aspects Comput."},{"key":"7523_CR15","doi-asserted-by":"publisher","unstructured":"Kasyanov, V. and Kasyanova, E., Methods and system for cloud parallel programming, Proc. 21st Int. Conference on Enterprise Information Systems, 2019, vol. 1, pp. 623\u2013629.\u00a0https:\/\/doi.org\/10.5220\/0007750506230629","DOI":"10.5220\/0007750506230629"},{"key":"7523_CR16","doi-asserted-by":"publisher","unstructured":"Kasyanov, V.N. and Stasenko, A.P., Sisal 3.2 language structure decomposition, Proc. European Computing Conference, Mastorakis, N., Mladenov, V., and Kontargyri, V., Eds., Lecture Notes in Electrical Engineering, vol. 28, Springer, 2009, pp. 533\u2013543.\u00a0https:\/\/doi.org\/10.1007\/978-0-387-85437-3_53","DOI":"10.1007\/978-0-387-85437-3_53"},{"key":"7523_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23178-0_10","volume-title":"Sisal 3.2 Language features overview, Parallel Computing Technologies. PaCT 2011","author":"A. Stasenko","year":"2011","unstructured":"Stasenko, A., Sisal 3.2 Language features overview, Parallel Computing Technologies. PaCT 2011, Malyshkin, V., Ed., Lecture Notes in Computer Science, vol. 6873, Springer, 2011, pp.\u00a0110\u2013124.\u00a0https:\/\/doi.org\/10.1007\/978-3-642-23178-0_10"},{"key":"7523_CR18","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1080\/17517575.2012.744854","volume":"7","author":"V. Kasyanov","year":"2013","unstructured":"Kasyanov, V., Sisal 3.2: Functional language for scientific parallel programming, Enterprise Inf. Syst., 2013, vol.\u00a07, no. 2, pp. 227\u2013236.\u00a0https:\/\/doi.org\/10.1080\/17517575.2012.744854","journal-title":"Enterprise Inf. Syst."},{"key":"7523_CR19","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/0743-7315(90)90035-N","volume":"10","author":"J.T. Feo","year":"1990","unstructured":"Feo, J.T., Cann, D.C., and Oldehoeft, R.R., A report on the sisal language project, J.\u00a0Parallel Distributed Comput., 1990, vol. 10, no. 4, pp. 349\u2013366.\u00a0https:\/\/doi.org\/10.1016\/0743-7315(90)90035-N","journal-title":"J.\u00a0Parallel Distributed Comput."},{"key":"7523_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45403-9_2","volume-title":"The Sisal project: Real world functional programming, Compiler Optimizations for Scalable Parallel Systems","author":"J.-L. Gaudiot","year":"2001","unstructured":"Gaudiot, J.-L., DeBoni, T., Feo, J., B\u00f6hm, W., Najjar, W., and Miller, P., The Sisal project: Real world functional programming, Compiler Optimizations for Scalable Parallel Systems,Pande, S. and Agrawal, D.P., Eds., Lecture Notes in Computer Science, vol. 1808, Springer, 2001, pp. 45\u201372.\u00a0https:\/\/doi.org\/10.1007\/3-540-45403-9_2"},{"key":"7523_CR21","doi-asserted-by":"publisher","unstructured":"Pyzhov, K. and Idrisov, R., Back-end translator for Sisal 3.1 compiler, Bull. Novosibirsk Comput. Center, 2013, no. 35, pp. 101\u2013119.https:\/\/doi.org\/10.31144\/bncc.cs.2542-1972.2013.n35.p101-119","DOI":"10.31144\/bncc.cs.2542-1972.2013.n35.p101-119"},{"key":"7523_CR22","doi-asserted-by":"publisher","first-page":"91","DOI":"10.25743\/ICT.2020.25.5.008","volume":"25","author":"D.A. Kondratyev","year":"2020","unstructured":"Kondratyev, D.A. and Promsky, A.V., Towards verification of scientific and engineering programs. The CPPS project,Journal of Computational Technologies, 2020, vol. 25, no. 5, pp. 91\u2013106.\u00a0https:\/\/doi.org\/10.25743\/ICT.2020.25.5.008","journal-title":"Journal of Computational Technologies"},{"key":"7523_CR23","unstructured":"Dean, J. and Ghemawat, S., MapReduce: Simplified data processing on large clusters, Proc. 6th Conf. on Symp. on Operating Systems Design & Implementation, 2004, vol. 6."},{"key":"7523_CR24","doi-asserted-by":"publisher","unstructured":"Kaufmann, M. and Moore, J.S., Iteration in ACL2, Proc. Sixteenth Int. Workshop on the ACL2 Theorem Prover and Its Applications, ser. EPTCS, 2020, vol. 327, pp. 16\u201331.\u00a0https:\/\/doi.org\/10.4204\/EPTCS.327.2","DOI":"10.4204\/EPTCS.327.2"},{"key":"7523_CR25","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1007\/s10009-020-00601-z","volume":"23","author":"S. Blom","year":"2021","unstructured":"Blom, S., Darabi, S., Huisman, M., and Safari, M., Correct program parallelisations,Int. J.\u00a0Software Tools Technol. Transfer, 2021, vol. 23, no. 5, pp. 741\u2013763.\u00a0https:\/\/doi.org\/10.1007\/s10009-020-00601-z","journal-title":"Int. J.\u00a0Software Tools Technol. Transfer"},{"key":"7523_CR26","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Kiniry, J., and Warnier, M., Java program verification challenges, Formal Methods for Components and Objects, de Boer, F.S., Bonsangue, M.M., Graf, S., and de\u00a0Roever,\u00a0W.P., Eds., Lecture Notes in Computer Science, vol. 2852, Springer, 2003, pp.\u00a0202\u2013219.\u00a0https:\/\/doi.org\/10.1007\/978-3-540-39656-7_8","DOI":"10.1007\/978-3-540-39656-7_8"},{"key":"7523_CR27","doi-asserted-by":"publisher","DOI":"10.1145\/3236454.3236483","volume-title":"Reasoning about Functional Programming in Java and C++, ISSTA \u201918: Companion Proceedings for the ISSTA\/ECOOP 2018 Workshops, Amsterdam","author":"D.R. Cok","year":"2018","unstructured":"Cok, D.R., Reasoning about Functional Programming in Java and C++, ISSTA \u201918: Companion Proceedings for the ISSTA\/ECOOP 2018 Workshops, Amsterdam, 2018, New York: Association for Computing Machinery, 2018, pp. 37\u201339.\u00a0https:\/\/doi.org\/10.1145\/3236454.3236483"},{"key":"7523_CR28","series-title":"Practical methods for reasoning about Java 8\u2019s functional programming features","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03592-1_15","volume-title":"Verified Software: Theories, Tools, and Experiments. VSTTE 2018","author":"D.R. Cok","year":"2018","unstructured":"Cok, D.R. and Tasiran, S., Practical methods for reasoning about Java 8\u2019s functional programming features, in Verified Software: Theories, Tools, and Experiments. VSTTE 2018, Piskac, R. and R\u00fcmmer, P., Eds., Lecture Notes in Computer Science, vol. 11294, Springer, 2018, pp. 267\u2013278.\u00a0https:\/\/doi.org\/10.1007\/978-3-030-03592-1_15"},{"key":"7523_CR29","unstructured":"ISO\/IEC 14882:2020: Programming language C++. ISO\/IEC, 2020."},{"key":"7523_CR30","unstructured":"ISO\/IEC 9899:2011: Programming language C. ISO\/IEC, 2011."},{"key":"7523_CR31","doi-asserted-by":"publisher","unstructured":"Krebbers, R. and Wiedijk, F., A typed C11 semantics for interactive theorem proving, CPP \u201915: Proc. 2015 Conference on Certified Programs and Proofs, Mumbai, India, 2015, New York: Association for Computing Machinery, 2015, pp. 15\u201327.\u00a0https:\/\/doi.org\/10.1145\/2676724.2693571","DOI":"10.1145\/2676724.2693571"},{"key":"7523_CR32","doi-asserted-by":"publisher","unstructured":"Sammler, M., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., and Garg, D., RefinedC: automating the foundational verification of C code with refined ownership types, PLDI 2021: Proc. 42nd ACM SIGPLAN Int. Conference on Programming Language Design and Implementation, New York: Association for Computing Machinery, 2021, pp. 158\u2013174.\u00a0https:\/\/doi.org\/10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"7523_CR33","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.entcs.2009.05.052","volume":"240","author":"M.O. Myreen","year":"2009","unstructured":"Myreen, M.O. and Gordon, M.J.C., Transforming programs into recursive functions, Electron. Notes Theor. Comput. Sci., 2009, vol. 240, pp. 185\u2013200. \u00a0https:\/\/doi.org\/10.1016\/j.entcs.2009.05.052","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"7523_CR34","doi-asserted-by":"publisher","unstructured":"Blanc, R., Kuncak, V., Kneuss, E., and Suter, P., An overview of the Leon verification system: verification by translation to recursive functions, SCALA \u201913: Proc. 4th Workshop on Scala, Montpellier, France, 2013, New York: Association for Computing Machinery, 2013, p.\u00a01.\u00a0https:\/\/doi.org\/10.1145\/2489837.2489838","DOI":"10.1145\/2489837.2489838"},{"key":"7523_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_11","volume-title":"Invariant generation for multi-path loops with polynomial assignments, Verification, Model Checking, and Abstract Interpretation. VMCAI 2018","author":"A. Humenberger","year":"2018","unstructured":"Humenberger, A., Jaroschek, M., and Kov\u00e1cs, L., Invariant generation for multi-path loops with polynomial assignments, Verification, Model Checking, and Abstract Interpretation. VMCAI 2018, Dillig, I. and Palsberg, J., Eds., Lecture Notes in Computer Science, vol. 10747, Springer, 2018, pp. 226\u2013246.\u00a0https:\/\/doi.org\/10.1007\/978-3-319-73721-8_11"},{"key":"7523_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_42","volume-title":"Diffy: Inductive reasoning of array programs using difference invariants, Computer Aided Verification. CAV 2021","author":"S. Chakraborty","year":"2021","unstructured":"Chakraborty, S., Gupta, A., and Unadkat, D., Diffy: Inductive reasoning of array programs using difference invariants, Computer Aided Verification. CAV 2021, Silva, A. and Leino,\u00a0K.R.M., Eds., Lecture Notes in Computer Science, vol. 12760, Springer, 2021, pp. 911\u2013935.\u00a0https:\/\/doi.org\/10.1007\/978-3-030-81688-9_42"},{"key":"7523_CR37","unstructured":"Tuerk, T., Local reasoning about while-loops, Proc. Theory Workshop at VSTTE 2010, 2010, pp. 29\u201339."},{"key":"7523_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_6","volume-title":"Towards full proof automation in Frama-C using auto-active verification, NASA Formal Methods. NFM 2019","author":"A. Blanchard","year":"2019","unstructured":"Blanchard, A., Loulergue, F., and Kosmatov, N., Towards full proof automation in Frama-C using auto-active verification, NASA Formal Methods. NFM 2019, Badger, J. and Rozier, K., Eds., Lecture Notes in Computer Science, vol. 11460, Springer, 2019, pp. 88\u2013105.\u00a0https:\/\/doi.org\/10.1007\/978-3-030-20652-9_6"},{"key":"7523_CR39","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/3470569","volume":"64","author":"P. Baudin","year":"2021","unstructured":"Baudin, P., Bobot, F., B\u00fchler, D., Correnson, L., Kirchner, F., Kosmatov, N., Maroneze, A., Perrelle, V., Prevosto, V., Signoles, J., and Williams, N., The dogged pursuit of bug-free C programs: the Frama-C software analysis platform, Commun. ACM, 2021, vol. 64, no. 8, pp. 56\u201368.\u00a0https:\/\/doi.org\/10.1145\/3470569","journal-title":"Commun. ACM"},{"key":"7523_CR40","doi-asserted-by":"publisher","unstructured":"Attali, I., Caromel, D., and Wendelborn, A., A formal semantics and an interactive environment for Sisal, Tools and Environments for Parallel and Distributed Systems, Zaky, A. and Lewis, T., Eds., The\u00a0Springer International Series in Software Engineering, vol. 2, Boston, Springer, 1996, pp.\u00a0229\u2013256.\u00a0https:\/\/doi.org\/10.1007\/978-1-4615-4123-3_11","DOI":"10.1007\/978-1-4615-4123-3_11"},{"key":"7523_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29852-4_9","volume-title":"Proof strategy for automated Sisal program verification, Software Technology: Methods and Tools. TOOLS 2019, Mazzara, M., Bruel, JM.","author":"D. Kondratyev","year":"2019","unstructured":"Kondratyev, D. and Promsky, A., Proof strategy for automated Sisal program verification, Software Technology: Methods and Tools. TOOLS 2019, Mazzara, M., Bruel, JM., Meyer, B., and Petrenko, A., Eds., Lecture Notes in Computer Science, vol. 11771, Cham: Springer, 2019, pp.\u00a0113\u2013120.\u00a0https:\/\/doi.org\/10.1007\/978-3-030-29852-4_9"},{"key":"7523_CR42","doi-asserted-by":"publisher","unstructured":"Beckert, B., Bingmann, T., Kiefer, M., Sanders, P., Ulbrich, M., and Weigl, A., Relational equivalence proofs between imperative and MapReduce algorithms, Verified Software. Theories, Tools, and Experiments. VSTTE 2018, Piskac, R. and R\u00fcmmer, P., Eds., Lecture Notes in Computer Science, vol. 11294, Springer, 2018, pp.\u00a0248\u2013266.\u00a0https:\/\/doi.org\/10.1007\/978-3-030-03592-1_14","DOI":"10.1007\/978-3-030-03592-1_14"},{"key":"7523_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_33","volume-title":"Formally validating a practical verification condition generator, Computer Aided Verification. CAV 2021","author":"G. Parthasarathy","year":"2021","unstructured":"Parthasarathy, G., M\u00fcller, P., and Summers, A., Formally validating a practical verification condition generator, Computer Aided Verification. CAV 2021, Silva, A. and Leino, K.R.M., Eds., Lecture Notes in Computer Science, vol. 12760, Springer, 2021, pp.\u00a0704\u2013727.\u00a0https:\/\/doi.org\/10.1007\/978-3-030-81688-9_33"}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411622070070.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411622070070","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411622070070.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:02:41Z","timestamp":1773612161000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411622070070"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12]]},"references-count":43,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["7523"],"URL":"https:\/\/doi.org\/10.3103\/s0146411622070070","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12]]},"assertion":[{"value":"15 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 December 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 December 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2023","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The author declares that he has no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}