Boolean and Cartesian abstraction for model checking C programs
From MaRDI portal
Recommendations
Cited in
(36)- Symbolic perimeter abstraction heuristics for cost-optimal planning
- A unifying view on SMT-based software verification
- Experience of improving the BLAST static verification tool
- Efficient strategies for CEGAR-based model checking
- Syntax-guided synthesis for lemma generation in hardware model checking
- Infinite-state invariant checking with IC3 and predicate abstraction
- A divide-and-conquer approach for analysing overlaid data structures
- Abstractions of data types
- On finite-state approximants for probabilistic computation tree logic
- Trading plaintext-awareness for simulatability to achieve chosen ciphertext security
- Automated formal analysis and verification: an overview
- Whale: an interpolation-based algorithm for inter-procedural verification
- Sound and complete abstract graph transformation
- SAT-Based Model Checking
- Abstraction and abstraction refinement
- Interpolation and model checking
- Predicate abstraction for program verification
- Combining model checking and data-flow analysis
- Symbolic trajectory evaluation
- Static detection of DoS vulnerabilities in programs that use regular expressions
- Cross-Checking - Enhanced Over-Approximation of the Reachable Global State Space of Component-Based Systems
- scientific article; zbMATH DE number 1903376 (Why is no real title available?)
- Software verification with PDR: an implementation of the state of the art
- Internal and External Logics of Abstract Interpretations
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Calculational design of a regular model checker by abstract interpretation
- Verification, Model Checking, and Abstract Interpretation
- Deciding program properties via complete abstractions on bounded domains
- String abstraction for model checking of C programs
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
- Lost in abstraction: monotonicity in multi-threaded programs
- Model checking as program verification by abstract interpretation
- Verifying time partitioning in the DEOS scheduling kernel
- Data structures for symbolic multi-valued model-checking
- Verification and falsification of programs with loops using predicate abstraction
- CPBPV: a constraint-programming framework for bounded program verification
This page was built for publication: Boolean and Cartesian abstraction for model checking C programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2769592)
