SMT-LIB

swMATH4103MaRDI QIDQ16290

No author found.

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

Ground interpolation for the theory of equality ⋮ Computing All-Pairs Shortest Paths by Leveraging Low Treewidth ⋮ Applying Machine Learning to Heuristics for Real Polynomial Constraint Solving ⋮ ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs ⋮ Automatic Verification of TLA +  Proof Obligations with SMT Solvers ⋮ The TPTP Typed First-Order Form with Arithmetic ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs ⋮ Exact Incremental Analysis of Timed Automata with an SMT-Solver ⋮ Automated Termination in Model Checking Modulo Theories ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Expressing Polymorphic Types in a Many-Sorted Language ⋮ HYST ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ TIP: Tons of Inductive Problems ⋮ Satisfiability Modulo Theories ⋮ Information Flow in Object-Oriented Software ⋮ SMTtoTPTP – A Converter for Theorem Proving Formats ⋮ Quantifier-Free Equational Logic and Prime Implicate Generation ⋮ Beagle – A Hierarchic Superposition Theorem Prover ⋮ Extensional Crisis and Proving Identity ⋮ Conflict Resolution ⋮ TIP: Tools for Inductive Provers ⋮ Semantic subtyping with an SMT solver ⋮ Unnamed Item ⋮ Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving ⋮ Computer Aided Verification ⋮ Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions ⋮ Playing in the grey area of proofs ⋮ Admissibility in Probabilistic Argumentation ⋮ Two Decades of Maude ⋮ Horn Clause Solvers for Program Verification ⋮ Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings ⋮ SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers ⋮ Matching Multiplications in Bit-Vector Formulas ⋮ Solving Nonlinear Integer Arithmetic with MCSAT ⋮ Partitioned Memory Models for Program Analysis ⋮ Coming to terms with quantified reasoning ⋮ LOIS: syntax and semantics ⋮ Practical SMT-based type error localization ⋮ SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME ⋮ Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools ⋮ HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier ⋮ Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories ⋮ Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1 ⋮ Counterexample-Guided Model Synthesis ⋮ Para-Disagreement Logics and Their Implementation Through Embedding in Coq and SMT ⋮ Modular reasoning about heap paths via effectively propositional formulas ⋮ The Strategy Challenge in SMT Solving ⋮ Unnamed Item ⋮ dReal: An SMT Solver for Nonlinear Theories over the Reals ⋮ bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR ⋮ Natural Domain SMT: A Preliminary Assessment ⋮ Light-Weight SMT-based Model Checking ⋮ Automated Testing and Debugging of SAT and QBF Solvers ⋮ A System for Solving Constraint Satisfaction Problems with SMT ⋮ A Slice-Based Decision Procedure for Type-Based Partial Orders ⋮ Unnamed Item ⋮ Complexity and Algorithms for Monomial and Clausal Predicate Abstraction ⋮ A Progressive Simplifier for Satisfiability Modulo Theories ⋮ Fast and Flexible Difference Constraint Propagation for DPLL(T) ⋮ Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic ⋮ Handling Polymorphism in Automated Deduction ⋮ Towards Modular Algebraic Specifications for Pointer Programs: A Case Study ⋮ Extending Sledgehammer with SMT Solvers ⋮ Heaps and Data Structures: A Challenge for Automated Provers ⋮ Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem ⋮ Dafny: An Automatic Program Verifier for Functional Correctness ⋮ A Logic-Based Framework Leveraging Neural Networks for Studying the Evolution of Neurological Disorders ⋮ Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints ⋮ Ground Interpolation for the Theory of Equality ⋮ Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis ⋮ Unnamed Item ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers ⋮ Model Finding for Recursive Functions in SMT ⋮ Race Against the Teens – Benchmarking Mechanized Math on Pre-university Problems ⋮ Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams ⋮ Finding Finite Models in Multi-sorted First-Order Logic ⋮ Validating QBF Validity in HOL4 ⋮ Building Bridges between Symbolic Computation and Satisfiability Checking ⋮ Loop Analysis by Quantification over Iterations ⋮ Petri Net Synthesis for Restricted Classes of Nets ⋮ Quantitative Abstractions for Collective Adaptive Systems ⋮ A Survey of Satisfiability Modulo Theory ⋮ A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ Goal-Directed Invariant Synthesis for Model Checking Modulo Theories ⋮ Thousands of Geometric Problems for Geometric Theorem Provers (TGTP) ⋮ Automated Reasoning ⋮ Using simplex method in verifying software safety ⋮ Computer Aided Verification ⋮ Definability of Accelerated Relations in a Theory of Arrays and Its Applications ⋮ Term Rewriting with Logical Constraints ⋮ Certified Roundoff Error Bounds Using Semidefinite Programming ⋮ Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic ⋮ E-matching for Fun and Profit ⋮ CC(X): Semantic Combination of Congruence Closure with Solvable Theories ⋮ Unifying type checking and property checking for low-level code ⋮ The SDEval benchmarking toolkit

This page was built for software: SMT-LIB