swMATH34795MaRDI QIDQ46504FDOQ46504
Author name not available (Why is that?)
Official website: http://stp.github.io
Source code repository: https://github.com/stp/stp
Cited In (only showing first 100 items - show all)
- RHLE Benchmarks
- Test generation from event system abstractions to cover their states and transitions
- On the hierarchical community structure of practical Boolean formulas
- Parallelizing SMT solving: lazy decomposition and conciliation
- A bit-vector differential model for the modular addition by a constant
- Combining model checking and testing
- Automatic search for bit-based division property
- Symbolic Execution as DPLL Modulo Theories
- A bit-vector differential model for the modular addition by a constant and its applications to differential and impossible-differential cryptanalysis
- Optimization modulo the theories of signed bit-vectors and floating-point numbers
- SaDiCaL
- A layered algorithm for quantifier elimination from linear modular constraints
- The SAT+CAS method for combinatorial search with applications to best matrices
- Executing and verifying higher-order functional-imperative programs in Maude
- Association of under-approximation techniques for generating tests from models
- Dynamic Path Reduction for Software Model Checking
- Symbolic execution formally explained
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Automatic differential analysis of ARX block ciphers with application to SPECK and LEA
- Wombit: a portfolio bit-vector solver using word-level propagation
- Path Feasibility Analysis for String-Manipulating Programs
- Array theory of bounded elements and its applications
- Symbolic execution based on language transformation
- Formal testing for separation assurance
- Discovering invariants via simple component analysis
- Black-box testing based on colorful taint analysis
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- Deciding Bit-Vector Formulas with mcSAT
- Efficiently solving quantified bit-vector formulas
- Boolector
- HaifaSat
- Yices
- KLEE
- UCLID
- UniTESK
- Limmat
- bv2epr
- SPARKSkein
- DART
- GATeL
- Eclat
- Pex
- Simple linear string constraints
- TRACER
- Lackwit
- MathSAT
- MathSAT5
- r-TuBound
- BitBlaze
- Nighthawk
- SPARK Pro
- NModel
- SpecExplorer
- Kaluza
- JPF-SE
- Skeptik
- YOGI
- Lynx
- MathCheck
- Snugglebug
- Smacc
- CodeSonar
- Klockwork
- EXPLODE
- LCTD
- LCTD: test-guided proofs for C programs on LLVM
- Looper
- OTAWA
- SageSAT
- OSMOSE
- TCAS
- BIGNUM
- KLOVERA
- CHAM
- LEA
- CATG
- CIL
- jCUTE
- UppSAT
- BINSEC/SE
- LCT
- AGEDIS
- KOOL
- Satisfiability modulo theories
- TEA
- XKCP
- AIspace
- Wombit
- MachSMT
- Integration of verification methods for program systems
- Strategies for scalable symbolic execution-driven test generation for programs
- Simulating circuit-level simplifications on CNF
- A generic framework for symbolic execution: a coinductive approach
- Propagation based local search for bit-precise reasoning
- PReLearn
- MedleySolver
- Complexity of fixed-size bit-vector logics
- Sharpening constraint programming approaches for bit-vector theory
- Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution
- Learning rate based branching heuristic for SAT solvers
This page was built for software: STP
