Parosh Abdulla

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

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

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

Parsimonious Optimal Dynamic Partial Order Reduction

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

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

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

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

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

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

2023

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

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

Abdulla, Parosh; Atig, Mohamed Faouzi; Meyer Bonneland, Frederik; Das, Sarbojit et al.

Part of Automated Technology for Verification and Analysis, 21st International Symposium, ATVA 2023, Singapore, Oct. 2023. Proceedings., 2023

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

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

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

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

Parameterized Verification under TSO with Data Types

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

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

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

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

Verifying Reachability for TSO Programs with Dynamic Thread Creation

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

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

DOI for Verifying Reachability for TSO Programs with Dynamic Thread Creation

On the State Reachability Problem for Concurrent Programs Under Power

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

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

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

The Decidability of Verification under PS 2.0

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

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

Solving Not-Substring Constraint with Flat Abstraction

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

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

DOI for Solving Not-Substring Constraint with Flat Abstraction

On the Separability Problem of String Constraints

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

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

DOI for On the Separability Problem of String Constraints

On the Formalization of Decentralized Contact Tracing Protocols

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

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

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

Chain-Free String Constraints

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

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

DOI for Chain-Free String Constraints

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

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

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

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

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)

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

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

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

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

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

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

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

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

Verification of Cache Coherence Protocols wrt. Trace Filters

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

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

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

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

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

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

Stateless model checking for TSO and PSO

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

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

DOI for Stateless model checking for TSO and PSO

Verification of buffered dynamic register automata

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

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

DOI for Verification of buffered dynamic register automata

What's decidable about availability languages?

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

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

DOI for What's decidable about availability languages?

Norn: An SMT solver for string constraints

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

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

DOI for Norn: An SMT solver for string constraints

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

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

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

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

Veriﬁcation 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

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

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

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

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

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

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

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

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

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

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

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

Carrying Probabilities to the Infinite World

Abdulla, Parosh Aziz

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

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

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

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

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

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

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

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

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

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

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

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

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

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

R-automata

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

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

DOI for R-automata

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

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

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

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

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

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

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

Multi-Clock Timed Networks

Abdulla, Parosh; Deneux, Johann; Mahata, Pritha

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

Open, Closed and Robust Timed Networks.

Abdulla, Parosh; Deneux, Johann; Mahata, Pritha

Part of CONCUR 2004 -- Concurrency Theory, p. 529, 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

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

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

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

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

Publications

Recent publications

All publications

Articles in journal

Articles, review/survey

Chapters in book

Conference papers

Conference proceedings (editor)

Manuscripts (preprints)

Monograph doctoral thesis