Verification and falsification of programs with loops using predicate abstraction

DOI10.1007/S00165-009-0110-2MaRDI QIDQ968302zbMATH OpenOpenAlexWikidataFDO

Authors 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)

Recommendations

• Predicate abstraction for software verification
• Predicate Abstraction in Program Verification: Survey and Current Trends
• Tools and Algorithms for the Construction and Analysis of Systems
• Predicate abstraction for program verification
• Predicate abstraction with minimum predicates

Cites work

• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1670780 (Why is no real title available?)
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 194009 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 1954380 (Why is no real title available?)
• scientific article; zbMATH DE number 2080047 (Why is no real title available?)
• scientific article; zbMATH DE number 3995020 (Why is no real title available?)
• scientific article; zbMATH DE number 1903378 (Why is no real title available?)
• Abstractions from proofs
• An axiomatic basis for computer programming
• Computer Aided Verification
• Constructive versions of Tarski's fixed point theorems
• Guarded commands, nondeterminacy and formal derivation of programs
• Invariant Synthesis for Combined Theories
• Lazy Abstraction with Interpolants
• Lazy abstraction
• Leaping Loops in the Presence of Abstraction
• Model Checking Software
• Predicate abstraction of ANSI-C programs using SAT
• Programming Languages and Systems
• Static Analysis
• The Daikon system for dynamic detection of likely invariants
• Theory and Applications of Satisfiability Testing
• Tools and Algorithms for the Construction and Analysis of Systems
• 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

Cited in

(9)

• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• scientific article; zbMATH DE number 1956497 (Why is no real title available?)
• Predicate abstraction for program verification
• Predicate abstraction of ANSI-C programs using SAT
• Proving safety with trace automata and bounded model checking
• Predicate Abstraction of Programs with Non-linear Computation
• Under-approximating loops in C programs for fast counterexample detection
• Verification, Model Checking, and Abstract Interpretation
• Predicate abstraction for software verification

Describes a project that uses

Uses Software

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

This page was built for publication: Verification and falsification of programs with loops using predicate abstraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q968302)