5 papers
Stateless Model Checking for POWER
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson +1
We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines sever…
Recency-Bounded Verification of Dynamic Database-Driven Systems (Extended Version)
Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig +2
We propose a formalism to model database-driven systems, called database manipulating systems (DMS). The actions of a DMS modify the current instance of a relational database by ad…
Complexity of regular abstractions of one-counter languages
Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman +3
We study the computational and descriptional complexity of the following transformation: Given a one-counter automaton (OCA) A, construct a nondeterministic finite automaton (NFA)…
Proceedings 14th International Workshop on Verification of Infinite-State Systems
Mohamed Faouzi Atig, Ahmed Rezine
This volume contains the proceedings of Infinity'12, the 14th International Workshop on Verification of Infinite-State Systems, which was held in Paris, France on the 27th of Augus…
Adding Time to Pushdown Automata
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jari Stenman
In this tutorial, we illustrate through examples how we can combine two classical models, namely those of pushdown automata (PDA) and timed automata, in order to obtain timed pushd…