Efficient SAT-based bounded model checking for software verification

DOI10.1016/j.tcs.2008.03.013zbMath1293.68079OpenAlexW2076933173MaRDI QIDQ947794

Malay K. Ganai, Aarti Gupta, Pranav Ashar, Franjo Ivančić, Zi-Jiang Yang

Publication date: 7 October 2008

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2008.03.013

zbMATH Keywords

software verificationbounded model checkingSAT-based model checking

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers, Solving dependency quantified Boolean formulas using quantifier localization, On CDCL-Based Proof Systems with the Ordered Decision Strategy, A proof system for unified temporal logic, Efficient SAT-based bounded model checking for software verification, CPBPV: a constraint-programming framework for bounded program verification, Dynamic Path Reduction for Software Model Checking, The Edge of Graph Transformation — Graphs for Behavioural Specification, Strong extension-free proof systems, Computing properties of stable configurations of thermodynamic binding networks, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1

Uses Software

• DiVer
• SPIN
• CADP
• Bogor
• Chaff
• BerkMin
• Java PathFinder
• Bandera
• Bebop
• CBMC
• CSSV
• ASTREE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking in dense real-time
• Reasoning about networks with many identical finite state processes
• Efficient SAT-based bounded model checking for software verification
• Affine relationships among variables of a program
• Model checking JAVA programs using JAVA PathFinder
• Predicate abstraction of ANSI-C programs using SAT
• Abstractions from proofs
• Program Analysis Using Symbolic Ranges
• Static Analysis in Disjunctive Numerical Domains
• Static Analysis of Numerical Algorithms
• Graph-Based Algorithms for Boolean Function Manipulation
• GRASP: a search algorithm for propositional satisfiability
• Tools and Algorithms for the Construction and Analysis of Systems
• Static Analysis
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Computer Aided Verification
• Reachability analysis of pushdown automata: Application to model-checking