Solving quantified linear arithmetic by counterexample-guided instantiation
type: Item
instance of: scholarly article
title: Solving quantified linear arithmetic by counterexample-guided instantiation
zbMATH Open document ID: 1377.68138
author: Andrew Reynolds
author: Tim King
author: Viktor Kuncak
published in: Formal Methods in System Design
publication date: 2018-01-08T00:00:00Z
full work available at URL: http://infoscience.epfl.ch/record/255788
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6823093
zbMATH Keywords: satisfiability modulo theories
zbMATH Keywords: quantifier elimination
zbMATH Keywords: linear arithmetic
zbMATH Keywords: quantifier instantiation
describes a project that uses: SMT-LIB
describes a project that uses: SIMPLIFY
describes a project that uses: RAReQS
describes a project that uses: Mjollnir
describes a project that uses: Spacer
describes a project that uses: Orbital library
describes a project that uses: TPTP
describes a project that uses: Yices
describes a project that uses: z3
describes a project that uses: SMTtoTPTP
MaRDI profile type: Publication
OpenAlex ID: W2744775619
Wikidata QID: Q124817119
cites work: Scaling Enumerative Program Synthesis via Divide and Conquer
cites work: A complete axiomatization of a theory with feature and arity constraints
cites work: Deciding local theory extensions via E-matching
cites work: Monadic second-order logic on tree-like structures
cites work: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
cites work: SMTtoTPTP – A Converter for Theorem Proving Formats
cites work: The complexity of logical theories
cites work: A constraint-based approach to solving games on infinite graphs
cites work: Linear Quantifier Elimination as an Abstract Decision Procedure
cites work: Equational formulae with membership constraints
cites work: Q5674430
cites work: Efficient E-Matching for SMT Solvers
cites work: Simplify: a theorem prover for program checking
cites work: A decision procedure for term algebras with queues
cites work: Applying Linear Quantifier Elimination
cites work: Automated Discovery of Simulation Between Programs
cites work: The first order properties of products of algebraic systems
cites work: The computational complexity of logical theories
cites work: Computer Science Logic
cites work: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
cites work: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
cites work: Q4003410
cites work: Incremental Instance Generation in Local Reasoning
cites work: Solving QBF with Counterexample Guided Refinement
cites work: SMT-based model checking for recursive programs
cites work: Theory of computation.
cites work: Q4813414
cites work: Weakest Precondition Synthesis for Compiler Optimizations
cites work: Automatic modular abstractions for linear constraints
cites work: On direct products of theories
cites work: Linear Quantifier Elimination
cites work: Real World Verification
cites work: Presburger arithmetic with bounded quantifier alternation
cites work: Playing with AVATAR
cites work: Counterexample-guided quantifier instantiation for synthesis in SMT
cites work: Verification and synthesis using real quantifier elimination
cites work: The CADE-14 ATP system competition
cites work: Q4226937
cites work: Efficiently solving quantified bit-vector formulas
DOI: 10.1007/S10703-017-0290-Y
description: scientific article; zbMATH DE number 6823093