Verification and falsification of programs with loops using predicate abstraction

DOI10.1007/S00165-009-0110-2zbMATH Open1215.68130OpenAlexW2024978854WikidataQ62040472 ScholiaQ62040472MaRDI QIDQ968302FDOQ968302

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

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

zbMATH Keywords

verification of programs with loops

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (7)

• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Title not available (Why is that?)
• Predicate abstraction of ANSI-C programs using SAT
• Predicate Abstraction of Programs with Non-linear Computation
• Under-approximating loops in C programs for fast counterexample detection
• Verification, Model Checking, and Abstract Interpretation
• Proving Safety with Trace Automata and Bounded Model Checking

Uses Software

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

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)