Predicate abstraction of ANSI-C programs using SAT
From MaRDI portal
Publication:1888196
DOI10.1023/B:FORM.0000040025.89719.f3zbMath1090.68022MaRDI QIDQ1888196
Karen Yorav, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
Publication date: 22 November 2004
Published in: Formal Methods in System Design (Search for Journal in Brave)
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Verification of SpecC using predicate abstraction ⋮ Interprocedural and flow-sensitive type analysis for memory and type safety of C code ⋮ SAT-Based Model Checking ⋮ Abstraction and Abstraction Refinement ⋮ Verification by gambling on program slices ⋮ Verifying Heap-Manipulating Programs in an SMT Framework ⋮ Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction ⋮ Loop Summarization Using Abstract Transformers ⋮ Verification of Boolean programs with unbounded thread creation ⋮ Efficient SAT-based bounded model checking for software verification ⋮ Loop summarization using state and transition invariants ⋮ Ranking function synthesis for bit-vector relations ⋮ Game-Based Probabilistic Predicate Abstraction in PRISM ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ CPBPV: a constraint-programming framework for bounded program verification ⋮ Implementing Efficient All Solutions SAT Solvers
Uses Software
This page was built for publication: Predicate abstraction of ANSI-C programs using SAT
