KLEE
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Beaver
- Boolector
- CUTE
- JMLUnit
- StringFuzz
- Ghidra
- Whiley
- BtorMC
- CalFuzzer
- WoLFram
- TVOC
- BLAST
- Symbolic computation via program transformation
- DiVinE
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
- Valgrind
- MiBench
- SAT competition
- Incremental bounded model checking for embedded software
- TASS_
- LLVM
- ISP
- Bogor
- SPARKSkein
- Limmat
- LTSmin
- PathCrawler
- ADL
- DART
- Euclide
- Pex
- Predator
- CPAchecker
- TASS: the toolkit for accurate scientific software
- FEVS: a functional equivalence verification suite for high-performance scientific computing
- Java PathFinder
- Symbolic execution formally explained
- Model checking boot code from AWS data centers
- Verifying Whiley programs with Boogie
- Algorithm selection for dynamic symbolic execution: a preliminary study
- MARMOT
- TRACER
- UFO
- ConTest
- Cetus
- CBMC
- r-TuBound
- Syntax-guided rewrite rule enumeration for SMT solvers
- ns-3
- libalf
- BitBlaze
- Efficient strategies for CEGAR-based model checking
- Scalable and precise refinement of cache timing analysis via path-sensitive verification
- SPARK Pro
- Nighthawk
- Wombit: a portfolio bit-vector solver using word-level propagation
- Constraint programming for dynamic symbolic execution of JavaScript
- Automatically proving termination and memory safety for programs with pointer arithmetic
- JPF-SE
- Executing and verifying higher-order functional-imperative programs in Maude
- BAP
- FloPSy
- SatAbs
- YOGI
- Snugglebug
- Joogie
- KLOVER
- Ctrl
- Smacc
- FShell
- Wolverine
- CodeSonar
- Klockwork
- Automated formal analysis and verification: an overview
- Loop invariant symbolic execution for parallel programs
- EXPLODE
- Sigma*
- LCTD
- Collective assertions
- Looper
- VS3
- JST
- Efficient loop navigation for symbolic execution
- Combining model checking and testing
- Coverity
- OTAWA
- Connecting program synthesis and reachability: automatic program repair using test-input generation
- CoVaC
- BoogiePL
- Luck
- Sigma*
- BotMiner
- Norn
- LCTD: test-guided proofs for C programs on LLVM
- Symbolic memory with pointers
- Rewriting modulo SMT and open system analysis
- SMACK
- BIGNUM
- ANaConDA
- KLEE-FP
This page was built for software: KLEE
