CBMC
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Data compression for proof replay
- CPBPV
- CUTE
- Juliet Test Suite
- MPI-CHECK
- Synchrobench
- Zing
- APS-1
- FocusCheck
- veriSoft
- SatEx
- DiVer
- PSATO
- BLAST
- HOL/SPIN
- SLAM
- Symbolic computation via program transformation
- A compiler for MSVL and its applications
- NuSMV
- Valgrind
- RuleBasePE
- QingTing1
- VST-Floyd: a separation logic tool to verify correctness of C programs
- SAT competition
- Incremental bounded model checking for embedded software
- On compiling Boolean circuits optimized for secure multi-party computation
- Fairness modulo theory: a new approach to LTL software model checking
- A unifying view on SMT-based software verification
- LLVM
- KLEE
- ARMC
- Dagger
- A bounded model checker for three-valued abstractions of concurrent software systems
- SCRATCH
- Bogor
- SPARKSkein
- Limmat
- bv2epr
- PathCrawler
- GATeL
- DART
- Cseq
- Predator
- SMTInterpol
- Ultimate Automizer
- CPAchecker
- visualSTATE
- Java PathFinder
- Bandera
- TACO
- SystemC
- Sharpening constraint programming approaches for bit-vector theory
- A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
- Efficient bounded model checking of heap-manipulating programs using tight field bounds
- Model checking boot code from AWS data centers
- CESAR
- SPEED
- Gauss
- RunLim
- Velodrome
- Bebop
- APS
- Verifying Whiley programs with Boogie
- The \textsc{MergeSat} solver
- Inductive benchmarks for automated reasoning
- SMCHR
- URBiVA
- Rhapsody
- YASM
- LLBMC
- Jerusat
- Verification by gambling on program slices
- UFO
- eVolCheck
- AutoMOTGen
- SingleTrack
- Threader
- Checkfence
- ESBMC
- SCOOT
- MOPS
- UMM
- JFLAP
- Loop summarization using state and transition invariants
- Scalable and precise refinement of cache timing analysis via path-sensitive verification
- SIMGRID
- SPARK Pro
- Nighthawk
- Translating Xd-C programs to MSVL programs
- Automated formal synthesis of provably safe digital controllers for continuous plants
- Abstract semantic diffing of evolving concurrent programs
- ppfolio
- SIMPLY
- System-level state equality detection for the formal dynamic verification of legacy distributed applications
- Verifying a scheduling protocol of safety-critical systems
- A taxonomy of exact methods for partial Max-SAT
- An automatic method for the dynamic construction of abstractions of states of a formal model
- FloPSy
- SatAbs
- MoonWalker
This page was built for software: CBMC
