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 Deductive Verification of Floating-Point Java Programs in KeY

2021 ◽  
pp. 242-261
Author(s):  
Rosa Abbasi ◽  
Jonas Schiffl ◽  
Eva Darulova ◽  
Mattias Ulbrich ◽  
Wolfgang Ahrendt
Keyword(s):  
Programming Language ◽  
Floating Point ◽  
Deductive Verification ◽  
Java Programming ◽  
Special Values ◽  
Floating Point Arithmetic ◽  
Smt Solvers ◽  
Java Programs ◽  
Transcendental Functions ◽  
Point Arithmetic

AbstractDeductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due to rounding as well as the presence of the special values infinity and ‘Not a Number’ (NaN). In this paper, we present the first floating-point support in a deductive verification tool for the Java programming language. Our support in the KeY verifier handles arithmetic via floating-point decision procedures inside SMT solvers and transcendental functions via axiomatization. We evaluate this integration on new benchmarks, and show that this approach is powerful enough to prove the absence of floating-point special values—often a prerequisite for further reasoning about numerical computations—as well as certain functional properties for realistic benchmarks.

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.

Efficient RGB to YCbCr Color Space Conversion for Embedded Application

2014 ◽  
Vol 543-547 ◽  
pp. 2873-2878
Author(s):  
Hui Yong Li ◽  
Hong Xu Jiang ◽  
Ping Zhang ◽  
Han Qing Li ◽  
Qian Cao
Keyword(s):  
Direct Method ◽  
Color Space ◽  
Video Data ◽  
Floating Point ◽  
Portable Devices ◽  
Embedded Processor ◽  
Color Space Conversion ◽  
Ycbcr Color Space ◽  
Original Approach ◽  
General Method

Modern embedded portable devices usually have to deal with large amounts of video data. Due to massive floating-point multiplications, the color space conversion is inefficient on the embedded processor. Considering the characteristics of RGB to YCbCr color space conversion, this paper proposed a strategy for truncated-based LUT Multiplier (T-LUT Multiplier). On this base, an original approach converting RGB to YCbCr is presented which employs the T-LUT Multiplier and the pipeline-based adder. Experimental results demonstrate that the proposed method can obtain maximum operating frequency of 358MHz, 3.5 times faster than the direct method. Furthermore, the power consumption is less than that of the general method approximately by 15%~27%.

scholarly journals Rigorous Roundoff Error Analysis of Probabilistic Floating-Point Computations

2021 ◽  
pp. 626-650
Author(s):  
George Constantinides ◽  
Fredrik Dahlqvist ◽  
Zvonimir Rakamarić ◽  
Rocco Salvia
Keyword(s):  
Random Variables ◽  
Random Variable ◽  
Floating Point ◽  
Roundoff Error ◽  
Smt Solver ◽  
Current State ◽  
Roundoff Errors ◽  
Error Distributions ◽  
Almost All ◽  
Point Arithmetic

AbstractWe present a detailed study of roundoff errors in probabilistic floating-point computations. We derive closed-form expressions for the distribution of roundoff errors associated with a random variable, and we prove that roundoff errors are generally close to being uncorrelated with their generating distribution. Based on these theoretical advances, we propose a model of IEEE floating-point arithmetic for numerical expressions with probabilistic inputs and an algorithm for evaluating this model. Our algorithm provides rigorous bounds to the output and error distributions of arithmetic expressions over random variables, evaluated in the presence of roundoff errors. It keeps track of complex dependencies between random variables using an SMT solver, and is capable of providing sound but tight probabilistic bounds to roundoff errors using symbolic affine arithmetic. We implemented the algorithm in the PAF tool, and evaluated it on FPBench, a standard benchmark suite for the analysis of roundoff errors. Our evaluation shows that PAF computes tighter bounds than current state-of-the-art on almost all benchmarks.

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.

Applying Program Transformations for Deductive Verification of the List Reverse Program

2021 ◽  
Vol 12 (3) ◽  
pp. 127-139
Author(s):  
V. I. Shelekhov ◽  
Keyword(s):  
Program Transformations ◽  
Data Types ◽  
Deductive Verification ◽  
C Language ◽  
Recursive Program ◽  
Smt Solvers ◽  
Source Program ◽  
Predicate Language ◽  
Transformation Methods ◽  
Recursive Data

The program transformation methods to simplify the deductive verification of programs with recursive data types are investigated. The list reversion program is considered as an example. A source program in the C language is translated to the cP functional language which includes no pointers. The resulting program is translated further to the WhyML language to perform deductive verification of the program. The cP language includes the same constructs of the C language except pointers. In the C program, all actions that include pointers are replaced by the equivalent fragments without pointers. These replacement are performed by the special transformations using the results of the program dataflow analysis. Three variants of deductive verification of the transformed list reverse program in the Why3 verification platform with SMT solvers (Z3 4.8.6, CVC3 2.4.1, CVC4 1.7) are performed. First, the recursive WhyML program supplied with specifications was automatically verified successfully using only SMT solvers. Second, the recursive program was translated to the P predicate language. Correctness formulae were constructed for the P program and translated further to the why3 specification language. The formulae proving correctness were easy like the first variant. But correctness formulae for the first and second variants were different. Third, the "imperative" WhyML program that included while loop with additional invariant specifications was verified. The proving was easy but not automatic. So, for deductive verification, recursive program variant appears to be more preferable against imperative program variant.

scholarly journals Syntax-Guided Quantifier Instantiation

2021 ◽  
pp. 145-163
Author(s):  
Aina Niemetz ◽  
Mathias Preiner ◽  
Andrew Reynolds ◽  
Clark Barrett ◽  
Cesare Tinelli
Keyword(s):  
State Of The Art ◽  
Satisfiability Modulo Theories ◽  
Floating Point ◽  
New Approach ◽  
Smt Solver ◽  
Floating Point Arithmetic ◽  
Novel Approach ◽  
Non Linear ◽  
Quantifier Instantiation ◽  
Point Arithmetic

AbstractThis paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntax-guided synthesis (SyGuS) to choose instantiation terms. It targets quantified constraints over background theories such as (non)linear integer, reals and floating-point arithmetic, bit-vectors, and their combinations. Unlike previous approaches for quantifier instantiation in these domains which rely on theory-specific strategies, the new approach can be applied to any (combined) theory, when provided with a grammar for instantiation terms for all sorts in the theory. We implement syntax-guided instantiation in the SMT solver CVC4, leveraging its support for enumerative SyGuS. Our experiments demonstrate the versatility of the approach, showing that it is competitive with or exceeds the performance of state-of-the-art solvers on a range of background theories.

scholarly journals Generative type-aware mutation for testing SMT solvers

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-19
Author(s):  
Jiwon Park ◽  
Dominik Winterer ◽  
Chengyu Zhang ◽  
Zhendong Su
Keyword(s):  
State Of The Art ◽  
The State ◽  
Default Mode ◽  
Smt Solver ◽  
Testing Period ◽  
Smt Solvers

We propose Generative Type-Aware Mutation, an effective approach for testing SMT solvers. The key idea is to realize generation through the mutation of expressions rooted with parametric operators from the SMT-LIB specification. Generative Type-Aware Mutation is a hybrid of mutation-based and grammar-based fuzzing and features an infinite mutation space—overcoming a major limitation of OpFuzz, the state-of-the-art fuzzer for SMT solvers. We have realized Generative Type-Aware Mutation in a practical SMT solver bug hunting tool, TypeFuzz. During our testing period with TypeFuzz, we reported over 237 bugs in the state-of-the-art SMT solvers Z3 and CVC4. Among these, 189 bugs were confirmed and 176 bugs were fixed. Most notably, we found 18 soundness bugs in CVC4’s default mode alone. Several of them were two years latent (7/18). CVC4 has been proved to be a very stable SMT solver and has resisted several fuzzing campaigns.

scholarly journals ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory

2020 ◽  
pp. 525-529 ◽  
Author(s):  
Mikhail R. Gadelha ◽  
Rafael Menezes ◽  
Felipe R. Monteiro ◽  
Lucas C. Cordeiro ◽  
Denis Nicole
Keyword(s):  
Test Generation ◽  
Point Theory ◽  
Floating Point

scholarly journals Sound and Complete Concolic Testing for Higher-order Functions

2021 ◽  
pp. 635-663
Author(s):  
Shu-Hung You ◽  
Robert Bruce Findler ◽  
Christos Dimoulas
Keyword(s):  
Directed Evolution ◽  
Programming Languages ◽  
Canonical Form ◽  
Higher Order ◽  
User Program ◽  
Smt Solver ◽  
Counter Example ◽  
Smt Solvers ◽  
Concolic Testing ◽  
Higher Order Functions

AbstractHigher-order functions have become a staple of modern programming languages. However, such values stymie concolic testers, as the SMT solvers at their hearts are inherently first-order.This paper lays a formal foundations for concolic testing higher-order functional programs. Three ideas enable our results: (i) our tester considers only program inputs in a canonical form; (ii) it collects novel constraints from the evaluation of the canonical inputs to search the space of inputs with partial help from an SMT solver and (iii) it collects constraints from canonical inputs even when they are arguments to concretized calls. We prove that (i) concolic evaluation is sound with respect to concrete evaluation; (ii) modulo concretization and SMT solver incompleteness, the search for a counter-example succeeds if a user program has a bug and (iii) this search amounts to directed evolution of inputs targeting hard-to-reach corners of the program.

Sign in / Sign up

Export Citation Format

Share Document