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)

Full work available at URL https://doi.org/10.1023/B:FORM.0000040025.89719.F3

zbMATH Keywords

ANSI-CPredicate abstractionSAT

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

(27)

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

Describes a project that uses

Uses Software

• Chaff
• Java PathFinder

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)