Efficient SAT-based bounded model checking for software verification
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1670555 (Why is no real title available?)
- scientific article; zbMATH DE number 1670775 (Why is no real title available?)
- scientific article; zbMATH DE number 438994 (Why is no real title available?)
- scientific article; zbMATH DE number 1956569 (Why is no real title available?)
- scientific article; zbMATH DE number 1979542 (Why is no real title available?)
- scientific article; zbMATH DE number 1738295 (Why is no real title available?)
- scientific article; zbMATH DE number 1796132 (Why is no real title available?)
- scientific article; zbMATH DE number 1903357 (Why is no real title available?)
- scientific article; zbMATH DE number 2102703 (Why is no real title available?)
- A symbolic approach to predicate abstraction.
- Abstractions from proofs
- Affine relationships among variables of a program
- Computer Aided Verification
- Efficient SAT-based bounded model checking for software verification
- GRASP: a search algorithm for propositional satisfiability
- Graph-Based Algorithms for Boolean Function Manipulation
- Interpolation and SAT-based model checking.
- Model checking JAVA programs using JAVA PathFinder
- Model-checking in dense real-time
- Predicate abstraction of ANSI-C programs using SAT
- Program Analysis Using Symbolic Ranges
- Reachability analysis of pushdown automata: Application to model-checking
- Reasoning about networks with many identical finite state processes
- Static Analysis
- Static Analysis in Disjunctive Numerical Domains
- Static Analysis of Numerical Algorithms
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification, Model Checking, and Abstract Interpretation
Cited in
(23)- Dynamic Path Reduction for Software Model Checking
- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
- Efficient SAT-based bounded model checking for software verification
- The Edge of Graph Transformation — Graphs for Behavioural Specification
- On CDCL-Based Proof Systems with the Ordered Decision Strategy
- The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
- Theory and Applications of Models of Computation
- scientific article; zbMATH DE number 5051652 (Why is no real title available?)
- Optimized SAT encoding of conformance checking artefacts
- Software verification with PDR: an implementation of the state of the art
- Solving dependency quantified Boolean formulas using quantifier localization
- SAT-Based Model Checking
- Bounded model checking of C programs using event automaton specifications
- Incremental bounded model checking for embedded software
- Strong extension-free proof systems
- CPBPV: a constraint-programming framework for bounded program verification
- A proof system for unified temporal logic
- Computing properties of stable configurations of thermodynamic binding networks
- A bounded model checker for SPARK programs
- Tools and Algorithms for the Construction and Analysis of Systems
- SAT-Based Model Checking without Unrolling
- Model checking of concurrent software systems via heuristic-guided SAT solving
- Improving saturation-based bounded model checking
Describes a project that uses
Uses Software
This page was built for publication: Efficient SAT-based bounded model checking for software verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q947794)