SMT-LIB

swMATH4103MaRDI QIDQ16290

No author found.

Related Items (only showing first 100 items - show all)

A decision procedure for (co)datatypes in SMT solvers ⋮ Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Deciding probabilistic automata weak bisimulation: theory and practice ⋮ Inductive benchmarks for automated reasoning ⋮ Automated generation of exam sheets for automated deduction ⋮ Symbolic computation via program transformation ⋮ The 2013 evaluation of SMT-COMP and SMT-LIB ⋮ Decision procedures for flat array properties ⋮ An experiment with satisfiability modulo SAT ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ Vampire with a brain is a good ITP hammer ⋮ Optimization modulo non-linear arithmetic via incremental linearization ⋮ An SMT solver for regular expressions and linear arithmetic over string length ⋮ A unified framework for DPLL(T) + certificates ⋮ Verification of clock synchronization algorithms: experiments on a combination of deductive tools ⋮ Modelling and solving temporal reasoning as propositional satisfiability ⋮ Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) ⋮ Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition ⋮ Strategies for scalable symbolic execution-driven test generation for programs ⋮ Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint ⋮ The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Polynomial constraints and unsat cores in \textsc{Tarski} ⋮ Satisfiability modulo bounded checking ⋮ Syntax-guided rewrite rule enumeration for SMT solvers ⋮ DRAT-based bit-vector proofs in CVC4 ⋮ SMT-based generation of symbolic automata ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Formal verification of synchronous data-flow program transformations toward certified compilers ⋮ Algorithmic introduction of quantified cuts ⋮ Automated theory exploration for interactive theorem proving: an introduction to the Hipster system ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Randomized algorithms for finding the shortest negative cost cycle in networks ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ Design and results of the Fifth Answer Set Programming Competition ⋮ Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers ⋮ Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT ⋮ Cutting the mix ⋮ Combining decision procedures by (model-)equality propagation ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Exploiting step semantics for efficient bounded model checking of asynchronous systems ⋮ SAT modulo linear arithmetic for solving polynomial constraints ⋮ Efficiently solving quantified bit-vector formulas ⋮ SMT proof checking using a logical framework ⋮ Induction with generalization in superposition reasoning ⋮ Resolution proof transformation for compression and interpolation ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Solving constraint satisfaction problems with SAT modulo theories ⋮ Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories ⋮ Making theory reasoning simpler ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) ⋮ Complexity of fixed-size bit-vector logics ⋮ The incremental satisfiability problem for a two conjunctive normal form ⋮ A decision procedure for separation logic in SMT ⋮ Decision procedures. An algorithmic point of view ⋮ Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings ⋮ Exploiting subproblem optimization in SAT-based maxsat algorithms ⋮ Z3str2: an efficient solver for strings, regular expressions, and length constraints ⋮ On the complexity of reconstructing chemical reaction networks ⋮ Sharpening constraint programming approaches for bit-vector theory ⋮ Linear time-dependent constraints programming with MSVL ⋮ MNiBLoS: a SMT-based solver for continuous t-norm based logics and some of their modal expansions ⋮ Tactics and certificates in Meta Dedukti ⋮ EUFORIA: complete software model checking with uninterpreted functions ⋮ Positive solutions of systems of signed parametric polynomial inequalities ⋮ A generic framework for implicate generation modulo theories ⋮ Superposition with datatypes and codatatypes ⋮ A FOOLish encoding of the next state relations of imperative programs ⋮ Datatypes with shared selectors ⋮ Integrating external deduction tools with ACL2 ⋮ Algorithmic reduction of biological networks with multiple time scales ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories ⋮ Integer induction in saturation ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ Extending SMT solvers to higher-order logic ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ Induction in saturation-based proof search ⋮ Faster, higher, stronger: E 2.3 ⋮ Optimization modulo the theory of floating-point numbers ⋮ Editorial: Symbolic computation and satisfiability checking ⋮ Fully incremental cylindrical algebraic decomposition ⋮ Cylindrical algebraic decomposition with equational constraints ⋮ Applying computer algebra systems with SAT solvers to the Williamson conjecture ⋮ Solving quantified verification conditions using satisfiability modulo theories ⋮ Unification with abstraction and theory instantiation in saturation-based reasoning ⋮ Constraint programming for dynamic symbolic execution of JavaScript ⋮ Solving bitvectors with MCSAT: explanations from bits and pieces ⋮ Subsumption demodulation in first-order theorem proving ⋮ Layered clause selection for theory reasoning (short paper) ⋮ Solving strong controllability of temporal problems with uncertainty using SMT ⋮ Verifying Whiley programs with Boogie ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ Reasoning about vectors using an SMT theory of sequences ⋮ New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis ⋮ Extending Sledgehammer with SMT solvers ⋮ Smt-Switch: a solver-agnostic C++ API for SMT solving

This page was built for software: SMT-LIB