[Show/Hide Left Column]

Emergence VERICONISS        
  • World
    • No language is assigned to this page.


Verification of Concurrent Infinite State Systems 

Action line: SciLex
Subject : reachability, model checking and equivalence checking of concurrent infinite state systems
Project Coordinator : Stefan Göller
Current Member : Georg Zetzsche (Post-doc)
Former Members : Christoph Haase (Post-doc), Piotr Hofman (Post-doc)
Host Laboratory : LSV Cachan
DigiCosme Funding : 2014/2017

This research project plans to investigate the central research questions of reachability, model checking and equivalence checking of models of infinite state systems that allow to model concurrency . This area of research is young and active on the one hand, but also complex and very badly understood on the other. We aim at developing a better understanding of how concurrent infinite state systems behave algorithmically with respect to the above-mentioned formal verification tasks.

Very generally speaking we would like to provide answers to the following questions. Firstly, when is the respective verification task decidable, i.e. when can it effectively be solved on computers? Secondly, in case the respective verification task is decidable, how many resources in terms of time and space consumption are sufficient and necessary to solve it on computers?


Scientific productions :

Interdisciplinary work :