| 1. |
|
|
| 2. |
- Cook, Byron, et al.
(författare)
-
Ranking function synthesis for bit-vector relations
- 2013
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 43:1, s. 93-120
-
Tidskriftsartikel (refereegranskat)abstract
- Ranking function synthesis is a key component of modern termination provers for imperative programs. While it is well-known how to generate linear ranking functions for relations over (mathematical) integers or rationals, efficient synthesis of ranking functions for machine-level integers (bit-vectors) is an open problem. This is particularly relevant for the verification of low-level code. We propose several novel algorithms to generate ranking functions for relations over machine integers: a complete method based on a reduction to Presburger arithmetic, and a template-matching approach for predefined classes of ranking functions based on reduction to SAT- and QBF-solving. The utility of our algorithms is demonstrated on examples drawn from Windows device drivers.
|
|
| 3. |
|
|
| 4. |
- Zeljic, Aleksandar, et al.
(författare)
-
Approximations for Model Construction
- 2014
-
Ingår i: Automated Reasoning. - Cham : Springer. - 9783319085869 - 9783319085876 ; , s. 344-359
-
Konferensbidrag (refereegranskat)abstract
- We consider the problem of efficiently computing models for satisfiable constraints, in the presence of complex background theories such as floating-point arithmetic. Model construction has various applications, for instance the automatic generation of test inputs. It is well-known that naive encoding of constraints into simpler theories (for instance, bit-vectors or propositional logic) can lead to a drastic increase in size, and be unsatisfactory in terms of memory and runtime needed for model construction. We define a framework for systematic application of approximations in order to speed up model construction. Our method is more general than previous techniques in the sense that approximations that are neither under- nor over-approximations can be used, and shows promising results in practice.
|
|
| 5. |
- Zeljic, Aleksandar, et al.
(författare)
-
Deciding bit-vector formulas with mcSAT
- 2016
-
Ingår i: Theory and Applications of Satisfiability Testing. - Cham : Springer. - 9783319409696 ; , s. 249-266
-
Konferensbidrag (refereegranskat)
|
|
| 6. |
- Zeljic, Aleksandar, et al.
(författare)
-
Exploring Approximations for Floating-Point Arithmetic using UppSAT
- 2018
-
Ingår i: Automated Reasoning. - Cham : Springer International Publishing. - 9783319942049 - 9783319942056 ; , s. 246-262
-
Konferensbidrag (refereegranskat)abstract
- We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT—an new implementation of a systematic approximation refinement framework as an abstract SMT solver. Provided with an approximation and a decision procedure (implemented in an off-the-shelf SMT solver), UppSAT yields an approximating SMT solver. Additionally, UppSAT includes a library of predefined approximation components which can be combined and extended to define new encodings, orderings and solving strategies. We propose that UppSAT can be used as a sandbox for easy and flexible exploration of new approximations. To substantiate this, we explore encodings of floating-point arithmetic into reduced precision floating-point arithmetic, real-arithmetic, and fixed-point arithmetic (encoded into the theory of bit-vectors in practice). In an experimental evaluation we compare the advantages and disadvantages of approximating solvers obtained by combining various encodings and decision procedures.
|
|
| 7. |
- Zeljic, Aleksandar
(författare)
-
From Machine Arithmetic to Approximations and back again : Improved SMT Methods for Numeric Data Types
- 2017
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Safety-critical systems, especially those found in avionics and automotive industries, rely on machine arithmetic to perform their tasks: integer arithmetic, fixed-point arithmetic or floating-point arithmetic (FPA). Machine arithmetic exhibits subtle differences in behavior compared to the ideal mathematical arithmetic, due to fixed-size representation in memory. Failure of safety-critical systems is unacceptable, due to high-stakes involving human lives or huge amounts of money, time and effort. By formally proving properties of systems, we can be assured that they meet safety requirements. However, to prove such properties it is necessary to reason about machine arithmetic. SMT techniques for machine arithmetic are lacking scalability. This thesis presents approaches that augment or complement existing SMT techniques for machine arithmetic.In this thesis, we explore approximations as a means of augmenting existing decision procedures. A general approximation refinement framework is presented, along with its implementation called UppSAT. The framework solves a sequence of approximations. Initially very crude, these approximations are fairly easy to solve. Results of solving approximate constraints are used to either reconstruct a solution of original constraints, obtain a proof of unsatisfiability or to refine the approximation. The framework preserves soundness, completeness, and termination of the underlying decision procedure, guaranteeing that eventually, either a solution is found or a proof that solution does not exist. We evaluate the impact of approximations implemented in the UppSAT framework on the state-of-the-art in SMT for floating-point arithmetic.A novel method to reason about the theory of fixed-width bit-vectors called mcBV is presented. It is an instantiation of the model constructing satisfiability calculus, mcSAT, and uses a new lazy representation of bit-vectors that allows both bit- and word-level reasoning. It uses a greedy explanation generalization mechanism capable of more general learning compared to traditional approaches. Evaluation of mcBV shows that it can outperform bit-blasting on several classes of problems.
|
|
