Difference between revisions of "Grenoble meeting 27 February 2015"

Revision as of 15:58, 27 March 2015

Location: Salle Turing, CE4, [VERIMAG Historic Building]

9h30 Coffee+croissants

10h00 Marek Trtik (Verimag) Formula-based Communication Between Program Analyses

A promising approach to checking of program properties is to combine some existing analyses into a better one ideally comprising the union of strengths and the intersection of weaknesses of individual techniques. Unfortunately, the approach is difficult in general as different analyses use different formalisms and build different models of an analysed program. We propose a new approach where individual analyses exchange their knowledge about memory content during their simultaneous execution via a formula-based communication language in order to mutually improve their own precision. The language is analysis-independent and so we can combine arbitrarily many analyses without writing a line of code relating any pair of contributing analyses. Moreover, we show that all static analyses we considered (two abstract interpretations (intervals and polyhedrons) and the classic King's symbolic execution) adopted the concept of the communication very naturally. Finally, although combining analyses by providing a dedicated code may often lead to better results (because of the generality of our communication concept), we show in our experimental evaluation on SV-COMP benchmark suite that our approach indeed provides interesting results in term of improved precision of computed invariants.

10h30 David Bühler (CEA) Improving Static Analyses of C Programs with Conditional Predicates

Designing sound static analyses is a continuing trade-off between precision and complexity. Notably, dataflow analyses often perform overly wide approximations when two control-flow paths meet, by merging states from each path. This paper presents a generic abstract interpretation based framework to enhance the precision of such analyses on join points. It relies on predicated domains, that preserve and reuse information valid only inside some branches of the code. Our predicates are derived from conditional statements, and postpone the loss of information. The work has been integrated into Frama-C, a C source code analysis platform. Experiments on real code show that our approach scales, and improves significantly the precision of the existing analyses of Frama-C. Joint work with Sandrine Blazy and Boris Yakobowski

11h00 Mihaela Sighireanu (LIAFA) Automating Program Proofs Based on Separation Logic with Inductive Definitions

We propose a novel approach for exploiting the inductive definitions in automating program proofs based on inductive invariants. We focus on iterative programs, although our techniques apply to recursive programs as well, and specifications that describe not only the shape of the data structures, but also their content or their size.Empirically, we find that our approach is powerful enough to deal with sophisticated benchmarks, e.g., iterative procedures for searching, inserting, or delet- ing elements in binary search tress, red-black trees, and AVL trees, in a very efficient way. Joint work with C. Enea and Z. Wu.

11h30 Radu Iosif (VERIMAG) Abstraction Refinement for Trace Inclusion of Infinite State Systems

A data automaton is a finite automaton equipped with variables (counters or registers) ranging over infinite data domains. A trace of a data automaton is an alternating sequence of alphabet symbols and values taken by the counters during an execution of the automaton. The problem addressed in this paper is the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable, we give a semi-algorithm based on abstraction refinement, which is proved to be sound and complete, but whose termination is not guaranteed. We have implemented our technique in a prototype tool and show promising results on several non-trivial examples.

12h00 Lunch (on site)

13h30 Cristina Serban (VERIMAG) A Formalization of Separation Logic in SMT_LIB V2.5: Syntax, Types and Semantics

14h00 Business Meeting: minutes

17h00 Coffee break