STP

swMATH34795MaRDI QIDQ46504FDOQ46504

Author name not available (Why is that?)

Official website: http://stp.github.io

Source code repository: https://github.com/stp/stp

Described by source

• A Decision Procedure for Bit-Vectors and Arrays

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