Mohamed Faouzi Atig

Checking Consistency of Event-Driven Traces

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

Ingår i Programming Languages and Systems, s. 173-194, 2026

• DOI för Checking Consistency of Event-Driven Traces
• Ladda ner fulltext (pdf) av Checking Consistency of Event-Driven Traces

Parametrised Verification of Intel-x86 Programs

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

Ingår i Proceedings of the ACM on Programming Languages, s. 1094-1122, 2026

• DOI för Parametrised Verification of Intel-x86 Programs
• Ladda ner fulltext (pdf) av 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.

Ingår i Frontiers of Combining Systems (FroCoS 2025), s. 327-345, 2025

• DOI för 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

Ingår i Theoretical Aspects of Computing - ICTAC 2025 - 22nd International Colloquium, Marrakech, Morocco, November 24-28, 2025, Proceedings, s. 106-123, 2025

• DOI för Verification of the Release-Acquire Semantics

Parsimonious Optimal Dynamic Partial Order Reduction

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

Ingår i Computer Aided Verification, PT II, CAV 2024, s. 19-43, 2024

• DOI för Parsimonious Optimal Dynamic Partial Order Reduction
• Ladda ner fulltext (pdf) av Parsimonious Optimal Dynamic Partial Order Reduction

Parametrised Verification of Intel-x86 Programs

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

Ingår i Proceedings of the ACM on Programming Languages, s. 1094-1122, 2026

• DOI för Parametrised Verification of Intel-x86 Programs
• Ladda ner fulltext (pdf) av Parametrised Verification of Intel-x86 Programs

Verification under Intel-x86 with Persistency

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

Ingår i Proceedings of the ACM on Programming Languages, 2024

• DOI för Verification under Intel-x86 with Persistency
• Ladda ner fulltext (pdf) av 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

Ingår i Computing, s. 2157-2157, 2022

• DOI för 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.

Ingår i Proceedings of the ACM on Programming Languages, 2021

• DOI för Deciding Reachability under Persistent x86-TSO
• Ladda ner fulltext (pdf) av Deciding Reachability under Persistent x86-TSO

What is decidable under the TSO memory model?

Atig, Mohamed Faouzi

Ingår i ACM SIGLOG News, s. 4-19, 2020

• DOI för What is decidable under the TSO memory model?

Preface to the VECoS 2018 special issue of ISSE

Atig, Mohamed Faouzi; Bliudze, Simon

Ingår i Innovations in Systems and Software Engineering, s. 99-100, 2020

• DOI för Preface to the VECoS 2018 special issue of ISSE

Parameterized verification under TSO is PSPACE-complete

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

Ingår i Proceedings of the ACM on Programming Languages, 2020

• DOI för Parameterized verification under TSO is PSPACE-complete
• Ladda ner fulltext (pdf) av 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.

Ingår i Proceedings of the ACM on Programming Languages, s. 1-29, 2019

• DOI för Optimal stateless model checking for reads-from equivalence under sequential consistency
• Ladda ner fulltext (pdf) av 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

Ingår i Proceedings of the ACM on Programming Languages, s. 1-29, 2018

• DOI för Optimal Stateless Model Checking under the Release-Acquire Semantics
• Ladda ner fulltext (pdf) av 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

Ingår i Logical Methods in Computer Science, 2018

• DOI för 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.

Ingår i Logical Methods in Computer Science, 2018

• DOI för 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.

Ingår i SIGPLAN notices, s. 602-617, 2017

• DOI för 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

Ingår i International Journal of Foundations of Computer Science, s. 945-975, 2017

• DOI för 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.

Ingår i Acta Informatica, s. 789-818, 2017

• DOI för Stateless model checking for TSO and PSO

Adjacent Ordered Multi-Pushdown Systems

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

Ingår i International Journal of Foundations of Computer Science, s. 1083-1096, 2014

• DOI för Adjacent Ordered Multi-Pushdown Systems

Budget-bounded model-checking pushdown systems

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

Ingår i Formal methods in system design, s. 273-301, 2014

• DOI för Budget-bounded model-checking pushdown systems

Model-Checking of Ordered Multi-Pushdown Automata

Atig, Mohamed Faouzi

Ingår i Logical Methods in Computer Science, s. 20, 2012

• DOI för 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

Ingår i Logical Methods in Computer Science, 2011

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

On Yen's path logic for Petri nets

Atig, Mohamed Faouzi; Habermehl, Peter

Ingår i International Journal of Foundations of Computer Science, s. 783-799, 2011

• DOI för On Yen's path logic for Petri nets

Verifying parallel programs with dynamic communication structures

Touili, Tayssir; Atig, Mohamed Faouzi

Ingår i Theoretical Computer Science, s. 3460-3468, 2010

• DOI för 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.

Ingår i Taming the Infinities of Concurrency, s. 1-21, Springer, 2024

• DOI för 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.

Ingår i Real Time and Such, s. 79-97, Springer, 2024

• DOI för 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.

Ingår i Principles of Systems Design, s. 494-510, Springer, 2022

• DOI för 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.

Ingår i Programming Languages and Systems, s. 173-194, 2026

• DOI för Checking Consistency of Event-Driven Traces
• Ladda ner fulltext (pdf) av 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.

Ingår i Frontiers of Combining Systems (FroCoS 2025), s. 327-345, 2025

• DOI för 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

Ingår i Theoretical Aspects of Computing - ICTAC 2025 - 22nd International Colloquium, Marrakech, Morocco, November 24-28, 2025, Proceedings, s. 106-123, 2025

• DOI för Verification of the Release-Acquire Semantics

Parsimonious Optimal Dynamic Partial Order Reduction

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

Ingår i Computer Aided Verification, PT II, CAV 2024, s. 19-43, 2024

• DOI för Parsimonious Optimal Dynamic Partial Order Reduction
• Ladda ner fulltext (pdf) av Parsimonious Optimal Dynamic Partial Order Reduction

Guiding Word Equation Solving using Graph Neural Networks

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

Ingår i Automated Technology for Verification and Analysi, s. 279-301, 2024

• DOI för 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

• Ladda ner fulltext (pdf) av Parsimonious Optimal Dynamic Partial Order Reduction

Verification under TSO with an infinite Data Domain

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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 276-295, 2024

• DOI för Verification under TSO with an infinite Data Domain
• Ladda ner fulltext (pdf) av 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.

Ingår i Automated Technology for Verification and Analysis, s. 176-198, 2023

• DOI för Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs
• Ladda ner fulltext (pdf) av 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.

Ingår i Computer Aided Verification - 35th International Conference, {CAV} 2023, Paris, France, July 17-22, 2023, Proceedings, Part {I}}, s. 184-205, 2023

• DOI för 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.

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 588-606, 2023

• DOI för Parameterized Verification under TSO with Data Types
• Ladda ner fulltext (pdf) av 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.

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 105-125, 2023

• DOI för Optimal Stateless Model Checking for Causal Consistency
• Ladda ner fulltext (pdf) av Optimal Stateless Model Checking for Causal Consistency

Probabilistic Total Store Ordering

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

Ingår i Programming Languages And Systems, ESOP 2022, s. 317-345, 2022

• DOI för Probabilistic Total Store Ordering
• Ladda ner fulltext (pdf) av 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.

Ingår i Networked Systems, NETYS 2022, s. 283-300, 2022

• DOI för 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.

Ingår i Networked Systems - 8th International Conference, {NETYS} 2020,  Morocco,  Revised Selected Papers, s. 47-59, 2021

• DOI för 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.

Ingår i Programming Languages And Systems, ESOP 2021, s. 1-29, 2021

• DOI för The Decidability of Verification under PS 2.0
• Ladda ner fulltext (pdf) av 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.

Ingår i Programming Languages And Systems,  APLAS 2021, s. 305-320, 2021

• DOI för Solving Not-Substring Constraint with Flat Abstraction

On the Separability Problem of String Constraints

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

Ingår i 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), 2020

• DOI för 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.

Ingår i 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, s. 65-70, 2020

Boosting Sequential Consistency Checking Using Saturation

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

Ingår i Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings, s. 360-376, 2020

• DOI för 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.

Ingår i PLDI 2020, s. 943-957, 2020

• DOI för Efficient Handling of String-Number Conversion

Chain-Free String Constraints

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

Ingår i Automated Technology for Verification and Analysis, s. 277-293, 2019

• DOI för 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

Ingår i PODS '19, s. 335-352, 2019

• DOI för 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

Ingår i Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, s. 1117-1132, 2019

• DOI för 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

Ingår i Networked Systems, s. 3-18, 2019

• DOI för 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

Ingår i SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018, 2018

• DOI för 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

Ingår i Verification and Evaluation of Computer and Communication Systems, s. 22-28, 2018

• DOI för 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.

Ingår i Proceedings of the 2018 18th Conference on Formal Methods in Computer Aided Design (FMCAD), 2018

• DOI för Trau: SMT solver for string constraints

Verification of timed asynchronous programs

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

Ingår i IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018

• DOI för 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.

Ingår i 29th International Conference on Concurrency Theory, 2018

• DOI för 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

Ingår i 29th International Conference on Concurrency Theory, 2018

• DOI för 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.

Ingår i Proc. 18th International Conference on Application of Concurrency to System Design, s. 11-20, 2018

• DOI för Complexity of reachability for data-aware dynamic systems

Perfect timed communication is hard

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

Ingår i Formal Modeling and Analysis of Timed Systems, s. 91-107, 2018

• DOI för Perfect timed communication is hard

Context-bounded analysis for POWER

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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 56-74, 2017

• DOI för Context-bounded analysis for POWER

Data Multi-Pushdown Automata

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

Ingår i The 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, 2017

• DOI för Data Multi-Pushdown Automata

On the Upward/Downward Closures of Petri Nets∗

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

Ingår i 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), 2017

• DOI för 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

Ingår i 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

Ingår i Networked Systems: 5th International Conference, NETYS 2017, Marrakech, Morocco, May 17-19, 2017, Proceedings, s. 272-287, 2017

• DOI för Parity Games on Bounded Phase Multi-pushdown Systems

Data Communicating Processes with Unreliable Channels

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

Ingår i Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016), s. 166-175, 2016

• DOI för 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

Ingår i 27th International Conference on Concurrency Theory, 2016

• DOI för 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.

Ingår i PODS'16, s. 195-210, 2016

• DOI för 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.

Ingår i Formal Techniques for Distributed Objects, Components, and Systems, s. 19-35, 2016

• DOI för Fencing programs with self-invalidation and self-downgrade

Acceleration in Multi-PushDown Systems

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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 698-714, 2016

• DOI för 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.

Ingår i Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016), s. 207-216, 2016

• DOI för The complexity of regular abstractions of one-counter languages

Stateless model checking for POWER

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

Ingår i Computer Aided Verification, s. 134-156, 2016

• DOI för Stateless model checking for POWER

Counter-Example Guided Program Verification

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

Ingår i FM 2016, s. 25-42, 2016

• DOI för 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

Ingår i Programming Languages and Systems, s. 308-332, 2015

• DOI för 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

Ingår i Networked Systems, s. 32-47, 2015

• DOI för 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.

Ingår i Proc. 15th Conference on Formal Methods in Computer-Aided Design, s. 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.

Ingår i Formal Aspects of Component Software, s. 198-206, 2015

• DOI för 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.

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 353-367, 2015

• DOI för Stateless model checking for TSO and PSO

Verification of buffered dynamic register automata

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

Ingår i Networked Systems, s. 15-31, 2015

• DOI för Verification of buffered dynamic register automata

What's decidable about availability languages?

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

Ingår i Proc. 35th IARCS Conference on Foundation of Software Technology and Theoretical Computer Science, s. 192-205, 2015

• DOI för 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.

Ingår i Computer Aided Verification, s. 462-469, 2015

• DOI för Norn: An SMT solver for string constraints

Activity profiles in online social media

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

Ingår i Proc. 6th International Conference on Advances in Social Networks Analysis and Mining, s. 850-855, 2014

• DOI för Activity profiles in online social media

Verification of Dynamic Register Automata

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

Ingår i Leibniz International Proceedings in Informatics, 2014

• Ladda ner fulltext (pdf) av Verification of Dynamic Register Automata

Computing optimal reachability costs in priced dense-timed pushdown automata

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

Ingår i Language and Automata Theory and Applications, s. 62-75, 2014

• DOI för Computing optimal reachability costs in priced dense-timed pushdown automata

Context-Bounded Analysis of TSO Systems

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

Ingår i From Programs to Systems, s. 21-38, 2014

• DOI för Context-Bounded Analysis of TSO Systems

String Constraints for Verification

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

Ingår i 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, s. 150-166, 2014

• DOI för String Constraints for Verification

Infinite-state energy games

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

Ingår i 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 för Infinite-state energy games

On Bounded Reachability Analysis of Shared Memory Systems

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

Ingår i {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

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

• DOI för 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.

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 530-536, 2013

• DOI för MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO
• Ladda ner fulltext (pdf) av 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

Ingår i Fundamentals of Software Engineering, s. 199-216, 2013

• DOI för Push-down automata with gap-order constraints

Adjacent ordered multi-pushdown systems

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

Ingår i Developments in Language Theory, s. 58-69, 2013

• DOI för Adjacent ordered multi-pushdown systems

Analysis of message passing programs using SMT-solvers

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

Ingår i Automated Technology for Verification and Analysis, s. 272-286, 2013

• DOI för Analysis of message passing programs using SMT-solvers

Author recognition in discussion boards

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

Ingår i 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

Ingår i Formal Techniques for Distributed Systems, s. 193-208, 2013

• DOI för Verification of Directed Acyclic Ad Hoc Networks
• Ladda ner fulltext (pdf) av Verification of Directed Acyclic Ad Hoc Networks

Dense-Timed Pushdown Automata

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

Ingår i Proc. 27th ACM/IEEE Symposium on Logic in Computer Science, s. 35-44, 2012

• DOI för Dense-Timed Pushdown Automata

Counter-Example Guided Fence Insertion under TSO

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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 204-219, 2012

• DOI för Counter-Example Guided Fence Insertion under TSO
• Ladda ner fulltext (pdf) av 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.

Ingår i Static Analysis, s. 164-180, 2012

• DOI för 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

Ingår i Language and Automata Theory and Applications, s. 58-69, 2012

• DOI för 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

Ingår i Computer Aided Verification, s. 210-227, 2012

• Ladda ner fulltext (pdf) av Detecting fair non-termination in multithreaded programs

Timed lossy channel systems

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

Ingår i IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, s. 374-386, 2012

• DOI för Timed lossy channel systems

Multi-Pushdown Systems with Budgets

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

Ingår i Formal Methods in Computer-Aided Design, s. 24-33, 2012

What's decidable about weak memory models?

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

Ingår i Programming Languages and Systems, s. 26-46, 2012

• DOI för 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

Ingår i Automated Technology for Verification and Analysis, s. 152-166, 2012

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

Adding time to pushdown automata

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

Ingår i Quantities in Formal Methods, s. 1-16, 2012

• DOI för Adding time to pushdown automata

Approximating Petri net reachability along context-free traces

Atig, Mohamed Faouzi; Ganty, Pierre

Ingår i IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, s. 152-163, 2011

• DOI för Approximating Petri net reachability along context-free traces
• Ladda ner fulltext (pdf) av Approximating Petri net reachability along context-free traces

Getting rid of store-buffers in TSO analysis

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

Ingår i Computer Aided Verification, s. 99-115, 2011

• DOI för 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

Ingår i Proc. 37th ACM Symposium on Principles of Programming Languages, s. 7-18, 2010

• DOI för On the verification problem for weak memory models

Global model checking of ordered multi-pushdown systems

Atig, Mohamed Faouzi

Ingår i IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, s. 216-227, 2010

• DOI för Global model checking of ordered multi-pushdown systems

From multi to single stack automata

Atig, Mohamed Faouzi

Ingår i CONCUR 2010 – Concurrency Theory, s. 117-131, 2010

• DOI för 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 för Verification and Evaluation of Computer and Communication Systems