scholarly journals Politeness for the Theory of Algebraic Datatypes (Extended Abstract)

2021 ◽  
Author(s):  
Ying Sheng ◽  
Yoni Zohar ◽  
Christophe Ringeissen ◽  
Jane Lange ◽  
Pascal Fontaine ◽  
...  
Keyword(s):  
Automated Reasoning ◽  
Satisfiability Modulo Theories ◽  
Combination Method ◽  
Smt Solvers ◽  
Natural Notion

Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness.

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 Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches

2021 ◽  
pp. 1-31
Author(s):  
YULIYA LIERLER
Keyword(s):  
Automated Reasoning ◽  
Hybrid Approach ◽  
Answer Set Programming ◽  
Satisfiability Modulo Theories ◽  
Declarative Programming ◽  
Scheduling Problems ◽  
New Horizons ◽  
Research Areas ◽  
Constraint Processing ◽  
Answer Set

Abstract Constraint answer set programming or CASP, for short, is a hybrid approach in automated reasoning putting together the advances of distinct research areas such as answer set programming, constraint processing, and satisfiability modulo theories. CASP demonstrates promising results, including the development of a multitude of solvers: acsolver, clingcon, ezcsp, idp, inca, dingo, mingo, aspmt2smt, clingo[l,dl], and ezsmt. It opens new horizons for declarative programming applications such as solving complex train scheduling problems. Systems designed to find solutions to constraint answer set programs can be grouped according to their construction into, what we call, integrational or translational approaches. The focus of this paper is an overview of the key ingredients of the design of constraint answer set solvers drawing distinctions and parallels between integrational and translational approaches. The paper also provides a glimpse at the kind of programs its users develop by utilizing a CASP encoding of Traveling Salesman problem for illustration. In addition, we place the CASP technology on the map among its automated reasoning peers as well as discuss future possibilities for the development of CASP.

scholarly journals JavaSMT 3: Interacting with SMT Solvers in Java

2021 ◽  
pp. 195-208
Author(s):  
Daniel Baier ◽  
Dirk Beyer ◽  
Karlheinz Friedberger
Keyword(s):  
Programming Languages ◽  
Satisfiability Modulo Theories ◽  
Performance Characteristics ◽  
Enabling Technology ◽  
Smt Solvers ◽  
Computer Aided ◽  
And Performance ◽  
Lock In Effect ◽  
Lock In ◽  
Update Process

AbstractSatisfiability Modulo Theories (SMT) is an enabling technology with many applications, especially in computer-aided verification. Due to advances in research and strong demand for solvers, there are many SMT solvers available. Since different implementations have different strengths, it is often desirable to be able to substitute one solver by another. Unfortunately, the solvers have vastly different APIs and it is not easy to switch to a different solver (lock-in effect). To tackle this problem, we developed JavaSMT, which is a solver-independent framework that unifies the API for using a set of SMT solvers. This paper describes version 3 of JavaSMT, which now supports eight SMT solvers and offers a simpler build and update process. Our feature comparisons and experiments show that different SMT solvers significantly differ in terms of feature support and performance characteristics. A unifying Java API for SMT solvers is important to make the SMT technology accessible for software developers. Similar APIs exist for other programming languages.

Functional verification of cyber-physical systems containing machine-learnt components

2021 ◽  
Vol 0 (0) ◽  
Author(s):  
Farzaneh Moradkhani ◽  
Martin Fränzle
Keyword(s):  
Neural Network ◽  
Machine Learning ◽  
Neural Networks ◽  
Cyber Physical Systems ◽  
Satisfiability Modulo Theories ◽  
Activation Functions ◽  
Physical Systems ◽  
Smt Solvers ◽  
Non Linear ◽  
Artificial Neural

Abstract Functional architectures of cyber-physical systems increasingly comprise components that are generated by training and machine learning rather than by more traditional engineering approaches, as necessary in safety-critical application domains, poses various unsolved challenges. Commonly used computational structures underlying machine learning, like deep neural networks, still lack scalable automatic verification support. Due to size, non-linearity, and non-convexity, neural network verification is a challenge to state-of-art Mixed Integer linear programming (MILP) solvers and satisfiability modulo theories (SMT) solvers [2], [3]. In this research, we focus on artificial neural network with activation functions beyond the Rectified Linear Unit (ReLU). We are thus leaving the area of piecewise linear function supported by the majority of SMT solvers and specialized solvers for Artificial Neural Networks (ANNs), the successful like Reluplex solver [1]. A major part of this research is using the SMT solver iSAT [4] which aims at solving complex Boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and therefore is suitable to verify the safety properties of a specific kind of neural network known as Multi-Layer Perceptron (MLP) which contain non-linear activation functions.

scholarly journals Modular strategic SMT solving with SMT-RAT

2018 ◽  
Vol 10 (1) ◽  
pp. 5-25 ◽  
Author(s):  
Gereon Kremer ◽  
Erika Ábrahám
Keyword(s):  
Satisfiability Modulo Theories ◽  
Integer Arithmetic ◽  
Smt Solving ◽  
Smt Solvers

Abstract In this paper we present the latest developments in SMT-RAT, a tool for the automated check of quantifier-free real and integer arithmetic formulas for satisfiability. As a distinguishing feature, SMT-RAT provides a set of solving modules and supports their strategic combination. We describe our CArL library for arithmetic computations, the available modules implemented on top of CArL, and how modules can be combined to satisfiability-modulo-theories (SMT) solvers. Besides the traditional SMT approach, some new modules support also the recently proposed and highly promising model-constructing satisfiability calculus approach.

scholarly journals Efficient and Complete FD-solving for extended array constraints

2017 ◽  
Author(s):  
Quentin Plazar ◽  
Mathieu Acher ◽  
Sébastien Bardin ◽  
Arnaud Gotlieb
Keyword(s):  
Data Structures ◽  
Automated Reasoning ◽  
Software Verification ◽  
Finite Domain ◽  
Local Consistency ◽  
Smt Solvers

Array constraints are essential for handling data structures in automated reasoning and software verification. Unfortunately, the use of a typical finite domain (FD) solver based on local consistency-based filtering has strong limitations when constraints on indexes are combined with constraints on array elements and size. This paper proposes an efficient and complete FD-solving technique for extended constraints over (possibly unbounded) arrays. We describe a simple but particularly powerful transformation for building an equisatisfiable formula that can be efficiently solved using standard FD reasoning over arrays, even in the unbounded case. Experiments show that the proposed solver significantly outperforms FD solvers, and successfully competes with the best SMT-solvers.

scholarly journals Politeness and Stable Infiniteness: Stronger Together

2021 ◽  
pp. 148-165
Author(s):  
Ying Sheng ◽  
Yoni Zohar ◽  
Christophe Ringeissen ◽  
Andrew Reynolds ◽  
Clark Barrett ◽  
...  
Keyword(s):  
Preliminary Evidence ◽  
Satisfiability Modulo Theories ◽  
The Other ◽  
Combination Method ◽  
Improve Performance ◽  
Worst Case ◽  
Smart Contract ◽  
Shared Variables ◽  
Speed Up ◽  
Time Required

AbstractWe make two contributions to the study of polite combination in satisfiability modulo theories. The first is a separation between politeness and strong politeness, by presenting a polite theory that is not strongly polite. This result shows that proving strong politeness (which is often harder than proving politeness) is sometimes needed in order to use polite combination. The second contribution is an optimization to the polite combination method, obtained by borrowing from the Nelson-Oppen method. The Nelson-Oppen method is based on guessing arrangements over shared variables. In contrast, polite combination requires an arrangement over all variables of the shared sorts. We show that when using polite combination, if the other theory is stably infinite with respect to a shared sort, only the shared variables of that sort need be considered in arrangements, as in the Nelson-Oppen method. The time required to reason about arrangements is exponential in the worst case, so reducing the number of variables considered has the potential to improve performance significantly. We show preliminary evidence for this by demonstrating a speed-up on a smart contract verification benchmark.

scholarly journals Personnel Scheduling as Satisfiability Modulo Theories

2017 ◽  
Author(s):  
Christoph Erkinger ◽  
Nysret Musliu
Keyword(s):  
Real Life ◽  
Satisfiability Modulo Theories ◽  
Compact Representation ◽  
Workforce Scheduling ◽  
Exact Methods ◽  
First Order ◽  
Smt Solvers ◽  
Benchmark Instances ◽  
Modeling Techniques ◽  
New Formulation

Rotating workforce scheduling (RWS) is an important real-life personnel rostering problem that appears in a large number of different business areas. In this paper, we propose a new exact approach to RWS that exploits the recent advances on Satisfiability Modulo Theories (SMT). While solving can be automated by using a number of so-called SMT-solvers, the most challenging task is to find an efficient formulation of the problem in first-order logic. We propose two new modeling techniques for RWS that encode the problem using formulas over different background theories. The first encoding provides an elegant approach based on linear integer arithmetic. Furthermore, we developed a new formulation based on bitvectors in order to achieve a more compact representation of the constraints and a reduced number of variables. These two modeling approaches were experimentally evaluated on benchmark instances from literature using different state-of-the-art SMT-solvers. Compared to other exact methods, the results of this approach showed an important improvement in the number of found solutions.

scholarly journals Towards Strong Higher-Order Automation for Fast Interactive Verification

10.29007/3ngx ◽  
2018 ◽  
Author(s):  
Jasmin Christian Blanchette ◽  
Pascal Fontaine ◽  
Stephan Schulz ◽  
Uwe Waldmann
Keyword(s):  
Research Council ◽  
Higher Order ◽  
Point Of View ◽  
Satisfiability Modulo Theories ◽  
Proof Assistants ◽  
First Order ◽  
The Core ◽  
Proof Rules ◽  
Level Of Automation ◽  
Smt Solvers

We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. From this point of view, it seems desirable to enrich superposition and SMT (satisfiability modulo theories) with higher-order reasoning in a careful manner, to preserve their good properties. Representative benchmarks from the interactive community can guide the design of proof rules and strategies. With higher-order superposition and higher-order SMT in place, highly automatic provers could be built on modern superposition provers and SMT solvers, following a stratified architecture reminiscent of that of modern SMT solvers. We hope that these provers will bring a new level of automation to the users of proof assistants. These challenges and work plan are at the core of the Matryoshka project, funded for five years by the European Research Council. We encourage researchers motivated by the same goals to get in touch with us, subscribe to our mailing list, and join forces.

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.

Sign in / Sign up

Export Citation Format

Share Document