CPAchecker
From MaRDI portal
Cited in
(only showing first 100 items - show all)- CUTE
- iRankFinder
- Pono
- BLAST
- SLAM
- Symbolic computation via program transformation
- DiVinE
- MiBench
- Fairness modulo theory: a new approach to LTL software model checking
- A unifying view on SMT-based software verification
- TASS_
- LLVM
- KLEE
- ARMC
- Dagger
- Aspic
- PURRS
- Efficient interpolation for the theory of arrays
- ProMoVer
- Princess
- Cseq
- Predator
- SMTInterpol
- Ultimate Automizer
- PeRIPLO
- OpenSMT
- Model checking boot code from AWS data centers
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- Synthesizing ranking functions for loop programs via SVM
- Interproc
- Backward symbolic execution with loop folding
- LLBMC
- Loop verification with invariants and contracts
- UFO
- Cleaneling
- NuSMV3
- Cetus
- SLAyer
- CBMC
- VMC
- Eldarica
- MTSA
- Aligators
- SLAB
- HSF
- Threader
- ESBMC
- McAiT
- Orion
- InvA
- Efficient strategies for CEGAR-based model checking
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- Translating Xd-C programs to MSVL programs
- A novel approach to verifying context free properties of programs
- Generalized rewrite theories, coherence completion, and symbolic methods
- Wombit: a portfolio bit-vector solver using word-level propagation
- CSIsat
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Verifying a scheduling protocol of safety-critical systems
- SatAbs
- QuteRTL
- AspectC++
- YOGI
- Vellvm
- Snugglebug
- Lazy-CSeq
- RGITL
- GNATprove
- DeltaCCS
- FShell
- Wolverine
- Data-driven verification of stochastic linear systems with signal temporal logic constraints
- IKOS
- LusSy
- Program analysis with local policy iteration
- Succinct representation of concurrent trace sets
- Reducing crash recoverability to reachability
- RiTHM
- Automated formal analysis and verification: an overview
- Splitting via Interpolants
- From under-approximations to over-approximations and back
- Software model checking with explicit scheduler and symbolic threads
- Eleven82
- SQCK
- EXPLODE
- Sigma*
- LCTD
- Guiding Craig interpolation with domain-specific abstractions
- SeaHorn
- OpenSMT2
- VS3
- Predicate abstraction for program verification
- Combining model checking and data-flow analysis
- DDVerify
- Coverity
- OTAWA
- EUREKA
- PKind
- Lazy abstraction-based controller synthesis
- BOXES
This page was built for software: CPAchecker
