Difference between revisions of "Grenoble meeting 18 July 2017"

Revision as of 09:36, 13 July 2017

Location: IMAG 2nd floor, room 285

10h00-10h30 Coffee

10h30-11h15 Raphael Cordelier (Liafa)

Verification de la librairie Ada listes avec Verifast

11h15-12h00 Cristina Serban (VERIMAG)

Complete Cyclic Proof Systems for Inductive Entailments

In this paper we develop cyclic proof systems for the problem of inclusion between the least sets of models of mutually recursive predicates, when the ground constraints in the inductive definitions belong to the quantifier-free fragments of (i) First Order Logic with the canonical Herbrand interpretation and (ii) Separation Logic, respectively. Inspired by classical automata-theoretic techniques of proving language inclusion between tree automata, we give a small set of inference rules, that are proved to be sound and complete, under certain semantic restrictions, involving the set of constraints in the inductive system. Moreover, we investigate the decidability and computational complexity of these restrictions for all the logical fragments considered and provide a proof search semi-algorithm that becomes a decision procedure for the entailment problem, for those systems that fulfill the restrictions.

12h00-12h45 Xiao Xu (Verimag)

The Impact of Alternation

Alternating automata have been widely used to model and verify systems that handle data from finite domains, such as communication protocols or hardware. The main advantage of the alternating model of computation is that complementation is possible in linear time, thus allowing to concisely encode trace inclusion problems that occur often in verification. In this paper we consider alternating automata over infinite alphabets, whose transition rules are formulae in a combined theory of booleans and some infinite data domain, that relate past and current values of the data variables. The data theory is not fixed, but rather it is a parameter of the class. We show that union, intersection and complementation are possible in linear time in this model and, though the emptiness problem is undecidable, we provide two efficient semi-algorithms, inspired by two state-of-the-art abstraction refinement model checking methods: lazy predicate abstraction \cite{HJMS02} and the \impact~ semi-algorithm \cite{mcmillan06}. We have implemented both methods and report the results of an experimental comparison.

12h45-14h00 Lunch (Canberra)

14h00-17h00 Discussion

Agenda: progress report, final-term review, etc.