CPAchecker
From MaRDI portal
Software:19440
No author found.
Related Items (42)
Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Software Verification with PDR: An Implementation of the State of the Art ⋮ Symbolic computation via program transformation ⋮ Splitting via Interpolants ⋮ From Under-Approximations to Over-Approximations and Back ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ Software Model Checking with Explicit Scheduler and Symbolic Threads ⋮ Predicate Abstraction for Program Verification ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Backward symbolic execution with loop folding ⋮ Loop verification with invariants and contracts ⋮ LCTD: test-guided proofs for C programs on LLVM ⋮ The MathSAT5 SMT Solver ⋮ Data-driven verification of stochastic linear systems with signal temporal logic constraints ⋮ Verifying a scheduling protocol of safety-critical systems ⋮ Fairness modulo theory: a new approach to LTL software model checking ⋮ A unifying view on SMT-based software verification ⋮ Efficient strategies for CEGAR-based model checking ⋮ Predicate Abstraction in Program Verification: Survey and Current Trends ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Predicate extension of symbolic memory graphs for the analysis of memory safety correctness ⋮ An Introduction to Test Specification in FQL ⋮ Lazy Abstraction-Based Controller Synthesis ⋮ DSValidator ⋮ Program Analysis with Local Policy Iteration ⋮ Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints ⋮ Translating Xd-C programs to MSVL programs ⋮ A novel approach to verifying context free properties of programs ⋮ Efficient interpolation for the theory of arrays ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Model checking boot code from AWS data centers ⋮ Succinct Representation of Concurrent Trace Sets ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ Reducing crash recoverability to reachability ⋮ Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012. Proceedings ⋮ Loop Invariants from Counterexamples ⋮ Wombit: a portfolio bit-vector solver using word-level propagation ⋮ Sigma* ⋮ Leveraging compiler intermediate representation for multi- and cross-language verification ⋮ Synthesizing ranking functions for loop programs via SVM ⋮ Automated formal analysis and verification: an overview
This page was built for software: CPAchecker
