scholarly journals Experiments on the feasibility of using a floating-point simplex in an SMT solver

10.29007/j7x4 ◽  
2018 ◽  
Author(s):  
Diego Caminha Barbosa de Oliveira ◽  
David Monniaux
Keyword(s):  
Simplex Algorithm ◽  
Decision Procedures ◽  
Linear Constraints ◽  
Decision Problems ◽  
Floating Point ◽  
Protocol Verification ◽  
Smt Solver ◽  
Smt Solvers ◽  
State Of Art ◽  
Floating Point Implementation

SMT solvers use simplex-based decision procedures to solve decision problems whose formulas are quantifier-free and atoms are linear constraints over the rationals. State-of-art SMT solvers use rational (exact) simplex implementations, which have shown good performance for typical software, hardware or protocol verification problems over the years.Yet, most other scientific and technical fields use (inexact) floating-point computations, which are deemed far more efficient than exact ones.It is therefore tempting to use a floating-point simplex implementation inside an SMT solver, though special precautions must be taken to avoid unsoundness.In this work, we describe experimental results, over common benchmarks (SMT-LIB) of the integration of a mature floating-point implementation of the simplex algorithm (GLPK) into an existing SMT solver (OpenSMT).We investigate whether commonly cited reasons for and against the use of floating-point truly apply to real cases from verification problems.

scholarly journals Complete decision procedure for the theory of bounded pointer arithmetic based on quantifier instantiation and SMT

2021 ◽  
Vol 33 (4) ◽  
pp. 177-194
Author(s):  
Rafael Faritovich Sadykov ◽  
Mikhail Usamovich Mandrykin
Keyword(s):  
Program Verification ◽  
Source Code ◽  
Decision Procedures ◽  
C Programs ◽  
Smt Solver ◽  
Smt Solvers ◽  
Relevant Logics ◽  
Soundness And Completeness ◽  
C Program ◽  
Quantifier Instantiation

The process of developing C programs is quite often prone to errors related to the uses of pointer arithmetic and operations on memory addresses. This promotes a need in developing various tools for automated program verification. One of the techniques frequently employed by those tools is invocation of appropriate decision procedures implemented within existing SMT-solvers. But at the same time both the SMT standard and most existing SMT-solvers lack the relevant logics (combinations of logical theories) for directly and precisely modelling the semantics of pointer operations in C. One of the possible ways to support these logics is to implement them in an SMT solver, but this approach can be time-consuming (as requires modifying the solver’s source code), inflexible (introducing any changes to the theory’s signature or semantics can be unreasonably hard) and limited (every solver has to be supported separately). Another way is to design and implement custom quantifier instantiation strategies. These strategies can be then used to translate formulas in the desired theory combinations to formulas in well-supported decidable logics such as QF_UFLIA. In this paper, we present an instantiation procedure for translating formulas in the theory of bounded pointer arithmetic into the QF_UFLIA logic. We formally proved soundness and completeness of our instantiation procedure in Isabelle/HOL. The paper presents an informal description of this proof of the proposed procedure. The theory of bounded pointer arithmetic itself was formulated based on known errors regarding the correct use of pointer arithmetic operations in industrial code as well as the semantics of these operations specified in the C standard. Similar procedure can also be defined for a practically relevant fragment of the theory of bit vectors (monotone propositional combinations of equalities between bitwise expressions). Our approach is sufficient to obtain efficient decision procedures implemented as Isabelle/HOL proof methods for several decidable logical theories used in C program verification by relying on the existing capabilities of well-known SMT solvers, such as Z3 and proof reconstruction capabilities of the Isabelle/HOL proof assistant.

scholarly journals Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers

10.29007/wh99 ◽  
2018 ◽  
Author(s):  
Sylvain Conchon ◽  
Guillaume Melquiond ◽  
Cody Roux ◽  
Mohamed Iguernelala
Keyword(s):  
Point Theory ◽  
Floating Point ◽  
Axiomatic Theory ◽  
Deductive Verification ◽  
Automatic Reasoning ◽  
Smt Solver ◽  
Smt Solvers ◽  
Approximation Errors ◽  
Natural Support ◽  
Original Approach

The treatment of the axiomatic theory of floating-point numbers isout of reach of current SMT solvers, especially when it comes toautomatic reasoning on approximation errors. In this paper, wedescribe a dedicated procedure for such a theory, which provides aninterface akin to the instantiation mechanism of an SMT solver.This procedure is based on the approach of the Gappa tool: itperforms saturation of consequences of the axioms, in order torefine bounds on expressions. In addition to the original approach,bounds are further refined by a constraint solver for lineararithmetic. Combined with the natural support for equalitiesprovided by SMT solvers, our approach improves the treatment ofgoals coming from deductive verification of numeric programs. Wehave implemented it in the Alt-Ergo SMT solver.

scholarly journals Reasoning with Triggers

10.29007/3c1n ◽  
2018 ◽  
Author(s):  
Claire Dross ◽  
Sylvain Conchon ◽  
Johannes Kanig ◽  
Andrei Paskevich
Keyword(s):  
Decision Procedure ◽  
Decision Procedures ◽  
Description Language ◽  
Smt Solver ◽  
First Order ◽  
Smt Solvers ◽  
Precise Sense ◽  
Universal Quantifiers ◽  
Internal Knowledge

SMT solvers can decide the satisfiability of ground formulas modulo a combination ofbuilt-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures.In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate using the theory of arrays, how such proofs can be achieved in our formalism.

scholarly journals Art of Formulating LPs and IPs from Real Life Problems

2013 ◽  
Vol 61 (2) ◽  
pp. 185-191
Author(s):  
Md Hasib Uddin Molla ◽  
M Babul Hasan
Keyword(s):  
Mathematical Model ◽  
Objective Function ◽  
Real Life ◽  
Linear Constraints ◽  
Decision Problems ◽  
System Of Equations ◽  
Present Formulation ◽  
Real Life Problem ◽  
Life Problems ◽  
Life Decision

Formulation of LPs and IPs is a technique to convert real life decision problems into a mathematical model. This model consists of a linear objective function and a set of linear constraints expressed in the form of a system of equations or inequalities. In this paper, we present formulation from real life problem as an art. We discuss formulation through real life example and solve them using computer techniques AMPL and LINDO. DOI: http://dx.doi.org/10.3329/dujs.v61i2.17068 Dhaka Univ. J. Sci. 61(2): 185-191, 2013 (July)

NUMERICAL STABILITY OF ALGORITHMS FOR 2D DELAUNAY TRIANGULATIONS

1995 ◽  
Vol 05 (01n02) ◽  
pp. 193-213 ◽  
Author(s):  
STEVEN FORTUNE
Keyword(s):  
Delaunay Triangulation ◽  
Floating Point ◽  
Worst Case ◽  
Delaunay Triangulations ◽  
Floating Point Arithmetic ◽  
Circular Arcs ◽  
Stability Of Algorithms ◽  
Forming Angle ◽  
Point Arithmetic ◽  
Floating Point Implementation

We consider the correctness of 2-d Delaunay triangulation algorithms implemented using floating-point arithmetic. The α-pseudocircle through points a, b, c consists of three circular arcs connecting ab, bc, and ac, each arc inside the circumcircle of a, b, c and forming angle α with the circumcircle; a triangulation is α-empty if the α-pseudocircle through the vertices of each triangle is empty. We show that a simple Delaunay triangulation algorithm—the flipping algorithm—can be implemented to produce O(n∈)-empty triangulations, where n is the number of point sites and ∈ is the relative error of floating-point arithmetic; its worst-case running time is O(n2). We also discuss floating-point implementation of other 2-d Delaunay triangulation algorithms.

Sign in / Sign up

Export Citation Format

Share Document