Difference between revisions of "Paris, April 29th and 30th"
Radu iosif (Talk | contribs) |
Radu iosif (Talk | contribs) |
||
| Line 30: | Line 30: | ||
| − | 16h00-17h00 '''Alessio Mansutti''': '' | + | 16h00-17h00 '''Alessio Mansutti''': ''Extending Propositional Separation Logic for Robustness Properties'' |
| − | + | We study an extension of propositional separation logic that can specify robustness properties, | |
| − | with | + | such as acyclicity and garbage freedom, for automatic verification of stateful programs with |
| − | + | singly-linked lists. We show that its satisfiability problem is PSpace-complete, whereas modest | |
| − | + | extensions of the logic are shown to be Tower-hard. As separating implication, reachability | |
| − | + | predicates (under some syntactical restrictions) and a unique quantified variable are allowed, | |
| − | + | this logic subsumes several PSpace-complete separation logics considered in previous works. | |
| − | + | ||
Latest revision as of 18:35, 23 April 2019
Location: Salle 3052, Bâtiment Sophie Germain, 8 place Aurélie Nemours 75013 Paris
Monday April 29th
10h00-12h00 Discussion on future project organisation
14h00-14h45 Wrapup of the pre-scientific discussion
15h00-16h00 Stephane Demri: Modal Separation Logics and Friends
Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in order to verify programs with mutable data structures. The separating conjunction allows us to evaluate formulae in subheaps, and this possibility to evaluate formulae in alternative models is a feature shared with many modal logics such as sabotage logics, logics of public announcements or relation-changing modal logics. In the first part of the talk, we present several versions of modal separation logics whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction. Fragments are genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. In the second part of the talk, we present the decidability status and the computational complexity of several modal separation logics, (for instance, leading to NP-complete or Tower-complete satisfiability problems). In the third part, we investigate the complexity of fragments of quantified CTL under the tree semantics (or similar modal logics with propositional quantification), some of these fragments being related to modal separation logics. Part of the presented work is done jointly with B. Bednarczyk (U. of Wroclaw) or with R. Fervari (U. of Cordoba).
16h00-17h00 Alessio Mansutti: Extending Propositional Separation Logic for Robustness Properties
We study an extension of propositional separation logic that can specify robustness properties, such as acyclicity and garbage freedom, for automatic verification of stateful programs with singly-linked lists. We show that its satisfiability problem is PSpace-complete, whereas modest extensions of the logic are shown to be Tower-hard. As separating implication, reachability predicates (under some syntactical restrictions) and a unique quantified variable are allowed, this logic subsumes several PSpace-complete separation logics considered in previous works.
Tuesday April 30th
10h00-11h00 Nicolas Peltier: Towards completeness results for fragments of symbolic heaps with inductive definitions (work in progress)
In this talk, I will present some ideas and preliminary results about algorithms for testing logical entailment between symbolic heaps, in the presence of user-defined inductive predicates and interpreted theories. I will consider simple sequent-based proof procedures with explicit induction and investigate the completeness and termination of these procedures for specific fragments. We shall consider partially defined tree-like data-structures enriched with additional "local" edges and interpreted values.
11h00-12h00 Radu Iosif: Interaction Logics for Parametric Architectures
We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous atomic state changes of a set of components. We specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology (i.e.\ architecture) of the system (e.g.\ pipeline, ring) via a decidable interaction logic, which is embedded in the classical weak sequential calculus of one successor (WS1S). Proving correctness of such system for safety properties, such as deadlock freedom or mutual exclusion, requires the inference of an inductive invariant that subsumes the set of reachable states and avoids the unsafe states. Our method synthesizes such invariants directly from the formula describing the interactions, without costly fixed point iterations. Finally, we present work in progress on the development of a separation logic of interactions, in which one specify parametric architectures using inductive definitions. Joint work with Marius Bozga and Joseph Sifakis (VERIMAG).
