Parosh Abdulla

On the Verification Problem of Remote Direct Memory Access Programs

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

Ingår i Computer Aided Verification, s. 113-135, 2026

• DOI för On the Verification Problem of Remote Direct Memory Access Programs
• Ladda ner fulltext (pdf) av 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.

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

Parameterized Verification of Quantum Circuits

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

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

• DOI för Parameterized Verification of Quantum Circuits
• Ladda ner fulltext (pdf) av Parameterized Verification of Quantum Circuits

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

Quantum Circuit Verification - A Potential Roadmap (Invited Talk)

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

Ingår i 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2025, s. 1-1, 2025

• DOI för Quantum Circuit Verification - A Potential Roadmap (Invited Talk)
• Ladda ner fulltext (pdf) av Quantum Circuit Verification - A Potential Roadmap (Invited Talk)

Parameterized Verification of Quantum Circuits

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

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

• DOI för Parameterized Verification of Quantum Circuits
• Ladda ner fulltext (pdf) av Parameterized Verification of Quantum Circuits

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

Efficient Linearizability Monitoring

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

Ingår i Proceedings of the ACM on Programming Languages, s. 1937-1960, 2025

• DOI för Efficient Linearizability Monitoring
• Ladda ner fulltext (pdf) av Efficient Linearizability Monitoring

A Symbolic Approach to Verifying Quantum Systems

Abdulla, Parosh Aziz

Ingår i Communications of the ACM, s. 84-84, 2025

• DOI för A Symbolic Approach to Verifying Quantum Systems
• Ladda ner fulltext (pdf) av 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.

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

• DOI för Verifying Quantum Circuits with Level-Synchronized Tree Automata
• Ladda ner fulltext (pdf) av 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

Ingår i Computers, 2025

• DOI för A Novel Approach to Efficiently Verify Sequential Consistency in Concurrent Programs
• Ladda ner fulltext (pdf) av 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.

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

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

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

Ingår i Proceedings of the ACM on Programming Languages, s. 761-785, 2023

• DOI för Optimal Reads-From Consistency Checking for C11-Style Memory Models
• Ladda ner fulltext (pdf) av 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.

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

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

Special Issue on NETYS'2016

Abdulla, Parosh Aziz; Delporte, Carole

Ingår i Computing, s. 1-2, 2019

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

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

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

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

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.

Ingår i International Journal on Software Tools for Technology Transfer, s. 549-563, 2017

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

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

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

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

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

Ingår i Journal of the ACM, 2017

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

Ingår i Acta Informatica, s. 357-385, 2016

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

Ingår i International Journal on Software Tools for Technology Transfer, s. 495-516, 2016

• DOI för Parameterized verification through view abstraction

Parameterized verification

Abdulla, Parosh A.; Delzanno, Giorgio

Ingår i International Journal on Software Tools for Technology Transfer, s. 469-473, 2016

• DOI för Parameterized verification

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

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

Ingår i Theoretical Computer Science, s. 1-22, 2016

• DOI för Parameterized verification of time-sensitive models of ad hoc network protocols

Well Structured Transition Systems with History

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

Ingår i Electronic Proceedings in Theoretical Computer Science, s. 115-128, 2015

• DOI för Well Structured Transition Systems with History

Stochastic Parity Games on Lossy Channel Systems

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

Ingår i Logical Methods in Computer Science, 2014

• DOI för Stochastic Parity Games on Lossy Channel Systems
• Ladda ner fulltext (pdf) av Stochastic Parity Games on Lossy Channel 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

Mediating for reduction (on minimizing alternating Buchi automata)

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

Ingår i Theoretical Computer Science, s. 26-43, 2014

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

Priced timed Petri nets

Abdulla, Parosh Aziz; Mayr, Richard

Ingår i Logical Methods in Computer Science, 2013

• DOI för Priced timed Petri nets

Monotonic abstraction for programs with multiply-linked structures

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

Ingår i International Journal of Foundations of Computer Science, s. 187-210, 2013

• DOI för Monotonic abstraction for programs with multiply-linked structures
• Ladda ner fulltext (pdf) av 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.

Ingår i International Journal on Software Tools for Technology Transfer, s. 223-241, 2012

• DOI för Regular model checking for LTL(MSO)

Regular model checking

Abdulla, Parosh Aziz

Ingår i International Journal on Software Tools for Technology Transfer, s. 109-118, 2012

• DOI för Regular model checking

Automatic verification of directory-based consistency protocols with graph constraints

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

Ingår i International Journal of Foundations of Computer Science, s. 761-782, 2011

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

Ingår i Information and Computation, s. 248-279, 2011

• DOI för A classification of the expressive power of well-structured transition systems

Sampled semantics of timed automata

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

Ingår i Logical Methods in Computer Science, 2010

• DOI för Sampled semantics of timed automata

Well (and better) quasi-ordered transition systems

Abdulla, Parosh Aziz

Ingår i Bulletin of Symbolic Logic, s. 457-515, 2010

Universality of R-automata with value copying

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

Ingår i Electronic Notes in Theoretical Computer Science, s. 131-141, 2009

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

Ingår i Electronic Notes in Theoretical Computer Science, s. 27-48, 2009

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

Ingår i International Journal of Foundations of Computer Science, s. 779-801, 2009

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

Ingår i International Journal of Foundations of Computer Science, s. 685-700, 2009

• DOI för Composed bisimulation for tree automata

Approximated parameterized verification of infinite-state processes with global conditions

Abdulla, Aziz; Delzanno, Giorgio; Rezine, Ahmed

Ingår i Formal methods in system design, s. 126-156, 2009

• DOI för Approximated parameterized verification of infinite-state processes with global conditions

Monotonic Abstraction in Parameterized Verification

Abdulla, Aziz; Delzanno, Giorgio; Rezine, Ahmed

Ingår i Electronic Notes in Theoretical Computer Science, s. 3-14, 2008

• DOI för Monotonic Abstraction in Parameterized Verification

Model checking race-freeness

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

Ingår i SIGARCH Computer Architecture News, s. 72-79, 2008

• DOI för Model checking race-freeness

Monotonic and downward closed games

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

Ingår i Journal of logic and computation (Print), s. 153-169, 2008

• DOI för Monotonic and downward closed games

Universality Analysis for One-Clock Timed Automata

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

Ingår i Fundamenta Informaticae, s. 419-450, 2008

Decisive Markov Chains

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

Ingår i Logical Methods in Computer Science, s. 1-32, 2007

• DOI för Decisive Markov Chains

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

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

Ingår i Logical Methods in Computer Science, s. 1-61, 2007

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

Ingår i Nordic Journal of Computing, s. 1-42, 2007

Bisimulation minimization of tree automata

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

Ingår i International Journal of Foundations of Computer Science, s. 699-713, 2007

• DOI för Bisimulation minimization of tree automata

Simulating perfect channels with probabilistic lossy channels

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

Ingår i Information and Computation, s. 22-40, 2005

Using Forward Reachability Analysis for Verification of Lossy Channel Systems

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

Ingår i Formal methods in system design, s. 39-65, 2004

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

Ingår i Formal methods in system design, s. 25-43, 2004

Model checking of systems with many identical timed processes

Abdulla, Parosh; Jonsson, Bengt

Ingår i Theoretical Computer Science, s. 241-264, 2003

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

Ingår i INFORMATION AND COMPUTATION, s. 109-127, 2000

Verifying programs with unreliable channels

Abdulla, PA; Jonsson, B

Ingår i Information and Computation, s. 91-101, 1996

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

Ingår i International Journal on Software Tools for Technology Transfer, s. 85-88, 2013

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

Decision problems in systolic circuit verification

Abdulla, Parosh

1990

• Ladda ner fulltext (pdf) av Decision problems in systolic circuit verification

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

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

Ingår i Principles of Formal Quantitative Analysis, s. 320-341, Springer Nature, 2025

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

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

Model checking parameterized systems

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

Ingår i Handbook of Model Checking, s. 685-725, Springer, 2018

• DOI för Model checking parameterized systems

Comparing source sets and persistent sets for partial order reduction

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

Ingår i Models, Algorithms, Logics and Tools, s. 516-536, Springer, 2017

• DOI för Comparing source sets and persistent sets for partial order reduction

On the existence of network invariants for verifying parameterized systems

Abdulla, Parosh; Jonsson, Bengt

Ingår i Correct System Design, s. 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

Ingår i Computer Aided Verification, s. 113-135, 2026

• DOI för On the Verification Problem of Remote Direct Memory Access Programs
• Ladda ner fulltext (pdf) av 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.

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

Quantum Circuit Verification - A Potential Roadmap (Invited Talk)

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

Ingår i 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2025, s. 1-1, 2025

• DOI för Quantum Circuit Verification - A Potential Roadmap (Invited Talk)
• Ladda ner fulltext (pdf) av 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.

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

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

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

Ingår i Programming Languages and Systems - 23rd Asian Symposium, APLAS 2025, Bengaluru, India, October 27-30, 2025, Proceedings, s. 173-194, 2025

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

Ingår i Automated technology for verification and analysis, ATVA 2024, pt i, s. 181-202, 2025

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

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

Boosting Constrained Horn Solving by Unsat Core Learning

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

Ingår i Verification, Model Checking, and Abstract Interpretation, s. 280-302, 2024

• DOI för Boosting Constrained Horn Solving by Unsat Core Learning

Concurrent Stochastic Lossy Channel Games

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

Ingår i 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), 2024

• DOI för Concurrent Stochastic Lossy Channel Games
• Ladda ner fulltext (pdf) av Concurrent Stochastic Lossy Channel Games

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

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

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

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

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

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

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

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

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

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

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

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

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

Fragment abstraction for concurrent shape analysis

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

Ingår i Programming Languages and Systems, s. 442-471, 2018

• DOI för Fragment abstraction for concurrent shape analysis

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

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

Automated Verification of Linearization Policies

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

Ingår i Automated Verification of Linearization Policies, 2016

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

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

Qualitative Analysis of VASS-Induced MDPs

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

Ingår i Foundations Of Software Science And Computation Structures (FOSSACS 2016), s. 319-334, 2016

• DOI för Qualitative Analysis of VASS-Induced MDPs

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

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

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

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

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

Optimal dynamic partial order reduction

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

Ingår i Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, s. 373-384, 2014

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

Ingår i Static Analysis, s. 1-17, 2014

• DOI för Block me if you can!: Context-sensitive parameterized verification
• Ladda ner fulltext (pdf) av 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

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

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

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

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

Verifying safety and liveness for the FlexTM hybrid transactional memory

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

s. 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.

Ingår i Automated Technology for Verification and Analysis, s. 224-239, 2013

• DOI för Verification of heap manipulating programs with ordered data by extended forest automata
• Ladda ner fulltext (pdf) av 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

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

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

Solving parity games on integer vectors

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

Ingår i CONCUR 2013 – Concurrency Theory, s. 106-120, 2013

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

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

An Integrated Specification and Verification Technique for Highly Concurrent Data Structures

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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, 2013

• Ladda ner fulltext (pdf) av 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

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

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

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

Ingår i Verification, Model Checking, and Abstract Interpretation, s. 476-495, 2013

• DOI för All for the price of few: (Parameterized verification through view abstraction)
• Ladda ner fulltext (pdf) av 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.

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

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

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

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

• DOI för Adding time to pushdown automata

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

On the verification of timed ad hoc networks

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

Ingår i Formal Modeling and Analysis of Timed Systems, s. 256-270, 2011

• DOI för On the verification of timed ad hoc networks

Computing Optimal Coverability Costs in Priced Timed Petri Nets

Abdulla, Parosh Aziz; Richard, Mayr

Ingår i LICS'2011, Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, s. 399-408, 2011

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

Ingår i CONCUR 2011 — Concurrency Theory, s. 187-202, 2011

• DOI för Advanced Ramsey-based Büchi automata inclusion testing

Carrying Probabilities to the Infinite World

Abdulla, Parosh Aziz

Ingår i CONCUR'2011, 22nd International Conference on Concurrency Theory., 2011

Forcing monotonicity in parameterized verification: From multisets to words

Abdulla, Parosh Aziz

Ingår i SOFSEM 2010, s. 1-15, 2010

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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 158-174, 2010

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

Ingår i Computer Aided Verification, s. 132-147, 2010

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

Ingår i Leveraging Applications of Formal Methods, Verification, and Validation, s. 60-74, 2010

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

Ingår i CONCUR 2010 – Concurrency Theory, s. 86-101, 2010

• DOI för Constrained monotonic abstraction: A CEGAR for parameterized verification

Approximated Context-Sensitive Analysis for Parameterized Verification

Abdulla, Aziz; Delzanno, Giorgio; Rezine, Ahmed

Ingår i Formal Techniques for Distributed Systems, s. 41-56, 2009

• DOI för Approximated Context-Sensitive Analysis for Parameterized Verification

Automatic Verification of Directory-Based Consistency Protocols

Abdulla, Aziz; Delzanno, Giorgio; Rezine, Ahmed

Ingår i Reachability Problems, s. 36-50, 2009

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

Ingår i Verification, Model Checking, and Abstract Interpretation, s. 22-36, 2008

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

Ingår i Formal Techniques for Networked and Distributed Systems, s. 69-83, 2008

• DOI för Parameterized tree systems

Monotonic abstraction in action: Automatic verification of distributed mutex algorithms

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

Ingår i Theoretical Aspects of Computing - ICTAC 2008, s. 50-65, 2008

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

Ingår i Foundations of Software Science and Computational Structures, s. 35-49, 2008

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

Ingår i Computer Aided Verification, s. 341-354, 2008

• DOI för Monotonic abstraction for programs with dynamic memory heaps

Model Checking Race-Freeness

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

Ingår i Proc. 1st Swedish Workshop on Multi-Core Computing, s. 89-96, 2008

R-automata

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

Ingår i CONCUR 2008 - Concurrency Theory, s. 67-81, 2008

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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 93-108, 2008

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

Ingår i Implementation and Application of Automata, s. 212-222, 2008

• DOI för Composed Bisimulation for Tree Automata

Sampled universality of timed automata

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

Ingår i Foundations of Software Science and Computational Structures, Proceedings, s. 2-16, 2007

• DOI för Sampled universality of timed automata

Zone-Based Universality Analysis for Single-Clock Timed Automata

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

Ingår i International Symposium on Fundamentals of Software Engineering, Proceedings, s. 98-112, 2007

Parameterized Verification of Infinite-state Processes with Global Conditions

Abdulla, Parosh; Delzanno, Giorgio; Rezine, Ahmed

Ingår i Computer Aided Verification, Proceedings, s. 145-157, 2007

Regular Model Checking without Transducers

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

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

Ingår i Proceedings of the fourth international symposium on Automated Technology for Verification and Analysis (ATVA), s. 24-38, 2006

Limiting Behavior of Markov Chains with Eager Attractors

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

Ingår i Third International Conference on the Quantitative Evaluation of Systems (QEST), s. 253-262, 2006

Minimization of Non-deterministic Automata with Large Alphabets

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

Ingår i Implementation and Application of Automata, s. 31-42, 2006

• DOI för Minimization of Non-deterministic Automata with Large Alphabets

Bisimulation Minimization of Tree Automata

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

Ingår i Implementation and Application of Automata, s. 173-185, 2006

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

Ingår i CONCUR 2004 -- Concurrency Theory, s. 529, 2004

Multi-Clock Timed Networks

Abdulla, Parosh; Deneux, Johann; Mahata, Pritha

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

Ingår i Computer Aided Verification, s. 348-360, 2004

A Survey of Regular Model Checking.

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

Ingår i CONCUR 2004 - Concurrency Theory, s. 35-48, 2004

Report on Dataflow Dependencies in Billing Processing Systems

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

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

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

Ingår i Computer Aided Verification, s. 555-568, 2002

• DOI för Regular Tree Model Checking

Effective Lossy Queue Languages.

Abdulla, PA; Boasson, L; Bouajjani, A

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

Ingår i Proc. 11th Int. Conf. on Computer Aided Verification, s. 134-145, 1999

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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 208-222, 1999

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

Ingår i Computer Aided Verification, s. 379-390, 1998

• DOI för A general approach to partial order reductions in symbolic verification

Simulation is decidable for one-counter nets

Abdulla, Parosh Aziz; Cerans, K

Ingår i CONCUR'98 Concurrency Theory, s. 253-268, 1998

• DOI för Simulation is decidable for one-counter nets

Verifying networks of timed processes

Abdulla, Parosh Aziz; Jonsson, Bengt

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 298-312, 1998

• DOI för Verifying networks of timed processes

Undecidable verification problems for programs with unreliable channels

Abdulla, Parosh Aziz; Jonsson, Bengt

Ingår i Automata, Languages and Programming, s. 71-90, 1996

• DOI för Undecidable verification problems for programs with unreliable channels

Stochastic Games with Lossy Channels

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

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

Abdulla, Parosh Aziz; Leino, Rustan

2011