VVS Workshop

June 30th, 2011, Verimag (CTL), Grenoble download flyer

Registration

Registration is free of charge. We only need to know how many participants will attend in order to estimate the number of people during the lunch and coffee breaks. There will also be an informal dinner on the evening of June 30th at the Bombay indian restaurant in downtown Grenoble. Please let us know if you intend to come, as reservations will be done in advance (you are kindly requested to pay for the restaurant yourself, expect it to be in the range of 20 to 30 euros).

To register please send email to iosif@imag.fr with subject line:

• • VVS register (for simple registration without dinner)

  • VVS register bombay (for registration including dinner reservation)

Programme

9h00 Welcome and coffee

9h30 Ahmed Bouajjani (LIAFA) Verifying concurrent programs running over TSO

We show that the state reachability problem under TSO is decidable, but highly complex (non primitive recursive) even for finite-state programs (whereas it is PSPACE complete for the SC model). This is due to the fact that, roughly speaking, store buffers have the power of lossy FIFO-channels. Then, we consider this problem under the assumption of a bounded number of context switches. We provide a translation that takes as input a concurrent program P and produces a program P’ such that, running P’ under SC yields the same set of reachable states as running P under TSO with at most K context-switches for each thread, for any fixed K. Basically we show that it is possible to use 2K additional copies of the shared variables of P as local variables to simulate the store buffers. This translation allows to transfer existing results and analysis/verification techniques from SC to TSO for the same class of programs. This talk is based on works with: Mohamed-Faouzi Atig, Sebastian Burckhardt, Madan Musuvathi, and Gennaro Parlato.

10h30 Coffee break

11h00 Ruzica Piskac (EPFL) Software Synthesis using Automated Reasoning

Software synthesis is a technique for automatically generating code from a given specification. The goal of software synthesis is to make software development easier, while increasing both the productivity of the programmer and the correctness of the produced code.

In this talk, I will present an approach to synthesis that relies on the use of automated reasoning and decision procedures. I will describe how to generalize decision procedures into predictable and complete synthesis procedures using linear integer arithmetic as an example. Linear integer arithmetic is interesting in of itself due to the fact that reasoning about collections, such as sets and multisets, can be reduced to reasoning about linear integer arithmetic. The reduction uses a semilinear set characterization of solutions to integer linear arithmetic formulas and a generalization of a recent result on sparse solutions of integer linear programming problems. I will explain how this decision procedure can be applied in both software synthesis and program verification.

11h30 Barbara Jobstmann (VERIMAG) Quantitative Verification and Synthesis

Quantitative constraints have been successfully used to state and analyze non-functional properties such as energy consumption, performance, or reliability. Functional properties are typically viewed in a purely qualitative sense. Desired properties are written in temporal languages and the outcome of verification is a simple Yes or No answer stating that a system satisfies or does not satisfy the desired property. We believe that this black and white view is insufficient both for verification and for synthesis. Instead, we propose that specifications should have a quantitative aspect.

Our recent research shows that quantitative techniques give new insights into qualitative specifications. For instance, average-reward properties allow us to express properties like default behavior or preference relations between implementations that all satisfy the functional property. These additional properties are particularly useful in a synthesis setting, where we aim to automatically construct a system that satisfies the specification, because they allow us to guide the synthesis process making the outcome of synthesis more predictable.

In this talk I will give an overview of (1) how classical specification can be augmented with quantitative constraints, (2) list different quantitative constraints that arise in this way, and (3) show how to verify and synthesize systems that satisfied the initial specification and optimize such quantitative constraints.

This is joint work with Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas Henzinger, Arjun Radhakrishna, and Rohit Singh.

12h00 Nicolas Halbwachs (VERIMAG) Static Analysis of Programs with Arrays

This talk presents some joint works with Mathias Peron and Valentin Perrelle on applying abstract interpretation to the discovery of properties about array contents. In Peron’s thesis and our PLDI’08 paper, we start from an idea from Gopan, Reps and Sagiv [Popl05], which consists in partitioning arrays into symbolic intervals (e.g., $[1,i - 1], [i,i], [i + 1,n]$), and in associating with each such interval $I$ and each array $A$ an abstract variable $A_I$; the new idea is to consider \it relational abstract properties $\Psi(A_I, B_I, ...)$ about these abstract variables, and to interpret such a property \it pointwise on the interval $I$: $\forall \ell \in I, \Psi(A[\ell], B[\ell],...)$. The resulting method is able, for instance, to discover that the result of an insertion sort procedure is a sorted array. A second part of the talk will summarize our VMCAI’10 paper with V. Perrelle, which concerns properties of array contents \it up to a permutation. For instance, to prove a sorting procedure, one has to show that the result is sorted, but also that it is a permutation of the initial array. In order to analyze this kind of properties, we define an abstract interpretation working on multisets of values, and able to discover invariant ``linear’’ equations about such multisets.

12h30 Cezara Dragoi (LIAFA) On Inter-Procedural Analysis of Programs with Lists and Data

We address the problem of automatic synthesis of assertions on sequential programs with singly-linked lists containing data over infinite domains such as integers or reals. Our approach is based on an accurate abstract inter-procedural analysis. We define compositional techniques for computing procedure summaries concerning various aspects such as shapes, sizes, and data.Relations between program configurations are represented by graphs where vertices represent list segments without sharing. The data in the these list segments are characterized by constraints in new complex abstract domains. We define an abstract domain whose elements correspond to an expressive class of first order universally quantified formulas and an abstract domain of multisets. Our analysis computes the effect of each procedure in a local manner, by considering only the reachable parts of the heap from its actual parameters. In order to avoid losses of information, we introduce a mechanism based on unfolding/folding operations allowing to strengthen the analysis in the domain of first-order formulas by the analysis in the multisets domains. The same mechanism is used for strengthening the sound (but incomplete) entailment operator of the domain of first-order formulas. We have implemented our techniques in a prototype tool and we have shown that our approach is powerful enough for automatic (1) generation of non-trivial procedure summaries, (2) pre/post- condition reasoning.

13h00 On-site lunch break

14h00 VERIMAG seminar: Nathalie Bertrand (IRISA) Determinizing timed automata

Timed automata are frequently used to model real-time systems. Essentially timed automata are an extension of finite automata with guards and resets of continuous variables (called clocks) evolving at the same pace. They are extensively used in the context of validation of real-time systems. One of the reasons for this popularity is that, despite the fact that they represent infinite state systems, their reachability is decidable, thanks to the construction of the region graph abstraction. As for other models, determinization is a key issue for several validation problems, such as monitoring, implementability and testing. However, not all timed automata can be determinized, and determinizability itself is undecidable. After introducing timed automata, we will review existing approaches to get round their unfeasible determinization. Then we will expose a novel game-based algorithm which, given a timed automaton, produces either a deterministic equivalent or a deterministic over-approximation, and which subsumes all other known contributions.

15h00 Pierre Corbineau (VERIMAG) On Positivstellensatz Witnesses in Degenerate Cases

One can reduce the problem of proving that a polynomial is nonnegative, or more generally of proving that a system of polynomial inequalities has no solutions, to finding polynomials that are sums of squares of polynomials and satisfy some linear equality (Positivstellensatz). This produces a witness for the desired property, from which it is reasonably easy to obtain a formal proof of the property suitable for a proof assistant such as Coq. The problem of finding a witness reduces to a feasibility problem in semidefinite programming, for which there exist numerical solvers. Unfortunately, this problem is in general not strictly feasible, meaning the solution can be a convex set with empty interior, in which case the numerical optimization method fails. Previously published methods thus assumed strict feasibility; we propose a workaround for this difficulty. We implemented our method and illustrate its use with examples, including extractions of proofs to Coq.

Joint work with David Monniaux.

15h30 Michael Emmi (LIAFA) On Sequentializing Concurrent Programs

We propose a general framework for compositional under- approximate concurrent program analyses by reduction to sequential program analyses—so-called sequentializations. We notice the existing sequentializations—based on bounding the number of execution contexts, execution rounds, or delays from a deterministic task-schedule—rely on three key features for scalable concurrent program analyses: (i) reduction to the sequential program model, (ii) compositional reasoning to avoid expensive task-product constructions, and (iii) parameterized exploration bounds. To understand how those sequentializations can be unified and generalized, we define a general framework which preserves their key features, and in which those sequentializations are particular instances. We also identify a most general instance which considers vastly more executions, by composing the rounds of different tasks in any order, re- stricted only by the unavoidable program and task-creation causality orders. In fact, we show this general instance is fundamentally more powerful by identifying an infinite family of state-reachability problems (to states g1 , g2 , . . .) which can be answered precisely with a fixed explo- ration bound, whereas the existing sequentializations require an increasing bound k to reach each gk . Our framework applies to a general class of shared-memory concurrent programs, with dynamic task-creation and arbitrary preemption.

16h00 Jules Villard (LSV/Queen Mary) Tracking Heaps that Hop with Heap-Hop

Heap-Hop is a program prover for concurrent heap-manipulating programs that use message-passing synchronization. Programs are annotated with pre and post-conditions and loop invariants, written in a fragment of separation logic. Communications are governed by a form of session types called contracts. Logic and contracts collaborate inside of Heap-Hop to prove memory safety, race freedom, absence of memory leaks and communication safety.

This is joint work with Étienne Lozes (LSV, ENS Cachan, CNRS) and Cristiano Calcagno (Monoidics Ltd and Imperial College, London).

16h30 Coffee break

17h00 VERIDYC business meeting