SMT-LIB

swMATH4103MaRDI QIDQ16290FDOQ16290

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• Editorial: Symbolic computation and satisfiability checking
• Coming to terms with quantified reasoning
• Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions
• Scalable fine-grained proofs for formula processing
• Optimization modulo non-linear arithmetic via incremental linearization
• An SMT solver for regular expressions and linear arithmetic over string length
• Vampire with a brain is a good ITP hammer
• Building bridges between symbolic computation and satisfiability checking
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
• Symbolic computation via program transformation
• The \textsc{SDEval} benchmarking toolkit
• Cylindrical algebraic decomposition with equational constraints
• The incremental satisfiability problem for a two conjunctive normal form
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Matching multiplications in bit-vector formulas
• Horn clause solvers for program verification
• TIP: tons of inductive problems
• Extensional crisis and proving identity
• Polyhedral approximation of multivariate polynomials using Handelman's theorem
• Solving nonlinear integer arithmetic with MCSAT
• Certified roundoff error bounds using semidefinite programming
• Randomized algorithms for finding the shortest negative cost cycle in networks
• Incomplete SMT techniques for solving non-linear formulas over the integers
• Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Algorithmic reduction of biological networks with multiple time scales
• Improving ENIGMA-style clause selection while learning from history
• Reliable reconstruction of fine-grained proofs in a proof assistant
• Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
• Layered clause selection for theory reasoning (short paper)
• Solving bitvectors with MCSAT: explanations from bits and pieces
• Expressing polymorphic types in a many-sorted language
• DRAT-based bit-vector proofs in CVC4
• On the complexity of reconstructing chemical reaction networks
• Petri Net Synthesis for Restricted Classes of Nets
• Optimization modulo the theory of floating-point numbers
• Fully incremental cylindrical algebraic decomposition
• Satisfiability modulo bounded checking
• The TPTP typed first-order form with arithmetic
• Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
• A unified framework for DPLL(T) + certificates
• Subsumption demodulation in first-order theorem proving
• Information flow in object-oriented software
• Proving the incompatibility of efficiency and strategyproofness via SMT solving
• A Progressive Simplifier for Satisfiability Modulo Theories
• Reasoning with finite sets and cardinality constraints in SMT
• Generating minimum transitivity constraints in P-time for deciding equality logic
• Design and results of the Fifth Answer Set Programming Competition
• Tactics and certificates in Meta Dedukti
• Inductive benchmarks for automated reasoning
• Invariant generation through strategy iteration in succinctly represented control flow graphs
• Positive solutions of systems of signed parametric polynomial inequalities
• A generic framework for implicate generation modulo theories
• A FOOLish encoding of the next state relations of imperative programs
• Datatypes with shared selectors
• Superposition with datatypes and codatatypes
• Solving quantified linear arithmetic by counterexample-guided instantiation
• \textsf{TSAT++}: an open platform for satisfiability modulo theories
• Computer Aided Verification
• TIP: tools for inductive provers
• Sharpening constraint programming approaches for bit-vector theory
• Model finding for recursive functions in SMT
• Goal-directed invariant synthesis for model checking modulo theories
• Modular reasoning about heap paths via effectively propositional formulas
• \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
• Title not available (Why is that?)
• Decision procedures. An algorithmic point of view
• Smt-Switch: a solver-agnostic C++ API for SMT solving
• Exploiting subproblem optimization in SAT-based maxsat algorithms
• Extending Sledgehammer with SMT solvers
• Faster, higher, stronger: E 2.3
• Algorithmic introduction of quantified cuts
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• MNiBLoS: a SMT-based solver for continuous t-norm based logics and some of their modal expansions
• EUFORIA: complete software model checking with uninterpreted functions
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• 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
• Resolution proof transformation for compression and interpolation
• Automated Reasoning
• Modelling and solving temporal reasoning as propositional satisfiability
• Deciding probabilistic automata weak bisimulation: theory and practice
• Automated Termination in Model Checking Modulo Theories
• Term Rewriting with Logical Constraints
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• The 2013 evaluation of SMT-COMP and SMT-LIB
• Decision procedures for flat array properties
• An experiment with satisfiability modulo SAT
• Adding decision procedures to SMT solvers using axioms with triggers
• Semi-intelligible Isar proofs from machine-generated proofs
• Combining decision procedures by (model-)equality propagation
• Exploiting step semantics for efficient bounded model checking of asynchronous systems
• SAT modulo linear arithmetic for solving polynomial constraints
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• An extension of lazy abstraction with interpolation for programs with arrays
• Cutting the mix
• Computing small unsatisfiable cores in satisfiability modulo theories

This page was built for software: SMT-LIB