Mohamed Faouzi Atig

Checking Consistency of Event-Driven Traces

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rajanbabu, Govind; Grahn, Samuel et al.

Part of Programming Languages and Systems, p. 173-194, 2026

• DOI for Checking Consistency of Event-Driven Traces
• Download full text (pdf) of Checking Consistency of Event-Driven Traces

Parametrised Verification of Intel-x86 Programs

Abdulla, Parosh; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, Narayan et al.

Part of Proceedings of the ACM on Programming Languages, p. 1094-1122, 2026

• DOI for Parametrised Verification of Intel-x86 Programs
• Download full text (pdf) of Parametrised Verification of Intel-x86 Programs

When GNNs Met a Word Equations Solver: Learning to Rank Equations

Abdulla, Parosh; Atig, Mohamed Faouzi; Cailler, Julie; Liang, Chencheng et al.

Part of Frontiers of Combining Systems (FroCoS 2025), p. 327-345, 2025

• DOI for When GNNs Met a Word Equations Solver: Learning to Rank Equations

Verification of the Release-Acquire Semantics

Abdulla, Parosh; Anastasiadi, Elli; Atig, Mohamed Faouzi; Grahn, Samuel

Part of Theoretical Aspects of Computing - ICTAC 2025 - 22nd International Colloquium, Marrakech, Morocco, November 24-28, 2025, Proceedings, p. 106-123, 2025

• DOI for Verification of the Release-Acquire Semantics

Guiding Word Equation Solving using Graph Neural Networks

Abdulla, Parosh; Atig, Mohamed Faouzi; Cailler, Julie; Liang, Chencheng et al.

Part of Automated Technology for Verification and Analysi, p. 279-301, 2024

• DOI for Guiding Word Equation Solving using Graph Neural Networks

Parametrised Verification of Intel-x86 Programs

Abdulla, Parosh; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, Narayan et al.

Part of Proceedings of the ACM on Programming Languages, p. 1094-1122, 2026

• DOI for Parametrised Verification of Intel-x86 Programs
• Download full text (pdf) of Parametrised Verification of Intel-x86 Programs

Verification under Intel-x86 with Persistency

Abdulla, Parosh; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, K. Narayan et al.

Part of Proceedings of the ACM on Programming Languages, 2024

• DOI for Verification under Intel-x86 with Persistency
• Download full text (pdf) of Verification under Intel-x86 with Persistency

The Computing Journal gratefully acknowledges the editorial work of the scientists listed below on the special issue entitled "SI: NETYS 2019"

Atig, Mohamed Faouzi

Part of Computing, p. 2157-2157, 2022

• DOI for The Computing Journal gratefully acknowledges the editorial work of the scientists listed below on the special issue entitled "SI: NETYS 2019"

Deciding Reachability under Persistent x86-TSO

Abdulla, Parosh; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, K. Narayan et al.

Part of Proceedings of the ACM on Programming Languages, 2021

• DOI for Deciding Reachability under Persistent x86-TSO
• Download full text (pdf) of Deciding Reachability under Persistent x86-TSO

What is decidable under the TSO memory model?

Atig, Mohamed Faouzi

Part of ACM SIGLOG News, p. 4-19, 2020

• DOI for What is decidable under the TSO memory model?

Preface to the VECoS 2018 special issue of ISSE

Atig, Mohamed Faouzi; Bliudze, Simon

Part of Innovations in Systems and Software Engineering, p. 99-100, 2020

• DOI for Preface to the VECoS 2018 special issue of ISSE

Parameterized verification under TSO is PSPACE-complete

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rezvan, Rojin

Part of Proceedings of the ACM on Programming Languages, 2020

• DOI for Parameterized verification under TSO is PSPACE-complete
• Download full text (pdf) of Parameterized verification under TSO is PSPACE-complete

Optimal stateless model checking for reads-from equivalence under sequential consistency

Abdulla, Parosh; Atig, Mohamed Faouzi; Jonsson, Bengt; Lång, Magnus et al.

Part of Proceedings of the ACM on Programming Languages, p. 1-29, 2019

• DOI for Optimal stateless model checking for reads-from equivalence under sequential consistency
• Download full text (pdf) of Optimal stateless model checking for reads-from equivalence under sequential consistency

Optimal Stateless Model Checking under the Release-Acquire Semantics

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Jonsson, Bengt; Ngo, Tuan-Phong

Part of Proceedings of the ACM on Programming Languages, p. 1-29, 2018

• DOI for Optimal Stateless Model Checking under the Release-Acquire Semantics
• Download full text (pdf) of Optimal Stateless Model Checking under the Release-Acquire Semantics

A load-buffer semantics for total store ordering

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Ngo, Tuan Phong

Part of Logical Methods in Computer Science, 2018

• DOI for A load-buffer semantics for total store ordering

Mending fences with self-invalidation and self-downgrade

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Kaxiras, Stefanos; Leonardsson, Carl et al.

Part of Logical Methods in Computer Science, 2018

• DOI for Mending fences with self-invalidation and self-downgrade

Flatten and Conquer: A Framework for Efficient Analysis of String Constraints

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Bui, Phi Diep et al.

Part of SIGPLAN notices, p. 602-617, 2017

• DOI for Flatten and Conquer: A Framework for Efficient Analysis of String Constraints

Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete

Atig, Mohamed Faouzi; Bollig, Benedikt; Habermehl, Peter

Part of International Journal of Foundations of Computer Science, p. 945-975, 2017

• DOI for Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete

Stateless model checking for TSO and PSO

Abdulla, Parosh Aziz; Aronis, Stavros; Atig, Mohamed Faouzi; Jonsson, Bengt et al.

Part of Acta Informatica, p. 789-818, 2017

• DOI for Stateless model checking for TSO and PSO

Adjacent Ordered Multi-Pushdown Systems

Atig, Mohamed Faouzi; Kumar, K. Narayan; Shivasan, Prakash

Part of International Journal of Foundations of Computer Science, p. 1083-1096, 2014

• DOI for Adjacent Ordered Multi-Pushdown Systems

Budget-bounded model-checking pushdown systems

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rezine, Othmane; Stenman, Jari

Part of Formal methods in system design, p. 273-301, 2014

• DOI for Budget-bounded model-checking pushdown systems

Model-Checking of Ordered Multi-Pushdown Automata

Atig, Mohamed Faouzi

Part of Logical Methods in Computer Science, p. 20, 2012

• DOI for Model-Checking of Ordered Multi-Pushdown Automata

Context-bounded analysis for concurrent programs with dynamic creation of threads

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Qadeer, Shaz

Part of Logical Methods in Computer Science, 2011

• DOI for Context-bounded analysis for concurrent programs with dynamic creation of threads

On Yen's path logic for Petri nets

Atig, Mohamed Faouzi; Habermehl, Peter

Part of International Journal of Foundations of Computer Science, p. 783-799, 2011

• DOI for On Yen's path logic for Petri nets

Verifying parallel programs with dynamic communication structures

Touili, Tayssir; Atig, Mohamed Faouzi

Part of Theoretical Computer Science, p. 3460-3468, 2010

• DOI for Verifying parallel programs with dynamic communication structures

Fairness and Liveness Under Weak Consistency

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Godbole, Adwait; Shankaranarayanan, Krishna et al.

Part of Taming the Infinities of Concurrency, p. 1-21, Springer, 2024

• DOI for Fairness and Liveness Under Weak Consistency

Trading Space for Simplicity in Stateless Model Checking

Abdulla, Parosh; Atig, Mohamed Faouzi; Das, Sarbojit; Jonsson, Bengt et al.

Part of Real Time and Such, p. 79-97, Springer, 2024

• DOI for Trading Space for Simplicity in Stateless Model Checking

Consistency and Persistency in Program Verification: Challenges and Opportunities

Abdulla, Parosh; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Jonsson, Bengt et al.

Part of Principles of Systems Design, p. 494-510, Springer, 2022

• DOI for Consistency and Persistency in Program Verification: Challenges and Opportunities

Checking Consistency of Event-Driven Traces

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rajanbabu, Govind; Grahn, Samuel et al.

Part of Programming Languages and Systems, p. 173-194, 2026

• DOI for Checking Consistency of Event-Driven Traces
• Download full text (pdf) of Checking Consistency of Event-Driven Traces

When GNNs Met a Word Equations Solver: Learning to Rank Equations

Abdulla, Parosh; Atig, Mohamed Faouzi; Cailler, Julie; Liang, Chencheng et al.

Part of Frontiers of Combining Systems (FroCoS 2025), p. 327-345, 2025

• DOI for When GNNs Met a Word Equations Solver: Learning to Rank Equations

Verification of the Release-Acquire Semantics

Abdulla, Parosh; Anastasiadi, Elli; Atig, Mohamed Faouzi; Grahn, Samuel

Part of Theoretical Aspects of Computing - ICTAC 2025 - 22nd International Colloquium, Marrakech, Morocco, November 24-28, 2025, Proceedings, p. 106-123, 2025

• DOI for Verification of the Release-Acquire Semantics

Guiding Word Equation Solving using Graph Neural Networks

Abdulla, Parosh; Atig, Mohamed Faouzi; Cailler, Julie; Liang, Chencheng et al.

Part of Automated Technology for Verification and Analysi, p. 279-301, 2024

• DOI for Guiding Word Equation Solving using Graph Neural Networks

Parsimonious Optimal Dynamic Partial Order Reduction

Abdulla, Parosh; Atig, Mohamed Faouzi; Das, Sarbojit; Jonsson, Bengt et al.

2024

• Download full text (pdf) of Parsimonious Optimal Dynamic Partial Order Reduction

Parsimonious Optimal Dynamic Partial Order Reduction

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Das, Sarbojit; Jonsson, Bengt et al.

Part of COMPUTER AIDED VERIFICATION, PT II, CAV 2024, p. 19-43, 2024

• DOI for Parsimonious Optimal Dynamic Partial Order Reduction
• Download full text (pdf) of Parsimonious Optimal Dynamic Partial Order Reduction

Verification under TSO with an infinite Data Domain

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Furbach, Florian; Garg, Shashwat

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 276-295, 2024

• DOI for Verification under TSO with an infinite Data Domain
• Download full text (pdf) of Verification under TSO with an infinite Data Domain

Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs

Abdulla, Parosh; Atig, Mohamed Faouzi; Meyer Bønneland, Frederik; Das, Sarbojit et al.

Part of Automated Technology for Verification and Analysis, p. 176-198, 2023

• DOI for Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs
• Download full text (pdf) of Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs

Overcoming Memory Weakness with Unified Fairness: Systematic Verification of Liveness in Weak Memory Models

Abdulla, Parosh; Atig, Mohamed Faouzi; Godbole, Adwait; Krishna, Shankaranarayanan et al.

Part of Computer Aided Verification - 35th International Conference, {CAV} 2023, Paris, France, July 17-22, 2023, Proceedings, Part {I}}, p. 184-205, 2023

• DOI for Overcoming Memory Weakness with Unified Fairness: Systematic Verification of Liveness in Weak Memory Models

Parameterized Verification under TSO with Data Types

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Furbach, Florian; Godbole, Adwait A. et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 588-606, 2023

• DOI for Parameterized Verification under TSO with Data Types
• Download full text (pdf) of Parameterized Verification under TSO with Data Types

Optimal Stateless Model Checking for Causal Consistency

Abdulla, Parosh; Atig, Mohamed Faouzi; Krishna, S.; Gupta, Ashutosh et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 105-125, 2023

• DOI for Optimal Stateless Model Checking for Causal Consistency
• Download full text (pdf) of Optimal Stateless Model Checking for Causal Consistency

Probabilistic Total Store Ordering

Abdulla, Parosh; Atig, Mohamed Faouzi; Agarwal, Raj Aryan; Godbole, Adwait et al.

Part of Programming Languages And Systems, ESOP 2022, p. 317-345, 2022

• DOI for Probabilistic Total Store Ordering
• Download full text (pdf) of Probabilistic Total Store Ordering

Verifying Reachability for TSO Programs with Dynamic Thread Creation

Abdulla, Parosh; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, K. Narayan et al.

Part of Networked Systems, NETYS 2022, p. 283-300, 2022

• DOI for Verifying Reachability for TSO Programs with Dynamic Thread Creation

On the State Reachability Problem for Concurrent Programs Under Power

Abdulla, Parosh; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Derevenetc, Egor et al.

Part of Networked Systems - 8th International Conference, {NETYS} 2020,  Morocco,  Revised Selected Papers, p. 47-59, 2021

• DOI for On the State Reachability Problem for Concurrent Programs Under Power

The Decidability of Verification under PS 2.0

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Godbole, Adwait; Krishna, S. et al.

Part of Programming Languages And Systems, ESOP 2021, p. 1-29, 2021

• DOI for The Decidability of Verification under PS 2.0
• Download full text (pdf) of The Decidability of Verification under PS 2.0

Solving Not-Substring Constraint with Flat Abstraction

Abdulla, Parosh; Atig, Mohamed Faouzi; Chen, Yu-Fang; Diep, Bui Phi et al.

Part of Programming Languages And Systems,  APLAS 2021, p. 305-320, 2021

• DOI for Solving Not-Substring Constraint with Flat Abstraction

On the Separability Problem of String Constraints

Abdulla, Parosh; Atig, Mohamed Faouzi; Dave, Vrunda; Krishna, Shankara Narayanan

Part of 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), 2020

• DOI for On the Separability Problem of String Constraints

On the Formalization of Decentralized Contact Tracing Protocols

Abdulla, Parosh; Atig, Mohamed Faouzi; Delzanno, Giorgio; Montali, Marco et al.

Part of Proceedings of the 2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the Bolzano Summer of Knowledge 2020 {(BOSK} 2020), September 25, 2020, p. 65-70, 2020

Boosting Sequential Consistency Checking Using Saturation

Zennou, Rachid; Atig, Mohamed Faouzi; Biswas, Ranadeep; Bouajjani, Ahmed et al.

Part of Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings, p. 360-376, 2020

• DOI for Boosting Sequential Consistency Checking Using Saturation

Efficient Handling of String-Number Conversion

Abdulla, Parosh; Atig, Mohamed Faouzi; Chen, Yu-Fang; Bui, Phi Diep et al.

Part of PLDI 2020, p. 943-957, 2020

• DOI for Efficient Handling of String-Number Conversion

Chain-Free String Constraints

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Phi Diep, Bui; Holik, Lukas et al.

Part of Automated Technology for Verification and Analysis, p. 277-293, 2019

• DOI for Chain-Free String Constraints

Reachability in database-driven systems with numerical attributes under recency bounding

Abdulla, Parosh Aziz; Cyriac, Aiswarya; Atig, Mohamed Faouzi; Montali, Marco

Part of PODS '19, p. 335-352, 2019

• DOI for Reachability in database-driven systems with numerical attributes under recency bounding

Verification of programs under the release-acquire semantics

Abdulla, Parosh Aziz; Arora, Jatin; Atig, Mohamed Faouzi; Krishna, Shankaranarayanan

Part of Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, p. 1117-1132, 2019

• DOI for Verification of programs under the release-acquire semantics

Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Jonsson, Bengt; Ngo, Tuan-Phong

Part of Networked Systems, p. 3-18, 2019

• DOI for Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)

Optimal Stateless Model Checking under the Release-Acquire Semantics

Abdulla, Parosh; Atig, Mohamed Faouzi; Jonsson, Bengt; Ngo, Tuan-Phong

Part of SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018, 2018

• DOI for Optimal Stateless Model Checking under the Release-Acquire Semantics

Replacing store buffers by load buffers in TSO

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Ngo, Tuan Phong

Part of Verification and Evaluation of Computer and Communication Systems, p. 22-28, 2018

• DOI for Replacing store buffers by load buffers in TSO

Trau: SMT solver for string constraints

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Bui, Phi Diep et al.

Part of Proceedings of the 2018 18th Conference on Formal Methods in Computer Aided Design (FMCAD), 2018

• DOI for Trau: SMT solver for string constraints

Verification of timed asynchronous programs

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Krishna, Shankara Narayanan; Vaidya, Shaan

Part of IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018

• DOI for Verification of timed asynchronous programs

Universal safety for timed Petri nets is PSPACE-complete

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Ciobanu, Radu; Mayr, Richard et al.

Part of 29th International Conference on Concurrency Theory, 2018

• DOI for Universal safety for timed Petri nets is PSPACE-complete

Verifying quantitative temporal properties of procedural programs

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Narayan Kumar, K.; Saivasan, Prakash

Part of 29th International Conference on Concurrency Theory, 2018

• DOI for Verifying quantitative temporal properties of procedural programs

Complexity of reachability for data-aware dynamic systems

Abdulla, Parosh Aziz; Aiswarya, C.; Atig, Mohamed Faouzi; Montali, Marco et al.

Part of Proc. 18th International Conference on Application of Concurrency to System Design, p. 11-20, 2018

• DOI for Complexity of reachability for data-aware dynamic systems

Perfect timed communication is hard

Abdulla, Parosh; Atig, Mohamed Faouzi; Krishna, Shankara Narayanan

Part of Formal Modeling and Analysis of Timed Systems, p. 91-107, 2018

• DOI for Perfect timed communication is hard

Context-bounded analysis for POWER

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Ngo, Tuan Phong

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 56-74, 2017

• DOI for Context-bounded analysis for POWER

Data Multi-Pushdown Automata

Aziz Abdulla, Parosh; Aiswarya, C.; Atig, Mohamed Faouzi

Part of The 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, 2017

• DOI for Data Multi-Pushdown Automata

On the Upward/Downward Closures of Petri Nets∗

Atig, Mohamed Faouzi; Meyer, Roland; Muskalla, Sebastian; Saivasan, Prakash

Part of 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), 2017

• DOI for On the Upward/Downward Closures of Petri Nets∗

Verification of Asynchronous Programs with Nested Locks

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, K. Narayan; Saivasan, Prakash

Part of 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India, 2017

Parity Games on Bounded Phase Multi-pushdown Systems

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, K. Narayan; Saivasan, Prakash

Part of Networked Systems: 5th International Conference, NETYS 2017, Marrakech, Morocco, May 17-19, 2017, Proceedings, p. 272-287, 2017

• DOI for Parity Games on Bounded Phase Multi-pushdown Systems

Data Communicating Processes with Unreliable Channels

Abdulla, Parosh Aziz; Cyriac, Aiswarya; Atig, Mohamed Faouzi

Part of Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016), p. 166-175, 2016

• DOI for Data Communicating Processes with Unreliable Channels

The benefits of duality in verifying concurrent programs under TSO

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Ngo, Tuan Phong

Part of 27th International Conference on Concurrency Theory, 2016

• DOI for The benefits of duality in verifying concurrent programs under TSO

Recency-Bounded Verification of Dynamic Database-Driven Systems

Abdulla, Parosh Aziz; Cyriac, Aiswarya; Atig, Mohamed Faouzi; Montali, Marco et al.

Part of PODS'16, p. 195-210, 2016

• DOI for Recency-Bounded Verification of Dynamic Database-Driven Systems

Fencing programs with self-invalidation and self-downgrade

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Kaxiras, Stefanos; Leonardsson, Carl et al.

Part of Formal Techniques for Distributed Objects, Components, and Systems, p. 19-35, 2016

• DOI for Fencing programs with self-invalidation and self-downgrade

Acceleration in Multi-PushDown Systems

Atig, Mohamed Faouzi; Kumar, K. Narayan; Saivasan, Prakash

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 698-714, 2016

• DOI for Acceleration in Multi-PushDown Systems

The complexity of regular abstractions of one-counter languages

Atig, Mohamed Faouzi; Chistikov, Dmitry; Hofman, Piotr; Kumar, K. Narayan et al.

Part of Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016), p. 207-216, 2016

• DOI for The complexity of regular abstractions of one-counter languages

Stateless model checking for POWER

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Jonsson, Bengt; Leonardsson, Carl

Part of Computer Aided Verification, p. 134-156, 2016

• DOI for Stateless model checking for POWER

Counter-Example Guided Program Verification

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Bui, Phi Diep

Part of FM 2016, p. 25-42, 2016

• DOI for Counter-Example Guided Program Verification

The Best of Both Worlds: Trading efficiency and optimality in fence insertion for TSO

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Ngo, Tuan-Phong

Part of Programming Languages and Systems, p. 308-332, 2015

• DOI for The Best of Both Worlds: Trading efficiency and optimality in fence insertion for TSO

Precise and sound automatic fence insertion procedure under PSO

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Lång, Magnus; Ngo, Tuan Phong

Part of Networked Systems, p. 32-47, 2015

• DOI for Precise and sound automatic fence insertion procedure under PSO

Verification of Cache Coherence Protocols wrt. Trace Filters

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Ganjei, Zeinab; Rezine, Ahmed et al.

Part of Proc. 15th Conference on Formal Methods in Computer-Aided Design, p. 9-16, 2015

MPass: An efficient tool for the analysis of message-passing programs

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Cederberg, Jonathan; Modi, Subham et al.

Part of Formal Aspects of Component Software, p. 198-206, 2015

• DOI for MPass: An efficient tool for the analysis of message-passing programs

Stateless model checking for TSO and PSO

Abdulla, Parosh Aziz; Aronis, Stavros; Atig, Mohamed Faouzi; Jonsson, Bengt et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 353-367, 2015

• DOI for Stateless model checking for TSO and PSO

Verification of buffered dynamic register automata

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Kara, Ahmet; Rezine, Othmane

Part of Networked Systems, p. 15-31, 2015

• DOI for Verification of buffered dynamic register automata

What's decidable about availability languages?

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Meyer, Roland; Salehi, Mehdi Seyed

Part of Proc. 35th IARCS Conference on Foundation of Software Technology and Theoretical Computer Science, p. 192-205, 2015

• DOI for What's decidable about availability languages?

Norn: An SMT solver for string constraints

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Holík, Lukás et al.

Part of Computer Aided Verification, p. 462-469, 2015

• DOI for Norn: An SMT solver for string constraints

Activity profiles in online social media

Atig, Mohamed Faouzi; Cassel, Sofia; Kaati, Lisa; Shrestha, Amendra

Part of Proc. 6th International Conference on Advances in Social Networks Analysis and Mining, p. 850-855, 2014

• DOI for Activity profiles in online social media

Verification of Dynamic Register Automata

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Kara, Ahmet; Rezine, Othmane

Part of Leibniz International Proceedings in Informatics, 2014

• Download full text (pdf) of Verification of Dynamic Register Automata

Computing optimal reachability costs in priced dense-timed pushdown automata

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Stenman, Jari

Part of Language and Automata Theory and Applications, p. 62-75, 2014

• DOI for Computing optimal reachability costs in priced dense-timed pushdown automata

Context-Bounded Analysis of TSO Systems

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Parlato, Gennaro

Part of From Programs to Systems, p. 21-38, 2014

• DOI for Context-Bounded Analysis of TSO Systems

String Constraints for Verification

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Holik, Lukas et al.

Part of Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings, p. 150-166, 2014

• DOI for String Constraints for Verification

Infinite-state energy games

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Hofman, Piotr; Mayr, Richard et al.

Part of Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, 2014

• DOI for Infinite-state energy games

On Bounded Reachability Analysis of Shared Memory Systems

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, K. Narayan; Saivasan, Prakash

Part of {IARCS} Annual Conference on Foundations of Software Technology and Theoretical Computer Science, {FSTTCS} 2014, December 15-17, 2014, New Delhi, India, 2014

Zenoness for Timed Pushdown Automata

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Stenman, Jari

Part of Proceedings 15th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2013, Hanoi, Vietnam, 14th October 2013., 2014

• DOI for Zenoness for Timed Pushdown Automata

MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Leonardsson, Carl et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 530-536, 2013

• DOI for MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO
• Download full text (pdf) of MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO

Push-down automata with gap-order constraints

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Delzanno, Giorgio; Podelski, Andreas

Part of Fundamentals of Software Engineering, p. 199-216, 2013

• DOI for Push-down automata with gap-order constraints

Adjacent ordered multi-pushdown systems

Atig, Mohamed Faouzi; Kumar, K. Narayan; Saivasan, Prakash

Part of Developments in Language Theory, p. 58-69, 2013

• DOI for Adjacent ordered multi-pushdown systems

Analysis of message passing programs using SMT-solvers

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Cederberg, Jonathan

Part of Automated Technology for Verification and Analysis, p. 272-286, 2013

• DOI for Analysis of message passing programs using SMT-solvers

Author recognition in discussion boards

Shrestha, Amendra; Kaati, Lisa; Cassel, Sofia; Atig, Mohamed Faouzi

Part of National Symposium on Technology and Methodology for Security and Crisis Management, 2013

Verification of Directed Acyclic Ad Hoc Networks

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rezine, Othmane

Part of Formal Techniques for Distributed Systems, p. 193-208, 2013

• DOI for Verification of Directed Acyclic Ad Hoc Networks
• Download full text (pdf) of Verification of Directed Acyclic Ad Hoc Networks

Dense-Timed Pushdown Automata

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Stenman, Jari

Part of Proc. 27th ACM/IEEE Symposium on Logic in Computer Science, p. 35-44, 2012

• DOI for Dense-Timed Pushdown Automata

Counter-Example Guided Fence Insertion under TSO

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Leonardsson, Carl et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 204-219, 2012

• DOI for Counter-Example Guided Fence Insertion under TSO
• Download full text (pdf) of Counter-Example Guided Fence Insertion under TSO

Automatic fence insertion in integer programs via predicate abstraction

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Leonardsson, Carl et al.

Part of Static Analysis, p. 164-180, 2012

• DOI for Automatic fence insertion in integer programs via predicate abstraction

The minimal cost reachability problem in priced timed pushdown systems

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Stenman, Jari

Part of Language and Automata Theory and Applications, p. 58-69, 2012

• DOI for The minimal cost reachability problem in priced timed pushdown systems

Detecting fair non-termination in multithreaded programs

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Emmi, Michael; Lal, Akash

Part of Computer Aided Verification, p. 210-227, 2012

• Download full text (pdf) of Detecting fair non-termination in multithreaded programs

Timed lossy channel systems

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Cederberg, Jonathan

Part of IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, p. 374-386, 2012

• DOI for Timed lossy channel systems

Multi-Pushdown Systems with Budgets

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Stenman, Jari; Rezine, Othmane

Part of Formal Methods in Computer-Aided Design, p. 24-33, 2012

What's decidable about weak memory models?

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Burckhardt, Sebastian; Musuvathi, Madanlal

Part of Programming Languages and Systems, p. 26-46, 2012

• DOI for What's decidable about weak memory models?

Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, K. Narayan; Saivasan, Prakash

Part of Automated Technology for Verification and Analysis, p. 152-166, 2012

• DOI for Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding

Adding time to pushdown automata

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Stenman, Jari

Part of Quantities in Formal Methods, p. 1-16, 2012

• DOI for Adding time to pushdown automata

Approximating Petri net reachability along context-free traces

Atig, Mohamed Faouzi; Ganty, Pierre

Part of IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, p. 152-163, 2011

• DOI for Approximating Petri net reachability along context-free traces
• Download full text (pdf) of Approximating Petri net reachability along context-free traces

Getting rid of store-buffers in TSO analysis

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Parlato, Gennaro

Part of Computer Aided Verification, p. 99-115, 2011

• DOI for Getting rid of store-buffers in TSO analysis

On the verification problem for weak memory models

Atig, Mohamed Faouzi; Bouajjani, Ahmed; Burckhardt, Sebastian; Musuvathi, Madanlal

Part of Proc. 37th ACM Symposium on Principles of Programming Languages, p. 7-18, 2010

• DOI for On the verification problem for weak memory models

Global model checking of ordered multi-pushdown systems

Atig, Mohamed Faouzi

Part of IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, p. 216-227, 2010

• DOI for Global model checking of ordered multi-pushdown systems

From multi to single stack automata

Atig, Mohamed Faouzi

Part of CONCUR 2010 – Concurrency Theory, p. 117-131, 2010

• DOI for From multi to single stack automata

Verification and Evaluation of Computer and Communication Systems

Atig, Mohamed Faouzi; Bensalem, Saddek; Bliudze, Simon; Monsuez, Bruno

2018

• DOI for Verification and Evaluation of Computer and Communication Systems