SATABS: SAT-based predicate abstraction for ANSI-C

DOI10.1007/978-3-540-31980-1_40MaRDI QIDQ5703792zbMATH OpenOpenAlexFDO

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

Publication date 10 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b107194

Mathematics Subject Classification ID

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

Recommendations

• Predicate abstraction of ANSI-C programs using SAT
• F-Soft: Software verification platform
• Efficient SAT-based bounded model checking for software verification
• Model checking: from hardware to software.
• Software verification with BLAST

Cited in

(25)

• Predicate abstraction of ANSI-C programs using SAT
• Efficient strategies for CEGAR-based model checking
• Loop summarization using state and transition invariants
• Verification of SpecC using predicate abstraction
• Verification of Boolean programs with unbounded thread creation
• Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
• Automated formal analysis and verification: an overview
• Splitting via Interpolants
• Loop Summarization and Termination Analysis
• SAT-Based Model Checking
• Abstraction and abstraction refinement
• Interpolation and model checking
• Predicate abstraction for program verification
• Temporalization of Probabilistic Propositional Logic
• A model checking-based approach for security policy verification of mobile systems
• Counterexample guided path reduction for static program analysis
• Predicate abstraction in program verification: survey and current trends
• Tools and Algorithms for the Construction and Analysis of Systems
• Model-Checking HyperLTL for Pushdown Systems
• Context-aware counter abstraction
• Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths
• Automatic analysis of DMA races using model checking and k-induction
• 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

• ComFoRT
• SatAbs

This page was built for publication: SATABS: SAT-based predicate abstraction for ANSI-C

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