STP

From MaRDI portal
Software:46504



swMATH34795MaRDI QIDQ46504


No author found.

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




Related Items (40)

Combining SAT solvers with computer algebra systems to verify combinatorial conjecturesA layered algorithm for quantifier elimination from linear modular constraintsSatisfiability Modulo TheoriesCombining Model Checking and TestingAutomatic search for bit-based division propertyLCTD: test-guided proofs for C programs on LLVMA bit-vector differential model for the modular addition by a constant and its applications to differential and impossible-differential cryptanalysisStrategies for scalable symbolic execution-driven test generation for programsSimulating circuit-level simplifications on CNFExecuting and verifying higher-order functional-imperative programs in MaudePropagation based local search for bit-precise reasoningA bit-vector differential model for the modular addition by a constantFormal testing for separation assuranceDiscovering invariants via simple component analysisBlack-box testing based on colorful taint analysisEfficiently solving quantified bit-vector formulasEstablishing flight software reliability: testing, model checking, constraint-solving, monitoring and learningSymbolic Execution as DPLL Modulo TheoriesTest generation from event system abstractions to cover their states and transitionsSimple linear string constraintsAlgorithm and tools for constructing canonical forms of linear semi-algebraic formulasSymbolic execution formally explainedComplexity of fixed-size bit-vector logicsReplacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic executionA generic framework for symbolic execution: a coinductive approachAssociation of Under-Approximation Techniques for Generating Tests from ModelsSymbolic execution based on language transformationParallelizing SMT solving: lazy decomposition and conciliationSharpening constraint programming approaches for bit-vector theoryDynamic Path Reduction for Software Model CheckingPath Feasibility Analysis for String-Manipulating ProgramsThe SAT+CAS method for combinatorial search with applications to best matricesOptimization modulo the theories of signed bit-vectors and floating-point numbersAutomatic Differential Analysis of ARX Block Ciphers with Application to SPECK and LEALearning Rate Based Branching Heuristic for SAT SolversDeciding Bit-Vector Formulas with mcSATWombit: a portfolio bit-vector solver using word-level propagationIntegration of verification methods for program systemsArray theory of bounded elements and its applicationsOn the hierarchical community structure of practical Boolean formulas


This page was built for software: STP