| 1. |
- Brillout, Angelo, et al.
(author)
-
An interpolating sequent calculus for quantifier-free Presburger arithmetic
- 2011
-
In: Journal of automated reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 47:4, s. 341-367
-
Journal article (peer-reviewed)abstract
- Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that serve as candidates for loop invariants. In this paper, we consider Craig interpolation for quantifier-free Presburger arithmetic (QFPA). Until recently, quantifier elimination was the only available interpolation method for this theory, which is, however, known to be potentially costly and inflexible. We introduce an interpolation approach based on a sequent calculus for QFPA that determines interpolants by annotating the steps of an unsatisfiability proof with partial interpolants. We prove our calculus to be sound and complete. We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available Presburger arithmetic benchmarks. The results document the robustness and efficiency of our interpolation procedure. Finally, we compare the procedure against alternative interpolation methods, both for QFPA and linear rational arithmetic.
|
|
| 2. |
|
|
| 3. |
- Cook, Byron, et al.
(author)
-
Ranking function synthesis for bit-vector relations
- 2013
-
In: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 43:1, s. 93-120
-
Journal article (peer-reviewed)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.
|
|
| 4. |
- Donaldson, Alastair F., et al.
(author)
-
Automatic analysis of DMA races using model checking and k-induction
- 2011
-
In: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 39:1, s. 83-113
-
Journal article (peer-reviewed)abstract
- Modern multicore processors, such as the Cell Broadband Engine, achieve high performance by equipping accelerator cores with small "scratch-pad" memories. The price for increased performance is higher programming complexity - the programmer must manually orchestrate data movement using direct memory access (DMA) operations. Programming using asynchronous DMA operations is error-prone, and DMA races can lead to nondeterministic bugs which are hard to reproduce and fix. We present a method for DMA race analysis in C programs. Our method works by automatically instrumenting a program with assertions modeling the semantics of a memory flow controller. The instrumented program can then be analyzed using state-of-the-art software model checkers. We show that bounded model checking is effective for detecting DMA races in buggy programs. To enable automatic verification of the correctness of instrumented programs, we present a new formulation of k-induction geared towards software, as a proof rule operating on loops. Our techniques are implemented as a tool, Scratch, which we apply to a large set of programs supplied with the IBM Cell SDK, in which we discover a previously unknown bug. Our experimental results indicate that our k-induction method performs extremely well on this problem class. To our knowledge, this marks both the first application of k-induction to software verification, and the first example of software model checking in the context of heterogeneous multicore processors.
|
|
| 5. |
- Donaldson, Alastair F., et al.
(author)
-
SCRATCH : a tool for automatic analysis of DMA races
- 2011
-
In: Proc. 16th ACM Symposium on Principles and Practice of Parallel Programming. - New York : ACM Press. - 9781450301190 ; , s. 311-312
-
Conference paper (peer-reviewed)
|
|
| 6. |
- Donaldson, Alastair F., et al.
(author)
-
Software verification using k-induction
- 2011
-
In: Static Analysis. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642237010 ; , s. 351-368
-
Conference paper (peer-reviewed)
|
|
| 7. |
|
|
| 8. |
|
|
