Verification and falsification of programs with loops using predicate abstraction

DOI10.1007/s00165-009-0110-2zbMath1215.68130OpenAlexW2024978854WikidataQ62040472 ScholiaQ62040472MaRDI QIDQ968302

Daniel Kroening, Georg Weissenbacher

Publication date: 5 May 2010

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-009-0110-2

zbMATH Keywords

verification of programs with loops

Mathematics Subject Classification ID

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

Related Items

Proving Safety with Trace Automata and Bounded Model Checking, Under-approximating loops in C programs for fast counterexample detection

Uses Software

• MiniSat
• SLAM
• SPIN
• Daikon
• Bebop
• SatAbs
• EUREKA
• FAST

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructive versions of Tarski's fixed point theorems
• Predicate abstraction of ANSI-C programs using SAT
• The Daikon system for dynamic detection of likely invariants
• Abstractions from proofs
• Guarded commands, nondeterminacy and formal derivation of programs
• Lazy abstraction
• Theory and Applications of Satisfiability Testing
• Model Checking Software
• Leaping Loops in the Presence of Abstraction
• Invariant Synthesis for Combined Theories
• Programming Languages and Systems
• An axiomatic basis for computer programming
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Lazy Abstraction with Interpolants
• Static Analysis
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation