Difference between revisions of "Infinite Systems Verification Day"
Radu iosif (Talk | contribs) |
Radu iosif (Talk | contribs) |
||
| Line 51: | Line 51: | ||
* ''logics for reasoning about infinite sets of program configurations, involving infinite data domains (array logics) and complex recursive data structures (separation logic), and'' | * ''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).'' | * ''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 | + | ''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.'' |
| − | 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.'' | + | |
Revision as of 09:47, 13 July 2016
When: 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
Programme
9:00 Welcome
9:30-10:30 Andreas Podelski (University of Freiburg)
TBA
10:30-11:30 Joel Ouaknine (Max Planck Institute for Software Systems and Oxford University)
TBA
11:30-12:30 Parosh Aziz Abdulla (Uppsala University)
TBA
14:00-17:00 Habilitation a Diriger des Recherches
Radu Iosif (Verimag) Automata and Logics for Program Verification
Jury:
- Alain Finkel (LSV, ENS de Cachan) Rapporteur
- Parosh Aziz Abdulla (Uppsala University) Rapporteur
- Joel Ouaknine (Max Planck Institute for Software Systems and Oxford University) Rapporteur
- Ahmed Bouajjani (Universite Paris Diderot) Examinateur
- Andreas Podelski (University of Freiburg) Examinateur
- Nicolas Halbwachs (Verimag, CNRS, Universite de Grenoble Alpes) Examinateur
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.
