Infinite Systems Verification Day - Revision history

Radu iosif at 12:09, 18 October 2016

2016-10-18T12:09:29Z

2016-10-18T12:09:05Z

2016-10-18T12:08:43Z

2016-10-18T12:06:40Z

2016-08-29T12:46:20Z

2016-08-29T12:20:15Z

2016-08-04T09:51:30Z

2016-08-04T09:51:05Z

2016-08-04T09:50:00Z

2016-07-28T14:51:29Z

@@ Line 21: / Line 21: @@
-:30-11:30 '''[http://www.cs.ox.ac.uk/people/joel.ouaknine/home.html Joel Ouaknine] (Max Planck Institute for Software Systems and Oxford University)''' [http://newstream.imag.fr/2016-09-29_Infinite-Systems-2.mp4 video]
+:30-11:30 '''[http://www.cs.ox.ac.uk/people/joel.ouaknine/home.html Joel Ouaknine] (Max Planck Institute for Software Systems and Oxford University)''' [[http://newstream.imag.fr/2016-09-29_Infinite-Systems-2.mp4 video]]
 ''Decision Problems for Linear Dynamical Systems''
@@ Line 28: / Line 28: @@
-:30-12:30 '''[http://user.it.uu.se/~parosh/ Parosh Aziz Abdulla] (Uppsala University)''' [http://newstream.imag.fr/2016-09-29_Infinite-Systems-3.mp4 video]
+:30-12:30 '''[http://user.it.uu.se/~parosh/ Parosh Aziz Abdulla] (Uppsala University)''' [[http://newstream.imag.fr/2016-09-29_Infinite-Systems-3.mp4 video]]
@@ Line 40: / Line 40: @@
 :00 '''Habilitation a Diriger des Recherches'''
-'''[[Radu Iosif]] (Verimag)''' [http://nts.imag.fr/images/6/6c/Hdr.pdf ''Automata and Logics for Program Verification''] [http://newstream.imag.fr/2016-09-29_Infinite-Systems-4.mp4 video]
+'''[[Radu Iosif]] (Verimag)''' [http://nts.imag.fr/images/6/6c/Hdr.pdf ''Automata and Logics for Program Verification''] [[http://newstream.imag.fr/2016-09-29_Infinite-Systems-4.mp4 video]]

← Older revision		Revision as of 12:09, 18 October 2016
Line 14:		Line 14:


−	9:30-10:30 '''[http://swt.informatik.uni-freiburg.de/staff/podelski Andreas Podelski] (University of Freiburg)''' [http://newstream.imag.fr/2016-09-29_Infinite-Systems-1.mp4 video]	+	9:30-10:30 '''[http://swt.informatik.uni-freiburg.de/staff/podelski Andreas Podelski] (University of Freiburg)''' [[http://newstream.imag.fr/2016-09-29_Infinite-Systems-1.mp4 video]]

	''Thread Modularity on the Next Level''		''Thread Modularity on the Next Level''

@@ Line 21: / Line 21: @@
-:30-11:30 '''[http://www.cs.ox.ac.uk/people/joel.ouaknine/home.html Joel Ouaknine] (Max Planck Institute for Software Systems and Oxford University)'''
+:30-11:30 '''[http://www.cs.ox.ac.uk/people/joel.ouaknine/home.html Joel Ouaknine] (Max Planck Institute for Software Systems and Oxford University)''' [http://newstream.imag.fr/2016-09-29_Infinite-Systems-2.mp4 video]
 ''Decision Problems for Linear Dynamical Systems''
@@ Line 28: / Line 28: @@
-:30-12:30 '''[http://user.it.uu.se/~parosh/ Parosh Aziz Abdulla] (Uppsala University)'''
+:30-12:30 '''[http://user.it.uu.se/~parosh/ Parosh Aziz Abdulla] (Uppsala University)''' [http://newstream.imag.fr/2016-09-29_Infinite-Systems-3.mp4 video]
 ''Automatic Verification of Linearization Policies''
@@ Line 39: / Line 40: @@
 :00 '''Habilitation a Diriger des Recherches'''
-'''[[Radu Iosif]] (Verimag)''' [http://nts.imag.fr/images/6/6c/Hdr.pdf ''Automata and Logics for Program Verification'']
+'''[[Radu Iosif]] (Verimag)''' [http://nts.imag.fr/images/6/6c/Hdr.pdf ''Automata and Logics for Program Verification''] [http://newstream.imag.fr/2016-09-29_Infinite-Systems-4.mp4 video]
 Jury:

← Older revision		Revision as of 12:06, 18 October 2016
Line 14:		Line 14:


−	9:30-10:30 '''[http://swt.informatik.uni-freiburg.de/staff/podelski Andreas Podelski] (University of Freiburg)'''	+	9:30-10:30 '''[http://swt.informatik.uni-freiburg.de/staff/podelski Andreas Podelski] (University of Freiburg)''' [http://newstream.imag.fr/2016-09-29_Infinite-Systems-1.mp4 video]

	''Thread Modularity on the Next Level''		''Thread Modularity on the Next Level''

@@ Line 43: / Line 43: @@
 Jury:
-* Alain Finkel (LSV, ENS de Cachan) ''rapporteur''
+* Alain Finkel (LSV, ENS de Cachan) ''reviewer''
-* Parosh Aziz Abdulla (Uppsala University) ''rapporteur''
+* Parosh Aziz Abdulla (Uppsala University) ''reviewer''
-* Joel Ouaknine (Max Planck Institute for Software Systems and Oxford University) ''rapporteur''
+* Joel Ouaknine (Max Planck Institute for Software Systems and Oxford University) ''reviewer''
-* Ahmed Bouajjani (Universite Paris Diderot) ''examinateur''
+* Ahmed Bouajjani (Universite Paris Diderot) ''examiner''
-* Andreas Podelski (University of Freiburg) ''examinateur''
+* Andreas Podelski (University of Freiburg) ''examiner''
-* Nicolas Halbwachs (Verimag, CNRS, Universite de Grenoble Alpes) ''examinateur''
+* Nicolas Halbwachs (Verimag, CNRS, Universite de Grenoble Alpes) ''examiner''

← Older revision		Revision as of 12:20, 29 August 2016
Line 30:		Line 30:
	11:30-12:30 '''[http://user.it.uu.se/~parosh/ Parosh Aziz Abdulla] (Uppsala University)'''		11:30-12:30 '''[http://user.it.uu.se/~parosh/ Parosh Aziz Abdulla] (Uppsala University)'''

−	~~TBA~~	+	''Automatic Verification of Linearization Policies''
		+
		+	We consider the problem of proving linearizability for concurrent threads that access a shared data structure. Such systems give rise to unbounded numbers of threads that operate on an bounded data domain and that access dynamically allocated memory. Furthermore, proving linearizability is harder than proving control state reachability due to existentially quantified linearization points. The problem is further complicated by the presence of advanced features such as non-fixed linearization points, speculation, and helping. In this presentation, we present a framework that can automatically verify linearizability for concurrent data structures that implement sets, stacks, and queues. We use a specification formalism for linearization techniques which allows the user to specify, in a simple and and concise manner, complex patterns including non-fixed linearization points. Then, we define abstraction techniques that allow to make the size of the data domain and the number of threads finite.

← Older revision		Revision as of 09:50, 4 August 2016
Line 14:		Line 14:


−	9:30-10:30 '''Andreas Podelski (University of Freiburg)'''	+	9:30-10:30 '''[http://swt.informatik.uni-freiburg.de/staff/podelski Andreas Podelski] (University of Freiburg)'''

	''Thread Modularity on the Next Level''		''Thread Modularity on the Next Level''

← Older revision		Revision as of 14:51, 28 July 2016
Line 1:		Line 1:

−	'''When''': September 29th, 2016	+	'''When''': Thursday, September 29th, 2016

	'''Where''': Auditorium, Ground Floor, [https://batiment.imag.fr/ IMAG Building]		'''Where''': Auditorium, Ground Floor, [https://batiment.imag.fr/ IMAG Building]