Cachan, April 29th and 30th - Revision history

Radu iosif at 18:02, 19 March 2019

2019-03-19T18:02:58Z

Radu iosif at 17:58, 19 March 2019

2019-03-19T17:58:59Z

Radu iosif at 17:58, 19 March 2019

2019-03-19T17:58:45Z

Radu iosif at 17:58, 19 March 2019

2019-03-19T17:58:10Z

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 order t..."

2019-03-19T17:56:33Z

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 order t..."

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(⇤,h6=i) and MSL(⇤,3), where ⇤ is the separating conjunction, 3 is the standard modal operator and h6=i 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.

← Older revision		Revision as of 18:02, 19 March 2019
Line 30:		Line 30:
	languages at hand (no external features such as labels) and take advantage of new normal		languages at hand (no external features such as labels) and take advantage of new normal
	forms and of their axiomatisation.		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 19: / Line 19: @@
 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''

@@ Line 1: / Line 1: @@
-Stephane Demri: ''Modal Separation Logics and Friends''
+'''Stephane Demri''': ''Modal Separation Logics and Friends''
 Separation logic is known as an assertion language to perform verification,
@@ Line 20: / Line 20: @@
 jointly with B. Bednarczyk (U. of Wroclaw) or with R. Fervari (U. of Cordoba).
-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,

← Older revision		Revision as of 17:58, 19 March 2019
Line 22:		Line 22:
	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, 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(⇤,h6=i) and MSL(⇤,3), where ⇤ is the separating conjunction, 3 is the standard modal operator and h6=i 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.	+	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.