Predicate abstraction of ANSI-C programs using SAT

DOI10.1023/B:FORM.0000040025.89719.F3MaRDI QIDQ1888196zbMATH OpenFDO

Authors Daniel Kroening, Natasha Sharygina, Karen Yorav, Edmund Clarke

Publication date 22 November 2004

Published in Formal Methods in System Design (Search for Journal in Brave)

zbMATH Keywords

SATPredicate abstractionANSI-C

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Tools and Algorithms for the Construction and Analysis of Systems
• Predicate abstraction with minimum predicates
• Tools and Algorithms for the Construction and Analysis of Systems
• Predicate Abstraction in Program Verification: Survey and Current Trends
• Verification and falsification of programs with loops using predicate abstraction

Cited in

(25)

• Loop summarization using state and transition invariants
• Verifying Heap-Manipulating Programs in an SMT Framework
• Efficient SAT-based bounded model checking for software verification
• Automated Technology for Verification and Analysis
• Implementing efficient All solutions SAT solvers
• Loop Summarization Using Abstract Transformers
• Interprocedural and flow-sensitive type analysis for memory and type safety of C code
• Predicate abstraction in a program logic calculus
• Game-Based Probabilistic Predicate Abstraction in PRISM
• Verification by gambling on program slices
• Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction
• Predicate Abstraction of Programs with Non-linear Computation
• Abstraction and abstraction refinement
• Verification and falsification of programs with loops using predicate abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Constraint-Based Invariant Inference over Predicate Abstraction
• Ranking function synthesis for bit-vector relations
• SAT-Based Model Checking
• Making predicate abstraction efficient: how to eliminate redundant predicates
• Predicate abstraction with minimum predicates
• CPBPV: a constraint-programming framework for bounded program verification
• Verification of Boolean programs with unbounded thread creation
• Tools and Algorithms for the Construction and Analysis of Systems
• Automatic abstraction of equations in a logic of equality
• Verification of SpecC using predicate abstraction

Describes a project that uses

Uses Software

• Java PathFinder
• Chaff

This page was built for publication: Predicate abstraction of ANSI-C programs using SAT

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