logo Région Lorraine

Meeting detail

Fifth SMArT meeting -- 13-14 November 2014 -- Loria, Nancy

JAIST-Loria Workshop 2014 on SMT

Workshop on the occasion of the visit of Mizuhito Ogawa (JAIST).
This meeting takes place in the context of the JAIST-LORIA Workshop 2014 and benefits from its sponsors.

Participants

Federico Dobal, Pascal Fontaine, Stephan Merz, Thomas Sturm.
Invited: Erika Abraham, Florian Corzilius, Maximilian Jaroschek, Gereon Kremer, Mizuhito Ogawa, Karsten Scheibler

Program

Thursday, November 13 (B011)

09:30-10:00 : welcome
10:00-11:00 : Pascal Fontaine. SMT, Nelson-Oppen and arithmetic (informal talk and discussions)
11:00-12:00 : open seminar: Thomas Sturm. Effective Quantifier Elimination and Decision - Theory, Implementations, Applications, Perspectives.

12:00-14:00 : Lunch

14:00-15:00 : Florian Corzilius. Introducing SMT-Rat (informal talk and discussions)
15:00-17:00 : Technical discussions: SMT-Rat, Redlog, RaSAT, iSAT

Dinner in Nancy

Friday, November 14 (A006)

09:00-10:00 : Maximilian Jaroschek. The SMArT project (informal talk and discussions)
10:00-11:00 : open seminar: Mizuhito Ogawa. raSAT : SMT solver for nonlinear inequality over reals
11:00-12:00 : Karsten Scheibler. Introducing iSAT (informal talk and discussions)

12:00-14:00 : Lunch

14:00-15:00 : Discussion: interval constraint propagation techniques
15:00-17:00 : Technical discussions and work planning

Thomas Sturm. Effective Quantifier Elimination and Decision - Theory, Implementations, Applications, Perspectives (abstract)

Effective quantifier elimination procedures for first-order theories provide a powerful tool for generically solving a wide range of problems based on logical specifications. In contrast to general first-order provers, quantifier elimination procedures are based on a fixed set of admissible logical symbols with an implicitly fixed semantics. This admits the use of sub-algorithms from symbolic computation. We are going to focus on quantifier elimination for the reals and its applications giving examples from geometry, verification, and SMT solving. Beyond quantifier elimination we are going to sketch work-in-progress on an incomplete decision procedure for the existential fragment of the reals, which has been successfully applied to the analysis of reaction systems in chemistry and in the life sciences. We conclude with an overview on quantifier-eliminable theories that have been realized in our open-source computer logic software Redlog (www.redlog.eu).

Florian Corzilius. Introducing SMT-Rat (abstract)

SMT-RAT is an open source C++ library consisting of a collection of SMT-compliant implementations of methods for solving non-linear real and integer arithmetic (NRA/NIA) formulas, we refer to as modules. These modules can be combined to (1) a theory solver in order to extend the supported logics of an existing SMT solver by NRA/NIA or (2) an SMT solver for NRA/NIA. The latter is especially intended to be a testing environment for the development of SMT-compliant implementations of further methods tackling NRA/NIA. Here, the developer only needs to implement the given interfaces of an SMT-RAT module and does not need to care about parsing input files, transforming formulas to conjunctive normal form or embedding a SAT solver in order to solve the Boolean skeleton of the given formula.

Maximilian Jaroschek. The SMArT Project (abstract)

The SMArT project is a collaboration between Inria, Loria, Systerel and the Max-Planck-Institut für Informatik. In this talk I give an overview of the project and its goals as well as the status quo of the current research. In particular, ideas on the problem of finding minimal infeasible subsets in real quantifier elimination using cylindrical algebraic decomposition and virtual substitution will be presented.

Mizuhito Ogawa. raSAT : SMT solver for nonlinear inequality over reals (abstract)

We present a simple iterative approximation refinement, called raSAT loop, which is an extension of the standard ICP (Interval Constraint Propagation) with testing. Two approximation schemes consist of interval arithmetic (over-approximation) and testing (under-approximation), to accelerate SAT detection. If both fails, input intervals are refined by decomposition. It is implemented as an SMT solver raSAT for nonlinear inequality over reals. We also investigate several heuristic measures to choose a variable and a box for refinement, targeting on SAT detection, e.g., SAT-likelyhood, sensitivity, and the number of unsolved atomic polynomial constraints. They are compared on Zankl and Meti-tarski benchmarks from QF_NRA category of SMT-LIB. They are also evaluated by comparing with Z3 4.3 and iSAT3. We also show a simple modification to handle mixed integers, and experiments on AProVE benchmark from QF_NIA category of SMT-LIB.