47 citations · 134 across the 31 of their papers we have counts for
11 papers · 1 filter
Verification under TSO with an infinite Data Domain
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach +1
We examine verification of concurrent programs under the total store ordering (TSO) semantics used by the x86 architecture. In our model, threads manipulate variables over infinite…
Chain-Free String Constraints (Technical Report)
Parosh Aziz Abdulla, Mohamed Faouzi Atig Bui Phi Diep, Lukáš Holík +1
We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This pro…
Parameterized Verification under TSO with Data Types
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach +4
We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially inf…
On the Separability Problem of String Constraints
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave +1
We address the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, d…
Communicating Timed Processes with Perfect Timed Channels
Parosh Aziz Abdulla, Mohamed Faouzi Atig, S. Krishna
We introduce the model of communicating timed automata (CTA) that extends the classical models of finite-state processes communicating through FIFO perfect channels and timed autom…
A Load-Buffer Semantics for Total Store Ordering
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani +1
We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are bas…
On the Upward/Downward Closures of Petri Nets
Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla +1
We study the size and the complexity of computing finite state automata (FSA) representing and approximating the downward and the upward closure of Petri net languages with coverab…
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)…
Zenoness for Timed Pushdown Automata
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jari Stenman
Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age.…
Proceedings 15th International Workshop on Verification of Infinite-State Systems
Lukas Holik, Lorenzo Clemente
This volume contains the proceedings of Infinity'13, the 15th International Workshop on Verification of Infinite-State Systems, which was held in Hanoi, Vietnam on the 14th of Octo…
Approximating Petri Net Reachability Along Context-free Traces
Mohamed Faouzi Atig, Pierre Ganty
We investigate the problem asking whether the intersection of a context-free language (CFL) and a Petri net language (PNL) is empty. Our contribution to solve this long-standing pr…