CPAchecker

swMATH7408MaRDI QIDQ19440FDOQ19440

Author name not available (Why is that?)

Official website: http://cpachecker.sosy-lab.org/

Cited In (76)

• Software model checking with explicit scheduler and symbolic threads
• Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
• Lazy abstraction-based controller synthesis
• Efficient strategies for CEGAR-based model checking
• Generalized rewrite theories, coherence completion, and symbolic methods
• Translating Xd-C programs to MSVL programs
• Data-driven verification of stochastic linear systems with signal temporal logic constraints
• Wombit: a portfolio bit-vector solver using word-level propagation
• Splitting via Interpolants
• Symbolic computation via program transformation
• Program analysis with local policy iteration
• Efficient interpolation for the theory of arrays
• Fairness modulo theory: a new approach to LTL software model checking
• Predicate abstraction for program verification
• An extension of lazy abstraction with interpolation for programs with arrays
• Guiding Craig interpolation with domain-specific abstractions
• Automated formal analysis and verification: an overview
• An introduction to test specification in FQL
• Software verification with PDR: an implementation of the state of the art
• Backward symbolic execution with loop folding
• Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints
• Loop verification with invariants and contracts
• Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
• MiBench
• 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
• Interproc
• Cetus
• CBMC
• Aligators
• NuSMV3
• Eldarica
• SLAyer
• VMC
• AspectC++
• SatAbs
• QuteRTL
• YOGI
• Vellvm
• Snugglebug
• GNATprove
• LCTD
• LCTD: test-guided proofs for C programs on LLVM
• SeaHorn
• Sigma*
• CoVaC
• Sigma*
• Chisel
• MinGW
• DSValidator
• DSVerifier
• Skink
• SAFARI
• Ultimate Taipan
• C2M
• MSVL
• UMC4M
• Yosys
• Model checking boot code from AWS data centers
• Succinct representation of concurrent trace sets
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Reducing crash recoverability to reachability
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• A novel approach to verifying context free properties of programs
• Leveraging compiler intermediate representation for multi- and cross-language verification
• Pono
• Combining model checking and data-flow analysis
• Predicate Abstraction in Program Verification: Survey and Current Trends
• TreeAutomizer
• A unifying view on SMT-based software verification
• From under-approximations to over-approximations and back
• The MathSAT5 SMT solver
• Synthesizing ranking functions for loop programs via SVM
• MTSA
• DSValidator: an automated counterexample reproducibility tool for digital systems
• Verifying a scheduling protocol of safety-critical systems
• Loop Invariants from Counterexamples

This page was built for software: CPAchecker