The following pages link to CPAchecker (Q19440):
Displaying 35 items.
- Guiding Craig interpolation with domain-specific abstractions (Q300418) (← links)
- LCTD: test-guided proofs for C programs on LLVM (Q338629) (← links)
- An extension of lazy abstraction with interpolation for programs with arrays (Q479820) (← links)
- 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. Proce (Q766306) (← links)
- Leveraging compiler intermediate representation for multi- and cross-language verification (Q784116) (← links)
- Symbolic computation via program transformation (Q1623144) (← links)
- Fairness modulo theory: a new approach to LTL software model checking (Q1702910) (← links)
- A unifying view on SMT-based software verification (Q1703012) (← links)
- Efficient interpolation for the theory of arrays (Q1799115) (← links)
- Model checking boot code from AWS data centers (Q2050104) (← links)
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (Q2058375) (← links)
- Synthesizing ranking functions for loop programs via SVM (Q2084940) (← links)
- Backward symbolic execution with loop folding (Q2145317) (← links)
- Loop verification with invariants and contracts (Q2152642) (← links)
- Efficient strategies for CEGAR-based model checking (Q2209549) (← links)
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness (Q2226974) (← links)
- Translating Xd-C programs to MSVL programs (Q2290648) (← links)
- A novel approach to verifying context free properties of programs (Q2290651) (← links)
- Generalized rewrite theories, coherence completion, and symbolic methods (Q2291817) (← links)
- Wombit: a portfolio bit-vector solver using word-level propagation (Q2323450) (← links)
- Automatically proving termination and memory safety for programs with pointer arithmetic (Q2362494) (← links)
- Verifying a scheduling protocol of safety-critical systems (Q2424721) (← links)
- Data-driven verification of stochastic linear systems with signal temporal logic constraints (Q2665419) (← links)
- Program Analysis with Local Policy Iteration (Q2796041) (← links)
- Succinct Representation of Concurrent Trace Sets (Q2819829) (← links)
- Reducing crash recoverability to reachability (Q2828248) (← links)
- Automated formal analysis and verification: an overview (Q2871577) (← links)
- Splitting via Interpolants (Q2891411) (← links)
- From Under-Approximations to Over-Approximations and Back (Q2894271) (← links)
- Software Model Checking with Explicit Scheduler and Symbolic Threads (Q2904614) (← links)
- Sigma* (Q2931821) (← links)
- Predicate Abstraction for Program Verification (Q3176373) (← links)
- Combining Model Checking and Data-Flow Analysis (Q3176374) (← links)
- Lazy Abstraction-Based Controller Synthesis (Q3297583) (← links)
- Predicate Abstraction in Program Verification: Survey and Current Trends (Q5240105) (← links)
