Cited in
(only showing first 100 items - show all)- Loop Invariants from Counterexamples
- 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
- Software model checking with explicit scheduler and symbolic threads
- Symbolic computation via program transformation
- Efficient interpolation for the theory of arrays
- Program analysis with local policy iteration
- Fairness modulo theory: a new approach to LTL software model checking
- An extension of lazy abstraction with interpolation for programs with arrays
- Predicate abstraction for program verification
- Guiding Craig interpolation with domain-specific abstractions
- Automated formal analysis and verification: an overview
- An introduction to test specification in FQL
- Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
- 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
- CUTE
- BLAST
- SLAM
- DiVinE
- MiBench
- ARMC
- Aspic
- KLEE
- LLVM
- Dagger
- TASS_
- PURRS
- ProMoVer
- Princess
- Cseq
- Predator
- SMTInterpol
- Ultimate Automizer
- UFO
- PeRIPLO
- OpenSMT
- Interproc
- Cleaneling
- LLBMC
- Cetus
- CBMC
- Aligators
- NuSMV3
- Eldarica
- SLAyer
- ESBMC
- HSF
- McAiT
- SLAB
- Orion
- InvA
- VMC
- Threader
- CSIsat
- AspectC++
- SatAbs
- QuteRTL
- YOGI
- Lazy-CSeq
- Vellvm
- Snugglebug
- GNATprove
- RGITL
- DeltaCCS
- FShell
- IKOS
- LusSy
- Wolverine
- RiTHM
- Eleven82
- EXPLODE
- LCTD
- SQCK
- SeaHorn
- OpenSMT2
- Coverity
- DDVerify
- VS3
- OTAWA
- EUREKA
- BOXES
- PKind
- CoVaC
- BoogiePL
- ROCS
- Sigma*
- Chisel
- DyTa
- EnerJ
- CTIGAR
- FuncTion
- LTLAutomizer
- SMACK
- BIGNUM
This page was built for software: CPAchecker
