scholarly journals Conflicts, Models and Heuristics for Quantifier Instantiation in SMT

10.29007/jmd3 ◽  
2018 ◽  
Author(s):  
Andrew Reynolds
Keyword(s):  
Formal Methods ◽  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Software Verification ◽  
Satisfiability Modulo Theories ◽  
Smt Solvers ◽  
Recent Advances ◽  
Common Technique ◽  
Quantifier Instantiation ◽  
Future Work

Satisfiability Modulo Theories (SMT) solvers have emerged as prominent tools in formal methods applications. While originally targeted towards quantifier-free inputs, SMT solvers are now often used for handling quantified formulas in automated theorem proving and software verification applications. The most common technique for handling quantified formulas in modern SMT solvers in quantifier instantiation. This paper gives an overview of recent advances in quantifier instantiation in SMT. In addition to the well-known technique known as E-matching, we discuss the use of conflicts and models for accelerating the search for (un)satisfiably. We further mention new instantiation-based techniques that are specialized to background theories such as linear real and integer arithmetic, and future work in this direction.

scholarly journals νZ - Maximal Satisfaction with Z3

10.29007/jmxj ◽  
2018 ◽  
Author(s):  
Nikolaj Bjorner ◽  
Anh-Dung Phan
Keyword(s):  
Theorem Proving ◽  
Optimization Problems ◽  
Linear Optimization ◽  
Satisfiability Modulo Theories ◽  
Objective Functions ◽  
Smt Solver ◽  
Smt Solvers ◽  
Free Variables ◽  
Linear Optimization Problems ◽  
Pareto Fronts

Satisfiability Modulo Theories, SMT, solvers are used inmany applications. These applications benefit from thepower of tuned and scalable theorem proving technologiesfor supported logics and specialized theory solvers.SMT solvers are primarily used to determine whether formulas are satisfiable.Furthermore, when formulas are satisfiable, many applications need modelsthat assign values to free variables.Yet, in many cases arbitrary assignments are insufficient,and what is really needed is an <i>optimal</i> assignmentwith respect to objective functions. So far, users of Z3,an SMT solver from Microsoft Research, build custom loopsto achieve objective values. This is no longer necessarywith νZ (new-Z, or max-Z), an extension within Z3 that letsusers formulate objective functions directly with Z3. Under the hood there is aportfolio of approaches for solving linear optimization problems overSMT formulas, MaxSMT, and their combinations. Objective functions are combinedas either Pareto fronts, lexicographically, or each objective is optimized independently.

scholarly journals AVATAR Modulo Theories

10.29007/k6tp ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Nikolaj Bjorner ◽  
Martin Suda ◽  
Andrei Voronkov
Keyword(s):  
Theorem Proving ◽  
Satisfiability Modulo Theories ◽  
Theorem Prover ◽  
Ground Theory ◽  
Smt Solver ◽  
First Order ◽  
Proof Search ◽  
Smt Solvers ◽  
Sat Solver ◽  
A New Technique

This paper introduces a new technique for reasoning with quantifiers and theories. Traditionally, first-order theorem provers (ATPs) are well suited to reasoning with first-order problems containing many quantifiers and satisfiability modulo theories (SMT) solvers are well suited to reasoning with first-order problems in ground theories such as arithmetic. A recent development in first-order theorem proving has been the AVATAR architecture which uses a SAT solver to guide proof search based on a propositional abstraction of the first-order clause space. The approach turns a single proof search into a sequence of proof searches on (much) smaller sub-problems. This work extends the AVATAR approach to use a SMT solver in place of the SAT solver, with the effect that the first-order solver only needs to consider ground-theory-consistent sub-problems. The new architecture has been implemented using the Vampire theorem prover and Z3 SMT solver. Our experimental results, and the results of recent competitions, show that such a combination can be highly effective.

The 10th IJCAR automated theorem proving system competition – CASC-J10

2021 ◽  
pp. 1-15
Author(s):  
Geoff Sutcliffe
Keyword(s):  
Theorem Proving ◽  
Classical Logic ◽  
Automated Theorem Proving ◽  
Fully Automatic

The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-J10 was the twenty-fifth competition in the CASC series. Twenty-four ATP systems and system variants competed in the various competition divisions. This paper presents an outline of the competition design, and a commentated summary of the results.

Retrieval System and Dynamic Algorithm Looking for Axioms of Notions Defined by Programs

1993 ◽  
Vol 19 (3-4) ◽  
pp. 275-301
Author(s):  
Andrzej Biela
Keyword(s):  
Theorem Proving ◽  
Dynamic Process ◽  
Functional Equations ◽  
Automated Theorem Proving ◽  
Retrieval System ◽  
Formal System ◽  
Dynamic Algorithm ◽  
Algorithmic Logic ◽  
Correctness Of Programs

In this paper we shall introduce a formal system of algorithmic logic which enables us to formulate some problems connected with a retrieval system which provides a comprehensive tool in automated theorem proving of theorems consisting of programs, procedures and functions. The procedures and functions may occur in considered theorems while the program of the above mentioned system is being executed. We can get an answer whether some relations defined by programs hold and we can prove functional equations in a dynamic way by looking for a special set of axioms /assumptions/ during the execution of system. We formulate RS-algorithm which enables us to construct the set of axioms for proving some properties of functions and relations defined by programs. By RS-algorithm we get the dynamic process of proving functional equations and we can answer the question whether some relations defined by programs hold. It enables us to solve some problems concerning the correctness of programs. This system can be used for giving an expert appraisement. We shall provide the major structures and a sketch of an implementation of the above formal system.

scholarly journals A Driver’s License Test for Driverless Vehicles

2017 ◽  
Vol 139 (12) ◽  
pp. S13-S16 ◽  
Author(s):  
Houssam Abbas ◽  
Matthew E. O’Kelly ◽  
Alena Rodionova ◽  
Rahul Mangharam
Keyword(s):  
Formal Methods ◽  
Theorem Proving ◽  
Autonomous Vehicle ◽  
Reachability Analysis ◽  
Initial State ◽  
Left Turn ◽  
Interactive Technique ◽  
Driver's License

This article elaborates the approaches that can be used to verify an autonomous vehicle (AV) before giving it a driver’s license. Formal methods applied to the problem of AV verification include theorem proving, reachability analysis, synthesis, and maneuver design. Theorem proving is an interactive technique in which the computer is largely responsible for demonstrating that the model satisfies the specification, with occasional help from the user. The latter provides lemmas and axioms that the tool leverages to advance the proof towards its conclusion. Reachability analysis is used to verify the operation of the AV during navigation. This provides an extension of onboard diagnostics to whole-AV operation, where the diagnosis does not concern one component’s requirements, but the safety of the entire AV. Another approach is to design correct-by-construction controllers from preverified maneuvers. The basic idea is that one builds a library of maneuvers, such as Left-Turn and Right-Turn, and verifies that the car can perform these maneuvers from any initial state.

Verifying B proof rules using deep embedding and automated theorem proving

2013 ◽  
Vol 14 (1) ◽  
pp. 101-119 ◽  
Author(s):  
Mélanie Jacquel ◽  
Karim Berkani ◽  
David Delahaye ◽  
Catherine Dubois
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Proof Rules ◽  
Deep Embedding
Sign in / Sign up

Export Citation Format

Share Document