Difference between revisions of "Infinite Systems Verification Day"

From Numerical Transition Systems
Jump to: navigation, search
 
(14 intermediate revisions by the same user not shown)
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]
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)''' [[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:
  
  
10:30-11:30 '''Joel Ouaknine (Max Planck Institute for Software Systems and Oxford University)'''
+
10: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]]
  
TBA
+
''Decision Problems for Linear Dynamical Systems''
  
 +
Dynamical systems, both discrete and continuous, permeate vast areas of mathematics, physics, engineering, and computer science. In this talk, we consider a selection of natural decision problems for linear dynamical systems, such as reachability of a given hyperplane. Such problems have applications in a wide array of scientific areas, ranging from theoretical biology and software verification to quantum computing and statistical physics. Perhaps surprisingly, the study of decidability and complexity questions for linear dynamical systems involves techniques from a variety of mathematical fields, including analytic and algebraic number theory, Diophantine geometry, and real algebraic geometry. I will survey some of the known results as well as recent advances and open problems.
  
11:30-12:30 '''Parosh Aziz Abdulla (Uppsala University)'''
 
  
TBA
+
11: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''
 +
 
 +
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.
  
  
Line 35: Line 40:
 
14:00 '''Habilitation a Diriger des Recherches'''
 
14:00 '''Habilitation a Diriger des Recherches'''
  
'''Radu Iosif (Verimag)''' [File: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:  
 
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''
  
  

Latest revision as of 13:09, 18 October 2016

When: Thursday, September 29th, 2016

Where: Auditorium, Ground Floor, IMAG Building

Registration: the event is free and open to the public

Travel and hotels: Grenoble local information



9:00 Welcome


9:30-10:30 Andreas Podelski (University of Freiburg) [video]

Thread Modularity on the Next Level

A thread-modular proof for the correctness of a concurrent program is based on an inductive and interference-free annotation of each thread. It is well-known that the corresponding proof system is not complete (unless one adds auxiliary variables). We introduce a hierarchy of proof systems where each level k corresponds to a new notion of thread modular- ity (level 1 corresponds to the original notion). Each level is strictly more expressive than the previous. The hierarchy can be used to prove interesting programs. We give the to our knowledge first proof of the MACH shootdown algorithm for TLB consistency. The algorithm is correct for an arbitrary number of CPUs. This is joint work with Jochen Hoenicke and Rupak Majumdar.


10:30-11:30 Joel Ouaknine (Max Planck Institute for Software Systems and Oxford University) [video]

Decision Problems for Linear Dynamical Systems

Dynamical systems, both discrete and continuous, permeate vast areas of mathematics, physics, engineering, and computer science. In this talk, we consider a selection of natural decision problems for linear dynamical systems, such as reachability of a given hyperplane. Such problems have applications in a wide array of scientific areas, ranging from theoretical biology and software verification to quantum computing and statistical physics. Perhaps surprisingly, the study of decidability and complexity questions for linear dynamical systems involves techniques from a variety of mathematical fields, including analytic and algebraic number theory, Diophantine geometry, and real algebraic geometry. I will survey some of the known results as well as recent advances and open problems.


11:30-12:30 Parosh Aziz Abdulla (Uppsala University) [video]


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.



14:00 Habilitation a Diriger des Recherches

Radu Iosif (Verimag) Automata and Logics for Program Verification [video]


Jury:

  • Alain Finkel (LSV, ENS de Cachan) reviewer
  • Parosh Aziz Abdulla (Uppsala University) reviewer
  • Joel Ouaknine (Max Planck Institute for Software Systems and Oxford University) reviewer
  • Ahmed Bouajjani (Universite Paris Diderot) examiner
  • Andreas Podelski (University of Freiburg) examiner
  • Nicolas Halbwachs (Verimag, CNRS, Universite de Grenoble Alpes) examiner


Abstract In this thesis, we present several theoretical and practical results on program verification, the main purpose being that of providing cost-efficient solutions to problems that almost always belong to undecidable classes. We appeal to logic and automata theory as they provide essentially the mechanisms to problem solving that are needed for program verification. In this respect, we investigate:

  • logics for reasoning about infinite sets of program configurations, involving infinite data domains (array logics) and complex recursive data structures (separation logic), and
  • automata extended with integer variables (counter machines), possibly with unbounded stacks (recursive integer programs).

We devoted special attention to the connection between logic and automata theory, by using counter machines and tree automata as effective decision procedures for array logics and separation logic, respectively. In this respect, we identified new decidable logical fragments and classes of automata and studied the complexity of their decision problems, such as, e.g. validity, reachability and termination, respectively. Most of these theoretical results have been implemented within prototype tools used to carry out experimental evaluations of their practical efficiency.


17:00 Cocktail