Parosh Abdulla

On the Verification Problem of Remote Direct Memory Access Programs

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rajanbabu, Govind; Spengler, Stephan

Part of Computer Aided Verification, p. 113-135, 2026

• DOI for On the Verification Problem of Remote Direct Memory Access Programs
• Download full text (pdf) of On the Verification Problem of Remote Direct Memory Access Programs

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

Parameterized Verification of Quantum Circuits

Abdulla, Parosh; Chen, Yu-Fang; Hecko, Michal; Holik, Lukas et al.

Part of Proceedings of the ACM on Programming Languages, p. 2021-2050, 2026

• DOI for Parameterized Verification of Quantum Circuits
• Download full text (pdf) of Parameterized Verification of Quantum Circuits

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

Quantum Circuit Verification - A Potential Roadmap (Invited Talk)

Abdulla, Parosh Aziz; Chen, Yu-Fang; Hecko, Michal; Holík, Lukás et al.

Part of 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2025, p. 1-1, 2025

• DOI for Quantum Circuit Verification - A Potential Roadmap (Invited Talk)
• Download full text (pdf) of Quantum Circuit Verification - A Potential Roadmap (Invited Talk)

Parameterized Verification of Quantum Circuits

Abdulla, Parosh; Chen, Yu-Fang; Hecko, Michal; Holik, Lukas et al.

Part of Proceedings of the ACM on Programming Languages, p. 2021-2050, 2026

• DOI for Parameterized Verification of Quantum Circuits
• Download full text (pdf) of Parameterized Verification of Quantum Circuits

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

Efficient Linearizability Monitoring

Abdulla, Parosh; Grahn, Samuel; Jonsson, Bengt; Krishna, Shankaranarayanan et al.

Part of Proceedings of the ACM on Programming Languages, p. 1937-1960, 2025

• DOI for Efficient Linearizability Monitoring
• Download full text (pdf) of Efficient Linearizability Monitoring

A Symbolic Approach to Verifying Quantum Systems

Abdulla, Parosh Aziz

Part of Communications of the ACM, p. 84-84, 2025

• DOI for A Symbolic Approach to Verifying Quantum Systems
• Download full text (pdf) of A Symbolic Approach to Verifying Quantum Systems

Verifying Quantum Circuits with Level-Synchronized Tree Automata

Abdulla, Parosh; Chen, Yo-Ga; Chen, Yu-Fang; Holik, Lukas et al.

Part of Proceedings of the ACM on Programming Languages, 2025

• DOI for Verifying Quantum Circuits with Level-Synchronized Tree Automata
• Download full text (pdf) of Verifying Quantum Circuits with Level-Synchronized Tree Automata

A Novel Approach to Efficiently Verify Sequential Consistency in Concurrent Programs

Abdulwahhab, Mohammed H.; Abdulla, Parosh; Jacksi, Karwan

Part of Computers, 2025

• DOI for A Novel Approach to Efficiently Verify Sequential Consistency in Concurrent Programs
• Download full text (pdf) of A Novel Approach to Efficiently Verify Sequential Consistency in Concurrent 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

Optimal Reads-From Consistency Checking for C11-Style Memory Models

Tunc, Hunkar Can; Abdulla, Parosh; Chakraborty, Soham; Krishna, Shankaranarayanan et al.

Part of Proceedings of the ACM on Programming Languages, p. 761-785, 2023

• DOI for Optimal Reads-From Consistency Checking for C11-Style Memory Models
• Download full text (pdf) of Optimal Reads-From Consistency Checking for C11-Style Memory Models

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

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

Special Issue on NETYS'2016

Abdulla, Parosh Aziz; Delporte, Carole

Part of Computing, p. 1-2, 2019

• DOI for Special Issue on NETYS'2016

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

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

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

An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures

Abdulla, Parosh; Haziza, Frédéric; Holík, Lukás; Jonsson, Bengt et al.

Part of International Journal on Software Tools for Technology Transfer, p. 549-563, 2017

• DOI for An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures

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

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

Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction

Abdulla, Parosh; Aronis, Stavros; Jonsson, Bengt; Sagonas, Konstantinos

Part of Journal of the ACM, 2017

• DOI for Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction

Verification of heap manipulating programs with ordered data by extended forest automata

Abdulla, Parosh Aziz; Holík, Lukás; Jonsson, Bengt; Lengál, Ondrej et al.

Part of Acta Informatica, p. 357-385, 2016

• DOI for Verification of heap manipulating programs with ordered data by extended forest automata

Parameterized verification through view abstraction

Abdulla, Parosh Aziz; Haziza, Frédéric; Holík, Lukás

Part of International Journal on Software Tools for Technology Transfer, p. 495-516, 2016

• DOI for Parameterized verification through view abstraction

Parameterized verification

Abdulla, Parosh A.; Delzanno, Giorgio

Part of International Journal on Software Tools for Technology Transfer, p. 469-473, 2016

• DOI for Parameterized verification

Parameterized verification of time-sensitive models of ad hoc network protocols

Abdulla, Parosh Aziz; Delzanno, Giorgio; Rezine, Othmane; Sangnier, Arnaud et al.

Part of Theoretical Computer Science, p. 1-22, 2016

• DOI for Parameterized verification of time-sensitive models of ad hoc network protocols

Well Structured Transition Systems with History

Abdulla, Parosh A.; Delzanno, Giorgio; Montali, Marco

Part of Electronic Proceedings in Theoretical Computer Science, p. 115-128, 2015

• DOI for Well Structured Transition Systems with History

Stochastic Parity Games on Lossy Channel Systems

Abdulla, Parosh Aziz; Clemente, Lorenzo; Mayr, Richard; Sandberg, Sven

Part of Logical Methods in Computer Science, 2014

• DOI for Stochastic Parity Games on Lossy Channel Systems
• Download full text (pdf) of Stochastic Parity Games on Lossy Channel 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

Mediating for reduction (on minimizing alternating Buchi automata)

Abdulla, Parosh Aziz; Chen, Yu-Fang; Holik, Lukag; Vojnar, Tomas

Part of Theoretical Computer Science, p. 26-43, 2014

• DOI for Mediating for reduction (on minimizing alternating Buchi automata)

Priced timed Petri nets

Abdulla, Parosh Aziz; Mayr, Richard

Part of Logical Methods in Computer Science, 2013

• DOI for Priced timed Petri nets

Monotonic abstraction for programs with multiply-linked structures

Abdulla, Parosh Aziz; Cederberg, Jonathan; Vojnar, Tomás

Part of International Journal of Foundations of Computer Science, p. 187-210, 2013

• DOI for Monotonic abstraction for programs with multiply-linked structures
• Download full text (pdf) of Monotonic abstraction for programs with multiply-linked structures

Regular model checking for LTL(MSO)

Abdulla, Parosh; Jonsson, Bengt; Nilsson, Marcus; d'Orso, Julien et al.

Part of International Journal on Software Tools for Technology Transfer, p. 223-241, 2012

• DOI for Regular model checking for LTL(MSO)

Regular model checking

Abdulla, Parosh Aziz

Part of International Journal on Software Tools for Technology Transfer, p. 109-118, 2012

• DOI for Regular model checking

Automatic verification of directory-based consistency protocols with graph constraints

Abdulla, Parosh Aziz; Delzanno, Giorgio; Rezine, Ahmed

Part of International Journal of Foundations of Computer Science, p. 761-782, 2011

• DOI for Automatic verification of directory-based consistency protocols with graph constraints

A classification of the expressive power of well-structured transition systems

Abdulla, Parosh Aziz; Delzanno, Giorgio; Van Begin, Laurent

Part of Information and Computation, p. 248-279, 2011

• DOI for A classification of the expressive power of well-structured transition systems

Sampled semantics of timed automata

Abdulla, Parosh Aziz; Krcal, Pavel; Yi, Wang

Part of Logical Methods in Computer Science, 2010

• DOI for Sampled semantics of timed automata

Well (and better) quasi-ordered transition systems

Abdulla, Parosh Aziz

Part of Bulletin of Symbolic Logic, p. 457-515, 2010

Universality of R-automata with value copying

Abdulla, Parosh Aziz; Krcal, Pavel; Yi, Wang

Part of Electronic Notes in Theoretical Computer Science, p. 131-141, 2009

• DOI for Universality of R-automata with value copying

A uniform (bi-)simulation-based framework for reducing tree automata

Abdulla, Parosh Aziz; Holík, Lukás; Kaati, Lisa; Vojnar, Tomás

Part of Electronic Notes in Theoretical Computer Science, p. 27-48, 2009

• DOI for A uniform (bi-)simulation-based framework for reducing tree automata

Monotonic Abstraction: on Efficient Verification of Parameterized Systems

Abdulla, Aziz; Delzanno, Giorgio; Henda, Ben; Rezine, Ahmed

Part of International Journal of Foundations of Computer Science, p. 779-801, 2009

• DOI for Monotonic Abstraction: on Efficient Verification of Parameterized Systems

Composed bisimulation for tree automata

Abdulla, Parosh Aziz; Bouajjani, Ahmed; Holík, Lukás; Kaati, Lisa et al.

Part of International Journal of Foundations of Computer Science, p. 685-700, 2009

• DOI for Composed bisimulation for tree automata

Approximated parameterized verification of infinite-state processes with global conditions

Abdulla, Aziz; Delzanno, Giorgio; Rezine, Ahmed

Part of Formal methods in system design, p. 126-156, 2009

• DOI for Approximated parameterized verification of infinite-state processes with global conditions

Monotonic Abstraction in Parameterized Verification

Abdulla, Aziz; Delzanno, Giorgio; Rezine, Ahmed

Part of Electronic Notes in Theoretical Computer Science, p. 3-14, 2008

• DOI for Monotonic Abstraction in Parameterized Verification

Model checking race-freeness

Abdulla, Parosh Aziz; Haziza, Frédéric; Kindahl, Mats

Part of SIGARCH Computer Architecture News, p. 72-79, 2008

• DOI for Model checking race-freeness

Monotonic and downward closed games

Abdulla, Parosh Aziz; Bouajjani, Ahmed; d'Orso, Julien

Part of Journal of logic and computation (Print), p. 153-169, 2008

• DOI for Monotonic and downward closed games

Universality Analysis for One-Clock Timed Automata

Abdulla, Parosh Aziz; Deneux, Johann; Ouaknine, Joel; Quaas, Karin et al.

Part of Fundamenta Informaticae, p. 419-450, 2008

Decisive Markov Chains

Abdulla, Parosh; Ben Henda, Noomene; Mayr, Richard

Part of Logical Methods in Computer Science, p. 1-32, 2007

• DOI for Decisive Markov Chains

Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness

Abdulla, Parosh Aziz; Mahata, Pritha; Mayr, Richard

Part of Logical Methods in Computer Science, p. 1-61, 2007

• DOI for Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness

Using Forward Reachability Analysis for Verification of Timed Petri Nets

Abdulla, Parosh Aziz; Deneux, Johann; Mahata, Pritha; Nylén, Aletta

Part of Nordic Journal of Computing, p. 1-42, 2007

Bisimulation minimization of tree automata

Abdulla, Parosh Aziz; Högberg, Johanna; Kaati, Lisa

Part of International Journal of Foundations of Computer Science, p. 699-713, 2007

• DOI for Bisimulation minimization of tree automata

Simulating perfect channels with probabilistic lossy channels

Abdulla, Parosh; Baier, Christel; Iyer, S. Purushotaman; Jonsson, Bengt

Part of Information and Computation, p. 22-40, 2005

Using Forward Reachability Analysis for Verification of Lossy Channel Systems

Abdulla, Parosh Aziz; Collomb-Annichini, Aurore; Bouajjani, Ahmed; Jonsson, Bengt

Part of Formal methods in system design, p. 39-65, 2004

• DOI for Using Forward Reachability Analysis for Verification of Lossy Channel Systems

SAT-solving the Coverability Problem for Unbounded Petri Nets

Abdulla, Parosh; Iyer, Purushothaman; Nylén, Aletta

Part of Formal methods in system design, p. 25-43, 2004

Model checking of systems with many identical timed processes

Abdulla, Parosh; Jonsson, Bengt

Part of Theoretical Computer Science, p. 241-264, 2003

• DOI for Model checking of systems with many identical timed processes

Algorithmic analysis of programs with well quasi-ordered domains

Abdulla, PA; Cerans, K; Jonsson, B; Tsay, YK

Part of INFORMATION AND COMPUTATION, p. 109-127, 2000

Verifying programs with unreliable channels

Abdulla, PA; Jonsson, B

Part of Information and Computation, p. 91-101, 1996

• DOI for Verifying programs with unreliable channels

Tools for software verification: Introduction to the special section from the seventeenth international conference on tools and algorithms for the construction and analysis of systems

Abdulla, Parosh Aziz; Leino, K. Rustan M.

Part of International Journal on Software Tools for Technology Transfer, p. 85-88, 2013

• DOI for Tools for software verification: Introduction to the special section from the seventeenth international conference on tools and algorithms for the construction and analysis of systems

On the Verification of Quantum Circuits (Research Challenges and Opportunities)

Abdulla, Parosh; Chen, Yo-Ga; Chen, Yu-Fang; Chung, Kai-Min et al.

Part of Principles of Formal Quantitative Analysis, p. 320-341, Springer Nature, 2025

• DOI for On the Verification of Quantum Circuits (Research Challenges and Opportunities)

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

Model checking parameterized systems

Abdulla, Parosh Aziz; Sistla, A. Prasad; Talupur, Muralidhar

Part of Handbook of Model Checking, p. 685-725, Springer, 2018

• DOI for Model checking parameterized systems

Comparing source sets and persistent sets for partial order reduction

Abdulla, Parosh; Aronis, Stavros; Jonsson, Bengt; Sagonas, Konstantinos

Part of Models, Algorithms, Logics and Tools, p. 516-536, Springer, 2017

• DOI for Comparing source sets and persistent sets for partial order reduction

On the existence of network invariants for verifying parameterized systems

Abdulla, Parosh; Jonsson, Bengt

Part of Correct System Design, p. 180-197, Springer-Verlag, Berlin, 1999

On the Verification Problem of Remote Direct Memory Access Programs

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rajanbabu, Govind; Spengler, Stephan

Part of Computer Aided Verification, p. 113-135, 2026

• DOI for On the Verification Problem of Remote Direct Memory Access Programs
• Download full text (pdf) of On the Verification Problem of Remote Direct Memory Access Programs

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

Quantum Circuit Verification - A Potential Roadmap (Invited Talk)

Abdulla, Parosh Aziz; Chen, Yu-Fang; Hecko, Michal; Holík, Lukás et al.

Part of 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2025, p. 1-1, 2025

• DOI for Quantum Circuit Verification - A Potential Roadmap (Invited Talk)
• Download full text (pdf) of Quantum Circuit Verification - A Potential Roadmap (Invited Talk)

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

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 - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings, p. 327-345, 2025

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

Checking Consistency of Event-Driven Traces

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

Part of Programming Languages and Systems - 23rd Asian Symposium, APLAS 2025, Bengaluru, India, October 27-30, 2025, Proceedings, p. 173-194, 2025

• DOI for Checking Consistency of Event-Driven Traces

Dynamic Partial Order Reduction for Transactional Programs on Serializable Platforms

Abdulla, Parosh; Gupta, Ashutosh; Krishna, Shankara Narayanan; Tuppe, Omkar

Part of Automated technology for verification and analysis, ATVA 2024, pt i, p. 181-202, 2025

• DOI for Dynamic Partial Order Reduction for Transactional Programs on Serializable Platforms

Parsimonious Optimal Dynamic Partial Order Reduction

Abdulla, Parosh; 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

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

Boosting Constrained Horn Solving by Unsat Core Learning

Abdulla, Parosh Aziz; Liang, Chencheng; Rümmer, Philipp

Part of Verification, Model Checking, and Abstract Interpretation, p. 280-302, 2024

• DOI for Boosting Constrained Horn Solving by Unsat Core Learning

Concurrent Stochastic Lossy Channel Games

Stan, Daniel; Najib, Muhammad; Widjaja Lin, Anthony; Abdulla, Parosh Aziz

Part of 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), 2024

• DOI for Concurrent Stochastic Lossy Channel Games
• Download full text (pdf) of Concurrent Stochastic Lossy Channel Games

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

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

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

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

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

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

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

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

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

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

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

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

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

Fragment abstraction for concurrent shape analysis

Abdulla, Parosh Aziz; Jonsson, Bengt; Trinh, Cong Quy

Part of Programming Languages and Systems, p. 442-471, 2018

• DOI for Fragment abstraction for concurrent shape analysis

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

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

Automated Verification of Linearization Policies

Abdulla, Parosh; Jonsson, Bengt; Trinh, Cong Quy

Part of Automated Verification of Linearization Policies, 2016

• DOI for Automated Verification of Linearization Policies

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

Qualitative Analysis of VASS-Induced MDPs

Abdulla, Parosh; Ciobanu, Radu; Mayr, Richard; Sangnier, Arnaud et al.

Part of Foundations Of Software Science And Computation Structures (FOSSACS 2016), p. 319-334, 2016

• DOI for Qualitative Analysis of VASS-Induced MDPs

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

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

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

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

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

Optimal dynamic partial order reduction

Abdulla, Parosh; Aronis, Stavros; Jonsson, Bengt; Sagonas, Konstantinos

Part of Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 373-384, 2014

• DOI for Optimal dynamic partial order reduction

Block me if you can!: Context-sensitive parameterized verification

Abdulla, Parosh Aziz; Haziza, Frédéric; Holík, Lukás

Part of Static Analysis, p. 1-17, 2014

• DOI for Block me if you can!: Context-sensitive parameterized verification
• Download full text (pdf) of Block me if you can!: Context-sensitive parameterized verification

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

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

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

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

Verifying safety and liveness for the FlexTM hybrid transactional memory

Abdulla, Parosh Aziz; Dwarkadas, Sandhya; Rezine, Ahmed; Shriraman, Arrvindh et al.

p. 785-790, 2013

Verification of heap manipulating programs with ordered data by extended forest automata

Abdulla, Parosh Aziz; Holík, Lukás; Jonsson, Bengt; Lengál, Ondrej et al.

Part of Automated Technology for Verification and Analysis, p. 224-239, 2013

• DOI for Verification of heap manipulating programs with ordered data by extended forest automata
• Download full text (pdf) of Verification of heap manipulating programs with ordered data by extended forest automata

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

Solving parity games on integer vectors

Abdulla, Parosh Aziz; Mayr, Richard; Sangnier, Arnaud; Sproston, Jeremy

Part of CONCUR 2013 – Concurrency Theory, p. 106-120, 2013

• DOI for Solving parity games on integer vectors

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

An Integrated Specification and Verification Technique for Highly Concurrent Data Structures

Abdulla, Parosh Aziz; Haziza, Frédéric; Holik, Lukas; Jonsson, Bengt et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, 2013

• Download full text (pdf) of An Integrated Specification and Verification Technique for Highly Concurrent Data Structures

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

All for the price of few: (Parameterized verification through view abstraction)

Abdulla, Parosh Aziz; Haziza, Frédéric; Holík, Lukáš

Part of Verification, Model Checking, and Abstract Interpretation, p. 476-495, 2013

• DOI for All for the price of few: (Parameterized verification through view abstraction)
• Download full text (pdf) of All for the price of few: (Parameterized verification through view abstraction)

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

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

Petri Nets with Time and Cost

Abdulla, Parosh Aziz; Richard, Mayr

2012

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

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

On the verification of timed ad hoc networks

Abdulla, Parosh Aziz; Delzanno, Giorgio; Rezine, Othmane; Sangnier, Arnaud et al.

Part of Formal Modeling and Analysis of Timed Systems, p. 256-270, 2011

• DOI for On the verification of timed ad hoc networks

Computing Optimal Coverability Costs in Priced Timed Petri Nets

Abdulla, Parosh Aziz; Richard, Mayr

Part of LICS'2011, Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, p. 399-408, 2011

• DOI for Computing Optimal Coverability Costs in Priced Timed Petri Nets

Advanced Ramsey-based Büchi automata inclusion testing

Abdulla, Parosh Aziz; Chen, Yu-Fang; Clemente, Lorenzo; Holík, Lukás et al.

Part of CONCUR 2011 — Concurrency Theory, p. 187-202, 2011

• DOI for Advanced Ramsey-based Büchi automata inclusion testing

Carrying Probabilities to the Infinite World

Abdulla, Parosh Aziz

Part of CONCUR'2011, 22nd International Conference on Concurrency Theory., 2011

Forcing monotonicity in parameterized verification: From multisets to words

Abdulla, Parosh Aziz

Part of SOFSEM 2010, p. 1-15, 2010

• DOI for Forcing monotonicity in parameterized verification: From multisets to words

When simulation meets antichains: On checking language inclusion of nondeterministic finite (tree) automata

Abdulla, Parosh Aziz; Chen, Yu-Fang; Holík, Lukás; Mayr, Richard et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 158-174, 2010

• DOI for When simulation meets antichains: On checking language inclusion of nondeterministic finite (tree) automata

Simulation subsumption in Ramsey-based Büchi automata universality and inclusion testing

Abdulla, Parosh Aziz; Chen, Yu-Fang; Clemente, Lorenzo; Holík, Lukás et al.

Part of Computer Aided Verification, p. 132-147, 2010

• DOI for Simulation subsumption in Ramsey-based Büchi automata universality and inclusion testing

Analyzing the security in the GSM radio network using attack jungles

Abdulla, Parosh Aziz; Cederberg, Jonathan; Kaati, Lisa

Part of Leveraging Applications of Formal Methods, Verification, and Validation, p. 60-74, 2010

• DOI for Analyzing the security in the GSM radio network using attack jungles

Constrained monotonic abstraction: A CEGAR for parameterized verification

Abdulla, Parosh Aziz; Chen, Yu-Fang; Delzanno, Giorgio; Haziza, Frédéric et al.

Part of CONCUR 2010 – Concurrency Theory, p. 86-101, 2010

• DOI for Constrained monotonic abstraction: A CEGAR for parameterized verification

Approximated Context-Sensitive Analysis for Parameterized Verification

Abdulla, Aziz; Delzanno, Giorgio; Rezine, Ahmed

Part of Formal Techniques for Distributed Systems, p. 41-56, 2009

• DOI for Approximated Context-Sensitive Analysis for Parameterized Verification

Automatic Verification of Directory-Based Consistency Protocols

Abdulla, Aziz; Delzanno, Giorgio; Rezine, Ahmed

Part of Reachability Problems, p. 36-50, 2009

• DOI for Automatic Verification of Directory-Based Consistency Protocols

Handling parameterized systems with non-atomic global conditions

Abdulla, Parosh Aziz; Ben Henda, Noomene; Delzanno, Giorgio; Rezine, Ahmed

Part of Verification, Model Checking, and Abstract Interpretation, p. 22-36, 2008

• DOI for Handling parameterized systems with non-atomic global conditions

Parameterized tree systems

Abdulla, Parosh Aziz; Ben Henda, Noomene; Delzanno, Giorgio; Haziza, Frédéric et al.

Part of Formal Techniques for Networked and Distributed Systems, p. 69-83, 2008

• DOI for Parameterized tree systems

Monotonic abstraction in action: Automatic verification of distributed mutex algorithms

Abdulla, Parosh Aziz; Delzanno, Giorgio; Rezine, Ahmed

Part of Theoretical Aspects of Computing - ICTAC 2008, p. 50-65, 2008

• DOI for Monotonic abstraction in action: Automatic verification of distributed mutex algorithms

Stochastic games with lossy channels

Abdulla, Parosh Aziz; Ben Henda, Noomene; de Alfaro, Luca; Mayr, Richard et al.

Part of Foundations of Software Science and Computational Structures, p. 35-49, 2008

• DOI for Stochastic games with lossy channels

Monotonic abstraction for programs with dynamic memory heaps

Abdulla, Parosh Aziz; Bouajjani, Ahmed; Cederberg, Jonathan; Haziza, Frédéric et al.

Part of Computer Aided Verification, p. 341-354, 2008

• DOI for Monotonic abstraction for programs with dynamic memory heaps

Model Checking Race-Freeness

Abdulla, Parosh Aziz; Haziza, Frédéric; Kindahl, Mats

Part of Proc. 1st Swedish Workshop on Multi-Core Computing, p. 89-96, 2008

R-automata

Abdulla, Parosh Aziz; Krcal, Pavel; Yi, Wang

Part of CONCUR 2008 - Concurrency Theory, p. 67-81, 2008

• DOI for R-automata

Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata

Abdulla, Parosh Aziz; Bouajjani, Ahmed; Holík, Lukás; Kaati, Lisa et al.

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 93-108, 2008

• DOI for Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata

Composed Bisimulation for Tree Automata

Abdulla, Parosh Aziz; Bouajjani, Ahmed; Holík, Lukás; Kaati, Lisa et al.

Part of Implementation and Application of Automata, p. 212-222, 2008

• DOI for Composed Bisimulation for Tree Automata

Sampled universality of timed automata

Abdulla, Parosh Aziz; Krcal, Pavel; Yi, Wang

Part of Foundations of Software Science and Computational Structures, Proceedings, p. 2-16, 2007

• DOI for Sampled universality of timed automata

Zone-Based Universality Analysis for Single-Clock Timed Automata

Abdulla, Parosh; Ouaknine, Joel; Quaas, Karin; Worrell, James

Part of International Symposium on Fundamentals of Software Engineering, Proceedings, p. 98-112, 2007

Parameterized Verification of Infinite-state Processes with Global Conditions

Abdulla, Parosh; Delzanno, Giorgio; Rezine, Ahmed

Part of Computer Aided Verification, Proceedings, p. 145-157, 2007

Regular Model Checking without Transducers

Abdulla, Parosh Aziz; Ben Henda, Noomene; Delzanno, Giorgio; Rezine, Ahmed

Part of TACAS'07, The 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2007

Eager Markov Chains: Eager Markov Chains

Abdulla, Parosh; Ben Henda, Noomene; Mayr, Richard; Sandberg, Sven

Part of Proceedings of the fourth international symposium on Automated Technology for Verification and Analysis (ATVA), p. 24-38, 2006

Limiting Behavior of Markov Chains with Eager Attractors

Abdulla, Parosh; Ben Henda, Noomene; Mayr, Richard; Sandberg, Sven

Part of Third International Conference on the Quantitative Evaluation of Systems (QEST), p. 253-262, 2006

Minimization of Non-deterministic Automata with Large Alphabets

Abdulla, Parosh Aziz; Deneux, Johann; Kaati, Lisa; Nilsson, Marcus

Part of Implementation and Application of Automata, p. 31-42, 2006

• DOI for Minimization of Non-deterministic Automata with Large Alphabets

Bisimulation Minimization of Tree Automata

Abdulla, Parosh Aziz; Kaati, Lisa; Högberg, Johanna

Part of Implementation and Application of Automata, p. 173-185, 2006

• DOI for Bisimulation Minimization of Tree Automata

Proving Liveness by Backwards Reachability

Abdulla, Parosh Aziz; Jonsson, Bengt; Rezine, Ahmed; Saksena, Mayank

2006

Open, Closed and Robust Timed Networks.

Abdulla, Parosh; Deneux, Johann; Mahata, Pritha

Part of CONCUR 2004 -- Concurrency Theory, p. 529, 2004

Multi-Clock Timed Networks

Abdulla, Parosh; Deneux, Johann; Mahata, Pritha

Part of LICS'2004, 18th IEEE Int. Symp. on Logic in Computer Science, 2004

Regular Model Checking for LTL(MSO)

Abdulla, Parosh; Jonsson, Bengt; Nilsson, Marcus; d'Orso, Julien et al.

Part of Computer Aided Verification, p. 348-360, 2004

A Survey of Regular Model Checking.

Abdulla, Parosh; Jonsson, Bengt; Nilsson, Marcus; Saksena, Mayank

Part of CONCUR 2004 - Concurrency Theory, p. 35-48, 2004

Report on Dataflow Dependencies in Billing Processing Systems

Abdulla, Parosh; Ben Henda, Noomene; Deneux, Johann; Jonsson, Bengt et al.

Part of Proc. ISoLA '04: 1st International Symposium on Leveraging Applications of Formal Methods, 2004

Designing Safe, Reliable Systems using Scade

Abdulla, Parosh; Deneux, Johann; Åkerlund, Ove

Part of Proc. ISoLA '04: International Symposium on Leveraging Applications of Formal Methods, 2004

Regular Tree Model Checking

Abdulla, Parosh Aziz; Jonsson, Bengt; Mahata, Pritha; d'Orso, Julien

Part of Computer Aided Verification, p. 555-568, 2002

• DOI for Regular Tree Model Checking

Effective Lossy Queue Languages.

Abdulla, PA; Boasson, L; Bouajjani, A

Part of ICALP'2001, 28th Int. Colloquium on Automata, Languages and Programmming., 2001

Handling Global Conditions in Parameterized System Verification

Abdulla, Parosh Aziz; Bouajjani, Ahmed; Jonnson, Bengt; Nilsson, Marcus

Part of Proc. 11th Int. Conf. on Computer Aided Verification, p. 134-145, 1999

• DOI for Handling Global Conditions in Parameterized System Verification

Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol

Abdulla, Parosh Aziz; Annichini, A; Bouajjani, A

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 208-222, 1999

• DOI for Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol

A general approach to partial order reductions in symbolic verification

Abdulla, Parosh Aziz; Jonsson, Bengt; Kindahl, Mats; Peled, D

Part of Computer Aided Verification, p. 379-390, 1998

• DOI for A general approach to partial order reductions in symbolic verification

Simulation is decidable for one-counter nets

Abdulla, Parosh Aziz; Cerans, K

Part of CONCUR'98 Concurrency Theory, p. 253-268, 1998

• DOI for Simulation is decidable for one-counter nets

Verifying networks of timed processes

Abdulla, Parosh Aziz; Jonsson, Bengt

Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 298-312, 1998

• DOI for Verifying networks of timed processes

Undecidable verification problems for programs with unreliable channels

Abdulla, Parosh Aziz; Jonsson, Bengt

Part of Automata, Languages and Programming, p. 71-90, 1996

• DOI for Undecidable verification problems for programs with unreliable channels

TACAS'2011, 17th International ConferenceTools and Algorithms for the Construction and Analysis of Systems.

Abdulla, Parosh Aziz; Leino, Rustan

2011

Stochastic Games with Lossy Channels

Abdulla, Parosh Aziz; Ben Henda, Noomene; Mayr, Richard; Sandberg, Sven

Decision problems in systolic circuit verification

Abdulla, Parosh

1990

• Download full text (pdf) of Decision problems in systolic circuit verification