WING 2014 WORKSHOP PAPERS: PAPERS WITH ABSTRACTS

ABSTRACT. Some of the intrinsic limitations of the widely used static techniques for loop invariant inference can be offset by combining them with dynamic techniques---based on executing automatically generated tests. We show how useful loop invariant candidates can be generated by systematically mutating postconditions; then, we apply dynamic checking to weed out invalid candidates, and static checking to select provably valid ones. We present a framework that automatically applies these techniques to carry out functional correctness proofs without manually written loop invariants. Applied to 28 methods (including 39 different loops) from various java.util classes, our DynaMate prototype automatically discharged 97% of all proof obligations, resulting in automatic complete correctness proofs of 25 out of the 28 methods---outperforming several state-of-the-art tools for fully automatic functional verification of programs with loops.

ABSTRACT. A crucial point in program analysis is the computation of loop invariants. Accurate invariants are required to prove properties on a program but they are difficult to compute. Extensive research has been carried out but, to the best of our knowledge, no benchmark has ever been developed to compare algorithms and tools.

We present ALICe, a toolset to compare automatic computation techniques of affine loop scalar invariants. It comes with a benchmark that we built using 102 test cases which we found in the loop invariant bibliography, and interfaces with three analysis programs, that rely on different techniques: Aspic, isl and PIPS. Conversion tools are provided to handle format heterogeneity of these programs.

Experimental results show the importance of model coding and the poor performances of PIPS on concurrent loops. To tackle these issues, we use two model restructurations techniques whose correctness is proved in Coq, and discuss the improvements realized.

ABSTRACT. We present an extension to an on-demand abstraction framework, which integrates deductive verification and abstract interpretation. Our extension allows for a significantly higher precision when reasoning about programs containing arrays. We demonstrate the usefulness of our approach in the context of reasoning about secure information flow. In addition to abstracting arrays that may have been modified, our approach can also keep full precision while adding additional information about array elements which have been only read but not modified.