Difference between revisions of "Paris meeting 2 December 2015"

Latest revision as of 18:26, 13 November 2015

Location: Liafa

10h00-10h30 Constatin Enea (Liafa)

Symbolic Abstract Data Type Inference

Formal specification is a vital ingredient to scalable verification of software systems. In the case of efficient implementations of concurrent objects like atomic registers, queues, and locks, symbolic formal representations of their abstract data types (ADTs) enable efficient modular reasoning, decoupling clients from implementations. Writing adequate formal specifications, however, is a complex task requiring rare expertise. In practice, programmers write reference implementations as informal specifications.

In this work we demonstrate that effective symbolic ADT representations can be automatically generated from the executions of reference implementations. Our approach exploits two key features of naturally-occurring ADTs: violations can be decomposed into a small set of representative patterns, and these patterns manifest in executions with few operations. By identifying certain algebraic properties of naturally-occurring ADTs, and exhaustively sampling executions up to a small number of operations, we generate concise symbolic ADT representations which are complete in practice, enabling the application of efficient symbolic verification algorithms without the burden of manual specification. Furthermore, the concise ADT violation patterns we generate are human-readable, and can serve as useful, formal documentation.

This is joint work with Michael Emmi.

10h30-11h00 Peter Habermehl (Liafa)

Regular transformations of data words through origin information

We introduce a class of transformations of finite data words which generalizes the well-known class of regular finite string transformations described by MSO-definable transductions of finite strings. These transformations map input words to output words whereas our transformations handle data words where each position has a letter from a finite alphabet and a data value. Each data value appearing in the output has as origin a data value in the input. As is the case for regular transformations we show that our class of transformations has equivalent characterizations in terms of novel deterministic two-way and streaming string transducers.

11h00-11h30 Radu Iosif (Verimag)

Abstraction Refinement and Antichains 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 in general, 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.

Joint work with Tomas Vojnar and Adam Rogalewicz

11h30-12h00 David Bühler (CEA)

A modular architecture for the combination of domains in Frama-C's abstract interpreter

Frama-C is a platform of plugins dedicated to the analysis of C code. Among them, the Value Analysis performs an abstract interpretation based analysis. It relies on a low-level memory model, a rich value domain, an ad hoc instance of trace partitioning, and has been deeply optimized to scale on big programs. Thanks to that, it already provides precise results and good analysis times on embedded codes. However, its abstract domain lacks relational components, is hardly extensible, and is completely hard-wired in the whole analyzer.

We present a major evolution of this plugin, that eases the introduction of new abstractions. The analysis is now parametrized by the abstract domain, and the new architecture allows the combination of several abstract domains, which communicate through the value of C expressions (expressed as intervals, congruences, and a precise representation of aliasing) and generated alarms (logical assertions excluding error cases).

This work has already enabled the integration of the numerical domains provided by the Apron library, and some specific new domains are currently being written and tested.

12h00-14h00 Lunch

14h00-15h00 Keynote Speaker: Bart Jacobs (University of Louvain, Belgium)

Verifying container libraries with VeriFast

VeriFast is a tool for sound modular verification of C and Java programs annotated with expressive separation logic specifications and proof hints. By automating only the trivial proof steps, VeriFast aims to combine reasonable annotation overhead (in terms of lines of annotations, but more importantly in terms of user effort; a high annotation rate might be acceptable if the annotations are easy to write) with good and predictable performance and good diagnosability of proof failures. In this talk, I will give a VeriFast crash course and go through some verified container implementations. Besides data structure shape, contents, and invariant description and algorithm verification, issues discussed include deep vs. shallow ownership of elements; dynamically bound 'equals' and 'hashCode' methods; specifying iterators; specifying abstract superclasses such as Collection. I will also discuss fine-grained concurrent data structure specification and verification.

15h00-15h30 Gustavo Petri (Liafa)

Data-Driven Shape Inference

I will present an automated procedure for discovering expressive shape specifications for inductive data structures. In this approach we extract potential shape predicates based on the definition of constructors of arbitrary user-defined inductive data types, and combine these predicates within an expressive first-order specification language using a lightweight data-driven learning procedure. Notably, this technique requires no programmer annotations, and is equipped with a type-based decision procedure to verify the correctness of discovered specifications.

Joint work with He Zhu and Suresh Jagannathan.

15h30-16h00 Yannick Moy (AdaCore)

Functionally Specified Containers for Use in Proven Code

As part of a new library of traits-based generic containers, we are developing a version of these generic containers that can be used in SPARK code, so that correct usage of the containers and functional properties over the containers's data can be formally proven using the SPARK toolset. This version of containers for vectors, lists, sets and maps defines ghost accessors over the content of imperative containers that return functional views (or 'models') of the container. Contrary to the previous containers used in SPARK, this new version relies exclusively on visible user-level contracts in SPARK on subprogram declarations to express properties, instead of depending on a hidden axiomatization in the intermediate language Why3. We will show proven examples of client code with the former containers and the new versions, that show the increased readability of new contracts on user code.

16h00-16h30 Coffee break

16h30-17h30 Business Meeting