Abstract
Formal verification of reactive systems is an increasingly important research area of computer science. Modern systems now include features which make their design difficult and verifying their correctness very demanding. Companies such as Facebook and Amazon have teams dedicated to formally verifying their systems while, in academia, works on verification have already been lauded with two Turing awards in the last twenty years.
As systems become more complex, more intricate models are required in order to capture their behaviour. Counter automata result from adding integer-valued counters to the widely studied model of finite automata. The formal verification community has found several uses for different classes of counter automata.
This project aims at (i) contributing to the theory of automatic software verification --- in particular, model checking various classes of one-counter automata, (ii) translating those model-checking algorithms into semi-decision procedures implementable in existing interactive software verification tools, and (iii) guiding the development of the theory based on the limitations and capabilities of such tools.
Researcher(s)
Research team(s)
Project type(s)