Finite model finding in satisfiability modulo theories

2013 ◽  
Author(s):  
Andrew Joseph Reynolds
Keyword(s):  
Satisfiability Modulo Theories ◽  
Finite Model ◽  
Model Finding

scholarly journals Constraint solving for finite model finding in SMT solvers

2017 ◽  
Vol 17 (4) ◽  
pp. 516-558
Author(s):  
ANDREW REYNOLDS ◽  
CESARE TINELLI ◽  
CLARK BARRETT
Keyword(s):  
Automated Reasoning ◽  
State Of The Art ◽  
Satisfiability Modulo Theories ◽  
Constraint Solving ◽  
Automated Verification ◽  
Finite Model ◽  
Cardinality Constraints ◽  
On Demand ◽  
Smt Solvers ◽  
Model Finding

AbstractSatisfiability modulo theories (SMT) solvers have been used successfully as reasoning engines for automated verification and other applications based on automated reasoning. Current techniques for dealing with quantified formulas in SMT are generally incomplete, forcing SMT solvers to report “unknown” when they fail to prove the unsatisfiability of a formula with quantifiers. This inability to return counter models limits their usefulness in applications that produce queries involving quantified formulas. In this paper, we reduce these limitations by integrating finite model finding techniques based on constraint solving into the architecture used by modern SMT solvers. This approach is made possible by a novel solver for cardinality constraints, as well as techniques for on-demand instantiation of quantified formulas. Experiments show that our approach is competitive with the state of the art in SMT, and orthogonal to approaches in automated theorem proving.

scholarly journals Towards Smarter MACE-style Model Finders

10.29007/w42s ◽  
2018 ◽  
Author(s):  
Mikolas Janota ◽  
Martin Suda
Keyword(s):  
Learning Algorithm ◽  
Satisfiability Modulo Theories ◽  
Finite Model ◽  
Machine Learning Algorithm ◽  
Model Property ◽  
Abstraction Refinement ◽  
Finite Model Property ◽  
Quantified Boolean Formulas ◽  
Boolean Formulas ◽  
The Right

Finite model finders represent a powerful tool for deciding problems with the finite model property, such as the Bernays-Sch ̈onfinkel fragment (EPR). Further, finite model finders provide useful information for counter-satisfiable conjectures. The paper investigates several novel techniques in a finite model-finder based on the translation to SAT, referred to as the MACE-style approach. The approach we propose is driven by counterexample abstraction refinement (CEGAR), which has proven to be a powerful tool in the context of quantifiers in satisfiability modulo theories (SMT) and quantified Boolean formulas (QBF).One weakness of CEGAR-based approaches is that certain amount of luck is required in order to guess the right model, because the solver always operates on incomplete information about the formula. To tackle this issue, we propose to enhance the model finder with a machine learning algorithm to improve the likelihood that the right model is encountered. The implemented prototype based on the presented ideas shows highly promising results.

scholarly journals Finite Model Finding in SMT

2013 ◽  
pp. 640-655 ◽  
Author(s):  
Andrew Reynolds ◽  
Cesare Tinelli ◽  
Amit Goel ◽  
Sava Krstić
Keyword(s):  
Finite Model ◽  
Model Finding

Quantifier Instantiation Techniques for Finite Model Finding in SMT

2013 ◽  
pp. 377-391 ◽  
Author(s):  
Andrew Reynolds ◽  
Cesare Tinelli ◽  
Amit Goel ◽  
Sava Krstić ◽  
Morgan Deters ◽  
...  
Keyword(s):  
Finite Model ◽  
Model Finding ◽  
Quantifier Instantiation

scholarly journals Revisiting Question Answering in Vampire

10.29007/fjc4 ◽  
2018 ◽  
Author(s):  
Giles Reger
Keyword(s):  
Question Answering ◽  
Theorem Prover ◽  
Finite Model ◽  
Future Directions ◽  
Model Finding

Question answering is the process of taking a conjecture existentially quantified at the outer- most level and providing one or more instantiations of the quantified variable(s) as a form of an answer to the implied question. For example, given the axioms p(a) and f(a)=a the question ?[X] : p(f(X)) could return the answer X=a. This paper reviews the question answering prob- lem focussing on how it is tackled within the VAMPIRE theorem prover. It covers how VAMPIRE extracts single answers, multiple answers, disjunctive answers, and answers involving theories such as arithmetic. The paper finishes by considering possible future directions, such as integration with finite model finding.

Finite Model Theory

1995 ◽  
Author(s):  
Heinz-Dieter Ebbinghaus ◽  
Jörg Flum
Keyword(s):  
Model Theory ◽  
Finite Model ◽  
Finite Model Theory

Engineering Theories with Z3

10.29007/x7b4 ◽  
2018 ◽  
Author(s):  
Nikolaj Bjorner
Keyword(s):  
Satisfiability Modulo Theories ◽  
Smt Solver ◽  
Testing Tools ◽  
Software And Hardware ◽  
Design And Testing

Modern Satisfiability Modulo Theories (SMT)solvers are fundamental to many programanalysis, verification, design and testing tools. They are a goodfit for the domain of software and hardware engineering becausethey support many domains that are commonly used by the tools.The meaning of domains are captured by theories that can beaxiomatized or supported by efficient <i>theory solvers</i>.Nevertheless, not all domains are handled by all solvers andmany domains and theories will never be native to any solver.We here explore different theories that extend MicrosoftResearch's SMT solver Z3's basicsupport. Some can be directly encoded or axiomatized,others make use of user theory plug-ins.Plug-ins are a powerful way for tools to supply their custom domains.

scholarly journals A spatio-temporal specification language and its completeness & decidability

2020 ◽  
Vol 9 (1) ◽  
Author(s):  
Tengfei Li ◽  
Jing Liu ◽  
Haiying Sun ◽  
Xiang Chen ◽  
Lipeng Zhang ◽  
...  
Keyword(s):  
Intelligent Transportation System ◽  
Cyber Physical Systems ◽  
Specification Language ◽  
Finite Model ◽  
Critical Systems ◽  
Physical Systems ◽  
Spatial Objects ◽  
Temporal Properties ◽  
Spatio Temporal ◽  
Temporal Specification

AbstractIn the past few years, significant progress has been made on spatio-temporal cyber-physical systems in achieving spatio-temporal properties on several long-standing tasks. With the broader specification of spatio-temporal properties on various applications, the concerns over their spatio-temporal logics have been raised in public, especially after the widely reported safety-critical systems involving self-driving cars, intelligent transportation system, image processing. In this paper, we present a spatio-temporal specification language, STSL PC, by combining Signal Temporal Logic (STL) with a spatial logic S4 u, to characterize spatio-temporal dynamic behaviors of cyber-physical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatio-temporal traces over real valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL PC combines the power of temporal modalities and spatial operators, and enjoys important properties such as finite model property. We provide a Hilbert-style axiomatization for the proposed STSL PC and prove the soundness and completeness by the spatio-temporal extension of maximal consistent set and canonical model. Further, we demonstrate the decidability of STSL PC and analyze the complexity of STSL PC. Besides, we generalize STSL to the evolution of spatial objects over time, called STSL OC, and provide the proof of its axiomatization system and decidability.

Sign in / Sign up

Export Citation Format

Share Document