Статья: ЛОГИКА ДЛЯ СУЖДЕНИЙ ОБ ОШИБКАХ В ЦИКЛАХ НАД ПОСЛЕДОВАТЕЛЬНОСТЯМИ ДАННЫХ (IFIL) (2023)

R. H“ahnle and M. Huisman, “Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools”, in Computing and Software Science, vol. 10000, Springer, 2019, pp. 345-373.

K. R. Apt and E.-R. Olderog, “Fifty years of Hoare’s logic”, Formal Aspects of Computing, vol. 31, no. 6, pp. 751-807, 2019. EDN: UKBEZU

K. R. Apt and E.-R. Olderog, “Assessing the Success and Impact of Hoare’s Logic”, in Theories of Programming: The Life and Works of Tony Hoare, 2021, pp. 41-76.

C. A. R. Hoare, “An axiomatic basis for computer programming”, Communications of the ACM, vol. 12, no. 10, pp. 576-580, 1969.

B. M“oller, P. O’Hearn, and T. Hoare, “On Algebra of Program Correctness and Incorrectness”, in Relational and Algebraic Methods in Computer Science, vol. 13027, Springer, 2021, pp. 325-343.

Q. L. Le, A. Raad, J. Villard, J. Berdine, D. Dreyer, and P. W. O’Hearn, “Finding Real Bugs in Big Programs with Incorrectness Logic”, Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA1, pp. 1-27, 2022.

P. W. O’Hearn, “Incorrectness logic”, Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, pp. 1-32, 2019.

A. Raad, J. Berdine, H.-H. Dang, D. Dreyer, P. O’Hearn, and J. Villard, “Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic”, in Computer Aided Verification, vol. 12225, Springer, 2020, pp. 225-252.

J. Vanegue, “Adversarial Logic”, in Static Analysis, vol. 13790, Springer, 2022, pp. 422-448.

M. Milanese and F. Ranzato, "Local Completeness Logic on Kleene Algebra with Tests", in Static Analysis, vol. 13790, Springer, 2022, pp. 350-371.  

B. Bruni, R. Giacobazzi, R. Gori, and F. Ranzato, "A Correctness and Incorrectness Program Logic", Journal of the ACM, vol. 70, no. 2, pp. 1-45, 2023.  

P. Maksimovi\'c, C. Cronj"ager, A. L"o"ow, J. Sutherland, and P. Gardner, "Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding", in 37th European Conference on Object-Oriented Programming (ECOOP 2023), vol. 263, Schloss Dagstuhl - Leibniz-Zentrum f"ur Informatik, 2023, pp. 19:1-19:27.  

N. Zilberstein, D. Dreyer, and A. Silva, "Outcome Logic: A Unifying Foundation of Correctness and Incorrectness Reasoning", Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, pp. 522-550, 2023.  

T. Dardinier and P. M"uller, "Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)". 2023.  

A. Humenberger, M. Jaroschek, and L. Kov\'acs, "Invariant Generation for Multi-Path Loops with Polynomial Assignments", in Verification, Model Checking, and Abstract Interpretation, vol. 10747, Springer, 2018, pp. 226-246.  

S. Chakraborty, A. Gupta, and D. Unadkat, "Full-program induction: verifying array programs sans loop invariants", International Journal on Software Tools for Technology Transfer, vol. 24, no. 5, pp. 843-888, 2022.  EDN: WCALXU  

V. A. Nepomniaschy, "Symbolic method of verification of definite iterations over altered data structures", Programming and Computer Software, vol. 31, no. 1, pp. 1-9, 2005.  EDN: HSBRRT  

V. A. Nepomniaschy, I. S. Anureev, I. N. Mikhailov, and A. V. Promskii, "Towards verification of C programs. C-light language and its formal semantics", Programming and Computer Software, vol. 28, no. 6, pp. 314-323, 2002.  EDN: LHCEKP  

V. A. Nepomniaschy, I. S. Anureev, and A. V. Promskii, "Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language", Programming and Computer Software, vol. 29, no. 6, pp. 338-350, 2003.  EDN: LHWXPB  

I. V. Maryasov, V. A. Nepomniaschy, A. V. Promsky, and D. A. Kondratyev, "Automatic C Program Verification Based on Mixed Axiomatic Semantics", Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 407-414, 2014.  EDN: UOLVCP  

D. A. Kondratyev and V. A. Nepomniaschy, "Automation of C Program Deductive Verification without Using Loop Invariants", Programming and Computer Software, vol. 48, no. 5, pp. 331-346, 2022.  EDN: MIMTLQ  

D. A. Kondratyev and A. V. Promsky, "The Complex Approach of the C-lightVer System to the Automated Error Localization in C-Programs", Automatic Control and Computer Sciences, vol. 54, no. 7, pp. 728-739, 2020.  EDN: OQPQSY  

J. S. Moore, "Milestones from the Pure Lisp Theorem Prover to ACL2", Formal Aspects of Computing, vol. 31, no. 6, pp. 699-732, 2019.  

D. A. Kondratyev, I. V. Maryasov, and V. A. Nepomniaschy, "The Automation of C Program Verification by the Symbolic Method of Loop Invariant Elimination", Automatic Control and Computer Sciences, vol. 53, no. 7, pp. 653-662, 2019.  EDN: ALYSLL  

L. Zhang and B. L. Kaminski, "Quantitative strongest post: a calculus for reasoning about the flow of quantitative information", Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA1, pp. 1-29, 2022.  

S. Dailler, D. Hauzar, C. March\'e, and Y. Moy, "Instrumenting a weakest precondition calculus for counterexample generation", Journal of Logical and Algebraic Methods in Programming, vol. 99, pp. 97-113, 2018.  

B. Becker, C. B. Louren\cco, and C. March\'e, "Explaining Counterexamples with Giant-Step Assertion Checking", in Proceedings of the 6th Workshop on Formal Integrated Development Environment, vol. 338, 2021, pp. 82-88.  

Q. L. Le, J. Sun, L. H. Pham, and S. Qin, "S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs". 2022.  

T. Dardinier, G. Parthasarathy, and P. M"uller, "Verification-Preserving Inlining in Automatic Separation Logic Verifiers", Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, pp. 789-818, 2023.  

R. K"onighofer, R. Toegl, and R. Bloem, "Automatic Error Localization for Software Using Deductive Verification", in Hardware and Software: Verification and Testing, vol. 8855, Springer, 2014, pp. 92-98.  

P. Baudin et al., "The dogged pursuit of bug-free C programs: the Frama-C software analysis platform", Communications of the ACM, vol. 64, no. 8, pp. 56-68, 2021.  EDN: SQNOYR  

M. R. Gadelha, F. Monteiro, L. Cordeiro, and D. Nicole, "ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference", in Tools and Algorithms for the Construction and Analysis of Systems, vol. 11429, Springer, 2019, pp. 209-213.  

S. L"owe, "CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation", in Tools and Algorithms for the Construction and Analysis of Systems, vol. 7795, Springer, 2013, pp. 610-612.  

D. Beyer and T. Lemberger, "CPA-SymExec: efficient symbolic execution in CPAchecker", in Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018, pp. 900-903.  

C. Cadar and M. Nowack, "KLEE symbolic execution engine in 2019", International Journal on Software Tools for Technology Transfer, vol. 23, no. 6, pp. 867-870, 2021.  EDN: JIAYUP  

B. Jacobs, J. Kiniry, and M. Warnier, "Java Program Verification Challenges", in Formal Methods for Components and Objects, vol. 2852, Springer, 2003, pp. 202-219.