Logic for reasoning about bugs in loops over data sequences (IFIL)

DOI10.18255/1818-1015-2023-3-214-233OpenAlexW4387423274MaRDI QIDQ6062741

Unnamed Author

Publication date: 2 December 2023

Published in: Modeling and Analysis of Information Systems (Search for Journal in Brave)

Full work available at URL: http://mathnet.ru/eng/mais800

zbMATH Keywords

ACL2Hoare logicloop invariantdeductive verificationfinite iterationbug localizationC-lightVerprogram incorrectness

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Towards verification of C programs: Axiomatic semantics of the C-kernel language
• Towards verification of C programs. C-light language and its formal semantics
• Instrumenting a weakest precondition calculus for counterexample generation
• Deductive software verification: from pen-and-paper proofs to industrial tools
• Local reasoning about the presence of bugs: incorrectness separation logic
• Milestones from the Pure Lisp Theorem Prover to ACL2
• Fifty years of Hoare's logic
• Symbolic method of verification of definite iterations over altered data structures
• On algebra of program correctness and incorrectness
• Invariant Generation for Multi-Path Loops with Polynomial Assignments
• Assessing the Success and Impact of Hoare’s Logic
• An axiomatic basis for computer programming
• Adversarial logic
• Local completeness logic on Kleene algebra with tests

This page was built for publication: Logic for reasoning about bugs in loops over data sequences (IFIL)