CPAchecker

swMATH7408MaRDI QIDQ19440FDOQ19440

Author name not available (Why is that?)

Cited In (42)

• Efficient strategies for CEGAR-based model checking
• Generalized rewrite theories, coherence completion, and symbolic methods
• An Introduction to Test Specification in FQL
• Combining Model Checking and Data-Flow Analysis
• 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
• From Under-Approximations to Over-Approximations and Back
• Software model checking with explicit scheduler and symbolic threads
• Symbolic computation via program transformation
• Lazy Abstraction-Based Controller Synthesis
• Efficient interpolation for the theory of arrays
• Fairness modulo theory: a new approach to LTL software model checking
• 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
• Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
• Backward symbolic execution with loop folding
• Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints
• Program Analysis with Local Policy Iteration
• Loop verification with invariants and contracts
• Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
• 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
• LCTD: test-guided proofs for C programs on LLVM
• Predicate Abstraction for Program Verification
• Sigma*
• DSValidator
• The MathSAT5 SMT Solver
• 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
• Predicate Abstraction in Program Verification: Survey and Current Trends
• A unifying view on SMT-based software verification
• Synthesizing ranking functions for loop programs via SVM
• Verifying a scheduling protocol of safety-critical systems
• Loop Invariants from Counterexamples
• Software Verification with PDR: An Implementation of the State of the Art

This page was built for software: CPAchecker