Paris, April 29th and 30th - Revision history

Radu iosif at 17:35, 23 April 2019

2019-04-23T17:35:36Z

Radu iosif at 14:53, 18 April 2019

2019-04-18T14:53:45Z

Radu iosif at 14:52, 18 April 2019

2019-04-18T14:52:55Z

Radu iosif at 14:50, 18 April 2019

2019-04-18T14:50:25Z

Radu iosif at 13:15, 1 April 2019

2019-04-01T13:15:18Z

Radu iosif at 13:15, 1 April 2019

2019-04-01T13:15:08Z

Radu iosif at 16:31, 20 March 2019

2019-03-20T16:31:01Z

Radu iosif at 16:30, 20 March 2019

2019-03-20T16:30:51Z

Radu iosif: Created page with "'''Stephane Demri''': ''Modal Separation Logics and Friends'' Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in o..."

2019-03-20T16:28:31Z

Created page with "'''Stephane Demri''': ''Modal Separation Logics and Friends'' Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in o..."

New page

'''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).

'''Alessio Mansutti''': ''Axiomatising Logics with Separating Conjunction and Modalities''

Modal separation logics are formalisms that combine modal operators to reason locally,
with separating connectives that allow to perform global updates on the models.
In this work, we design Hilbert-style proof systems for the modal separation logics
MSL(*,<=/=>) and MSL(*,<>), where * is the separating conjunction, <> is the standard
modal operator and <=/=> is the difference modality. The calculi only use the logical
languages at hand (no external features such as labels) and take advantage of new normal
forms and of their axiomatisation.

'''Nicolas Peltier''': TBA

'''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.

@@ Line 30: / Line 30: @@
-h00-17h00 '''Alessio Mansutti''': ''Axiomatising Logics with Separating Conjunction and Modalities''
+h00-17h00 '''Alessio Mansutti''': ''Extending Propositional Separation Logic for Robustness Properties''
-Modal separation logics are formalisms that combine modal operators to reason locally,
+We study an extension of propositional separation logic that can specify robustness properties,
-with separating connectives that allow to perform global updates on the models.
+such as acyclicity and garbage freedom, for automatic verification of stateful programs with
-In this work, we design Hilbert-style proof systems for the modal separation logics
+singly-linked lists. We show that its satisfiability problem is PSpace-complete, whereas modest
-MSL(*,<=/=>) and MSL(*,<>), where * is the separating conjunction, <> is the standard
+extensions of the logic are shown to be Tower-hard. As separating implication, reachability
-modal operator and <=/=> is the difference modality. The calculi only use the logical
+predicates (under some syntactical restrictions) and a unique quantified variable are allowed,
-languages at hand (no external features such as labels) and take advantage of new normal
+this logic subsumes several PSpace-complete separation logics considered in previous works.
-forms and of their axiomatisation.

← Older revision		Revision as of 14:53, 18 April 2019
Line 65:		Line 65:
	from the formula describing the interactions, without costly fixed point iterations. Finally, we present work in progress		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.		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).

@@ Line 6: / Line 6: @@
 h00-14h45 Wrapup of the pre-scientific discussion
 h00-16h00 '''Stephane Demri''': ''Modal Separation Logics and Friends''
@@ Line 27: / Line 28: @@
 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).
 h00-17h00 '''Alessio Mansutti''': ''Axiomatising Logics with Separating Conjunction and Modalities''

@@ Line 1: / Line 1: @@
 Location: Salle 3052, Bâtiment Sophie Germain, 8 place Aurélie Nemours 75013 Paris
-'''Stephane Demri''': ''Modal Separation Logics and Friends''
+h00-12h00 Discussion on future project organisation
 Separation logic is known as an assertion language to perform verification,
@@ Line 23: / Line 28: @@
 jointly with B. Bednarczyk (U. of Wroclaw) or with R. Fervari (U. of Cordoba).
+h00-17h00 '''Alessio Mansutti''': ''Axiomatising Logics with Separating Conjunction and Modalities''
 '''Alessio Mansutti''': ''Axiomatising Logics with Separating Conjunction and Modalities''
 Modal separation logics are formalisms that combine modal operators to reason locally,
@@ Line 35: / Line 39: @@
-'''Nicolas Peltier''': Towards completeness results for fragments of symbolic heaps with inductive definitions (work in progress)
+== Tuesday April 30th ==
 In this talk, I will present some ideas and preliminary results about algorithms for testing logical
@@ Line 44: / Line 51: @@
-'''Radu Iosif''': ''Interaction Logics for Parametric Architectures''
+h00-12h00 '''Radu Iosif''': ''Interaction Logics for Parametric Architectures''
 We consider concurrent systems consisting of a finite but unknown number of components,

@@ Line 42: / Line 42: @@
 termination of these procedures for specific fragments. We shall consider partially defined tree-like data-structures
 enriched with additional "local" edges and interpreted values.
 '''Radu Iosif''': ''Interaction Logics for Parametric Architectures''

← Older revision		Revision as of 13:15, 1 April 2019
Line 35:		Line 35:


−	'''Nicolas Peltier''': ~~TBA~~	+	'''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.

	'''Radu Iosif''': ''Interaction Logics for Parametric Architectures''		'''Radu Iosif''': ''Interaction Logics for Parametric Architectures''

← Older revision		Revision as of 16:31, 20 March 2019
Line 1:		Line 1:
	Location: Salle 3052, Bâtiment Sophie Germain, 8 place Aurélie Nemours 75013 Paris		Location: Salle 3052, Bâtiment Sophie Germain, 8 place Aurélie Nemours 75013 Paris
		+

	'''Stephane Demri''': ''Modal Separation Logics and Friends''		'''Stephane Demri''': ''Modal Separation Logics and Friends''

← Older revision		Revision as of 16:30, 20 March 2019
Line 1:		Line 1:
		+	Location: Salle 3052, Bâtiment Sophie Germain, 8 place Aurélie Nemours 75013 Paris
		+
	'''Stephane Demri''': ''Modal Separation Logics and Friends''		'''Stephane Demri''': ''Modal Separation Logics and Friends''