STP
From MaRDI portal
Software:46504
No author found.
Source code repository: https://github.com/stp/stp
Related Items (40)
Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ A layered algorithm for quantifier elimination from linear modular constraints ⋮ Satisfiability Modulo Theories ⋮ Combining Model Checking and Testing ⋮ Automatic search for bit-based division property ⋮ LCTD: test-guided proofs for C programs on LLVM ⋮ A bit-vector differential model for the modular addition by a constant and its applications to differential and impossible-differential cryptanalysis ⋮ Strategies for scalable symbolic execution-driven test generation for programs ⋮ Simulating circuit-level simplifications on CNF ⋮ Executing and verifying higher-order functional-imperative programs in Maude ⋮ Propagation based local search for bit-precise reasoning ⋮ A bit-vector differential model for the modular addition by a constant ⋮ Formal testing for separation assurance ⋮ Discovering invariants via simple component analysis ⋮ Black-box testing based on colorful taint analysis ⋮ Efficiently solving quantified bit-vector formulas ⋮ Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning ⋮ Symbolic Execution as DPLL Modulo Theories ⋮ Test generation from event system abstractions to cover their states and transitions ⋮ Simple linear string constraints ⋮ Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas ⋮ Symbolic execution formally explained ⋮ Complexity of fixed-size bit-vector logics ⋮ Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ Association of Under-Approximation Techniques for Generating Tests from Models ⋮ Symbolic execution based on language transformation ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Sharpening constraint programming approaches for bit-vector theory ⋮ Dynamic Path Reduction for Software Model Checking ⋮ Path Feasibility Analysis for String-Manipulating Programs ⋮ The SAT+CAS method for combinatorial search with applications to best matrices ⋮ Optimization modulo the theories of signed bit-vectors and floating-point numbers ⋮ Automatic Differential Analysis of ARX Block Ciphers with Application to SPECK and LEA ⋮ Learning Rate Based Branching Heuristic for SAT Solvers ⋮ Deciding Bit-Vector Formulas with mcSAT ⋮ Wombit: a portfolio bit-vector solver using word-level propagation ⋮ Integration of verification methods for program systems ⋮ Array theory of bounded elements and its applications ⋮ On the hierarchical community structure of practical Boolean formulas
This page was built for software: STP