Parosh Aziz Abdulla

According to our database1, Parosh Aziz Abdulla
  • authored at least 185 papers between 1988 and 2017.
  • has a "Dijkstra number"2 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2017
An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures.
STTT, 2017

Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction.
J. ACM, 2017

What is Decidable about Perfect Timed Channels?
CoRR, 2017

Context-Bounded Analysis for POWER.
CoRR, 2017

The Benefits of Duality in Verifying Concurrent Programs under TSO.
CoRR, 2017

Stateless model checking for TSO and PSO.
Acta Inf., 2017

Context-Bounded Analysis for POWER.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Flatten and conquer: a framework for efficient analysis of string constraints.
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Data Multi-Pushdown Automata.
Proceedings of the 28th International Conference on Concurrency Theory, 2017

Comparing Source Sets and Persistent Sets for Partial Order Reduction.
Proceedings of the Models, Algorithms, Logics and Tools, 2017

2016
Parameterized verification of time-sensitive models of ad hoc network protocols.
Theor. Comput. Sci., 2016

Parameterized verification through view abstraction.
STTT, 2016

Parameterized verification.
STTT, 2016

Preface.
Fundam. Inform., 2016

Mending Fences with Self-Invalidation and Self-Downgrade.
CoRR, 2016

Stateless Model Checking for POWER.
CoRR, 2016

Recency-Bounded Verification of Dynamic Database-Driven Systems (Extended Version).
CoRR, 2016

Verification of heap manipulating programs with ordered data by extended forest automata.
Acta Inf., 2016

Automated Verification of Linearization Policies.
Proceedings of the Static Analysis - 23rd International Symposium, 2016

Recency-Bounded Verification of Dynamic Database-Driven Systems.
Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, 2016

Data Communicating Processes with Unreliable Channels.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Qualitative Analysis of VASS-Induced MDPs.
Proceedings of the Foundations of Software Science and Computation Structures, 2016

Fencing Programs with Self-Invalidation and Self-Downgrade.
Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2016

Counter-Example Guided Program Verification.
Proceedings of the FM 2016: Formal Methods, 2016

The Benefits of Duality in Verifying Concurrent Programs under TSO.
Proceedings of the 27th International Conference on Concurrency Theory, 2016

Stateless Model Checking for POWER.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015
Verification of Evolving Graph Structures (Dagstuhl Seminar 15451).
Dagstuhl Reports, 2015

Well Structured Transition Systems with History.
Proceedings of the Proceedings Sixth International Symposium on Games, 2015

Qualitative Analysis of VASS-Induced MDPs.
CoRR, 2015

Stateless Model Checking for TSO and PSO.
CoRR, 2015

Stateless Model Checking for TSO and PSO.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

View Abstraction - A Tutorial (Invited Paper).
Proceedings of the 2nd International Workshop on Synthesis of Complex Parameters, 2015

Precise and Sound Automatic Fence Insertion Procedure under PSO.
Proceedings of the Networked Systems - Third International Conference, 2015

Verification of Buffered Dynamic Register Automata.
Proceedings of the Networked Systems - Third International Conference, 2015

What's Decidable about Availability Languages?.
Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

Verification of Cache Coherence Protocols wrt. Trace Filters.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO.
Proceedings of the Programming Languages and Systems, 2015

Norn: An SMT Solver for String Constraints.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
Mediating for reduction (on minimizing alternating Büchi automata).
Theor. Comput. Sci., 2014

Budget-bounded model-checking pushdown systems.
Formal Methods in System Design, 2014

Stochastic Parity Games on Lossy Channel Systems.
Logical Methods in Computer Science, 2014

Infinite-State Energy Games.
CoRR, 2014

Block Me If You Can! - Context-Sensitive Parameterized Verification.
Proceedings of the Static Analysis - 21st International Symposium, 2014

Optimal dynamic partial order reduction.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Computing Optimal Reachability Costs in Priced Dense-Timed Pushdown Automata.
Proceedings of the Language and Automata Theory and Applications, 2014

Verification of Dynamic Register Automata.
Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 2014

MPass: An Efficient Tool for the Analysis of Message-Passing Programs.
Proceedings of the Formal Aspects of Component Software - 11th International Symposium, 2014

Infinite-state energy games.
Proceedings of the 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), 2014

String Constraints for Verification.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
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.
STTT, 2013

Monotonic Abstraction for Programs with Multiply-Linked Structures.
Int. J. Found. Comput. Sci., 2013

Stochastic Parity Games on Lossy Channel Systems
CoRR, 2013

Solving Parity Games on Integer Vectors.
CoRR, 2013

Priced Timed Petri Nets.
Logical Methods in Computer Science, 2013

Zenoness for Timed Pushdown Automata.
Proceedings of the Proceedings 15th International Workshop on Verification of Infinite-State Systems, 2013

All for the Price of Few.
Proceedings of the Verification, 2013

An Integrated Specification and Verification Technique for Highly Concurrent Data Structures.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Stochastic Parity Games on Lossy Channel Systems.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

Push-Down Automata with Gap-Order Constraints.
Proceedings of the Fundamentals of Software Engineering - 5th International Conference, 2013

Verification of Directed Acyclic Ad Hoc Networks.
Proceedings of the Formal Techniques for Distributed Systems, 2013

Verifying safety and liveness for the FlexTM hybrid transactional memory.
Proceedings of the Design, Automation and Test in Europe, 2013

Solving Parity Games on Integer Vectors.
Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata.
Proceedings of the Automated Technology for Verification and Analysis, 2013

Analysis of Message Passing Programs Using SMT-Solvers.
Proceedings of the Automated Technology for Verification and Analysis, 2013

2012
Regular model checking for LTL(MSO).
STTT, 2012

Regular model checking.
STTT, 2012

Petri Nets with Time and Cost
Proceedings of the Proceedings 14th International Workshop on Verification of Infinite-State Systems, 2012

Adding Time to Pushdown Automata
Proceedings of the Proceedings Quantities in Formal Methods, 2012

Counter-Example Guided Fence Insertion under TSO.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Automatic Fence Insertion in Integer Programs via Predicate Abstraction.
Proceedings of the Static Analysis - 19th International Symposium, 2012

Dense-Timed Pushdown Automata.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

The Minimal Cost Reachability Problem in Priced Timed Pushdown Systems.
Proceedings of the Language and Automata Theory and Applications, 2012

Timed Lossy Channel Systems.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2012

Multi-pushdown systems with budgets.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

2011
Automatic Verification of Directory-Based Consistency Protocols with Graph Constraints.
Int. J. Found. Comput. Sci., 2011

A classification of the expressive power of well-structured transition systems.
Inf. Comput., 2011

Computing Optimal Coverability Costs in Priced Timed Petri Nets
CoRR, 2011

Monotonic Abstraction for Programs with Multiply-Linked Structures.
Proceedings of the Reachability Problems - 5th International Workshop, 2011

Computing Optimal Coverability Costs in Priced Timed Petri Nets.
Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

On the Verification of Timed Ad Hoc Networks.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2011

Advanced Ramsey-Based Büchi Automata Inclusion Testing.
Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Carrying Probabilities to the Infinite World.
Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

2010
Sampled Semantics of Timed Automata
Logical Methods in Computer Science, 2010

Well (and better) quasi-ordered transition systems.
Bulletin of Symbolic Logic, 2010

When Simulation Meets Antichains.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Forcing Monotonicity in Parameterized Verification: From Multisets to Words.
Proceedings of the SOFSEM 2010: Theory and Practice of Computer Science, 2010

Analyzing the Security in the GSM Radio Network Using Attack Jungles.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification.
Proceedings of the CONCUR 2010 - Concurrency Theory, 21th International Conference, 2010

Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Monotonic Abstraction: on Efficient Verification of Parameterized Systems.
Int. J. Found. Comput. Sci., 2009

Composed Bisimulation for Tree Automata.
Int. J. Found. Comput. Sci., 2009

Approximated parameterized verification of infinite-state processes with global conditions.
Formal Methods in System Design, 2009

Universality of R-automata with Value Copying.
Electr. Notes Theor. Comput. Sci., 2009

A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata.
Electr. Notes Theor. Comput. Sci., 2009

Automatic Verification of Directory-Based Consistency Protocols.
Proceedings of the Reachability Problems, 3rd International Workshop, 2009

Infinite-State Verification: From Transition Systems to Markov Chains.
Proceedings of the QEST 2009, 2009

A Language-Based Comparison of Extensions of Petri Nets with and without Whole-Place Operations.
Proceedings of the Language and Automata Theory and Applications, 2009

Mediating for Reduction (on Minimizing Alternating Büchi Automata).
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2009

Minimal Cost Reachability/Coverability in Priced Timed Petri Nets.
Proceedings of the Foundations of Software Science and Computational Structures, 2009

Approximated Context-Sensitive Analysis for Parameterized Verification.
Proceedings of the Formal Techniques for Distributed Systems, 2009

Automated Analysis of Data-Dependent Programs with Dynamic Memory.
Proceedings of the Automated Technology for Verification and Analysis, 2009

2008
Model checking race-freeness.
SIGARCH Computer Architecture News, 2008

Monotonic and Downward Closed Games.
J. Log. Comput., 2008

Universality Analysis for One-Clock Timed Automata.
Fundam. Inform., 2008

Monotonic Abstraction in Parameterized Verification.
Electr. Notes Theor. Comput. Sci., 2008

Composed Bisimulation for Tree Automata.
Proceedings of the Implementation and Applications of Automata, 2008

Handling Parameterized Systems with Non-atomic Global Conditions.
Proceedings of the Verification, 2008

Computing Simulations over Tree Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

On the Qualitative Analysis of Conformon P Systems.
Proceedings of the Membrane Computing - 9th International Workshop, 2008

Monotonic Abstraction in Action.
Proceedings of the Theoretical Aspects of Computing, 2008

Stochastic Games with Lossy Channels.
Proceedings of the Foundations of Software Science and Computational Structures, 2008

Parameterized Tree Systems.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2008

Shape Analysis via Monotonic Abstraction.
Proceedings of the Beyond the Finite: New Challenges in Verification and Semistructured Data, 20.04., 2008

R-Automata.
Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

Monotonic Abstraction for Programs with Dynamic Memory Heaps.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007
Using Forward Reachability Analysis for Verification of Timed Petri Nets.
Nord. J. Comput., 2007

Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness.
Logical Methods in Computer Science, 2007

Decisive Markov Chains.
Logical Methods in Computer Science, 2007

Bisimulation Minimization of Tree Automata.
Int. J. Found. Comput. Sci., 2007

Decisive Markov Chains
CoRR, 2007

Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Zone-Based Universality Analysis for Single-Clock Timed Automata.
Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

Sampled Universality of Timed Automata.
Proceedings of the Foundations of Software Science and Computational Structures, 2007

Comparing the Expressive Power of Well-Structured Transition Systems.
Proceedings of the Computer Science Logic, 21st International Workshop, 2007

Parameterized Verification of Infinite-State Processes with Global Conditions.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006
Tree regular model checking: A simulation-based approach.
J. Log. Algebr. Program., 2006

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

Bisimulation Minimization of Tree Automata.
Proceedings of the Implementation and Application of Automata, 2006

Limiting Behavior of Markov Chains with Eager Attractors.
Proceedings of the Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 2006

06081 Abstracts Collection -- Software Verification: Infinite-State Model Checking and Static Program Analysis.
Proceedings of the Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02., 2006

06081 Executive Summary -- Software Verification: Infinite-State Model Checking and Static Program Analysis.
Proceedings of the Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02., 2006

Proving Liveness by Backwards Reachability.
Proceedings of the CONCUR 2006 - Concurrency Theory, 17th International Conference, 2006

Eager Markov Chains.
Proceedings of the Automated Technology for Verification and Analysis, 2006

2005
Verification of probabilistic systems with faulty communication.
Inf. Comput., 2005

Simulating perfect channels with probabilistic lossy channels.
Inf. Comput., 2005

Closed, Open, and Robust Timed Networks.
Electr. Notes Theor. Comput. Sci., 2005

Minimization of Non-deterministic Automata with Large Alphabets.
Proceedings of the Implementation and Application of Automata, 2005

Simulation-Based Iteration of Tree Transducers.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Verifying Infinite Markov Chains with a Finite Attractor or the Global Coarseness Property.
Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Decidability and Complexity Results for Timed Automata via Channel Machines.
Proceedings of the Automata, Languages and Programming, 32nd International Colloquium, 2005

Verification of Parameterized Timed Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2005

2004
SAT-Solving the Coverability Problem for Petri Nets.
Formal Methods in System Design, 2004

Using Forward Reachability Analysis for Verification of Lossy Channel Systems.
Formal Methods in System Design, 2004

Better Quasi-Ordered Transition Systems
CoRR, 2004

Multi-Clock Timed Networks.
Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

Designing Safe, Reliable Systems using Scade.
Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2004

Designing Safe, Reliable Systems Using Scade.
Proceedings of the Leveraging Applications of Formal Methods, 2004

Decidability of Zenoness, Syntactic Boundedness and Token-Liveness for Dense-Timed Petri Nets.
Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

Forward Reachability Analysis of Timed Petri Nets.
Proceedings of the Formal Techniques, 2004

A Survey of Regular Model Checking.
Proceedings of the CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31, 2004

Regular Model Checking for LTL(MSO).
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003
Model checking of systems with many identical timed processes.
Theor. Comput. Sci., 2003

Verification of Probabilistic Systems with Faulty Communication.
Proceedings of the Foundations of Software Science and Computational Structures, 2003

Deciding Monotonic Games.
Proceedings of the Computer Science Logic, 17th International Workshop, 2003

Algorithmic Improvements in Regular Model Checking.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002
Regular Model Checking Made Simple and Efficient.
Proceedings of the CONCUR 2002, 2002

Regular Tree Model Checking.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
Ensuring completeness of symbolic verification methods for infinite-state systems.
Theor. Comput. Sci., 2001

Effective Lossy Queue Languages.
Proceedings of the Automata, Languages and Programming, 28th International Colloquium, 2001

Channel Representations in Protocol Verification.
Proceedings of the CONCUR 2001, 2001

Timed Petri Nets and BQOs.
Proceedings of the Application and Theory of Petri Nets 2001, 2001

2000
Algorithmic Analysis of Programs with Well Quasi-ordered Domains.
Inf. Comput., 2000

Symbolic Reachability Analysis Based on SAT-Solvers.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

Better is Better than Well: On Efficient Verification of Infinite-State Systems.
Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

Reasoning about Probabilistic Lossy Channel Systems.
Proceedings of the CONCUR 2000, 2000

Invited Tutorial: Verification of Infinite-State and Parameterized Systems.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Unfoldings of Unbounded Petri Nets.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999
Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1999

Handling Global Conditions in Parameterized System Verification.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

On the Existence of Network Invariants for Verifying Parameterized Systems.
Proceedings of the Correct System Design, 1999

1998
Verifying Networks of Timed Processes (Extended Abstract).
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998

Simulation Is Decidable for One-Counter Nets (Extended Abstract).
Proceedings of the CONCUR '98: Concurrency Theory, 1998

A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract).
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997
An Improved Search Strategy for Lossy Channel Systems.
Proceedings of the Formal Description Techniques and Protocol Specification, 1997

1996
Undecidable Verification Problems for Programs with Unreliable Channels.
Inf. Comput., 1996

Verifying Programs with Unreliable Channels.
Inf. Comput., 1996

General Decidability Theorems for Infinite-State Systems.
Proceedings of the Proceedings, 1996

1995
Decidability of Simulation and Bisimulation between Lossy Channel Systems and Finite State Systems (Extended Abstract).
Proceedings of the CONCUR '95: Concurrency Theory, 1995

1994
Undecidable Verification Problems for Programs with Unreliable Channels.
Proceedings of the Automata, Languages and Programming, 21st International Colloquium, 1994

1993
Verifying Programs with Unreliable Channels
Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

1992
Automatic Verification of a Class Systolic Circuits.
Formal Asp. Comput., 1992

1988
An Equivalence Decision Problem in Systolic Array Verification.
Proceedings of the Specification and Verification of Concurrent Systems [BCS-FACS Workshop, 1988


  Loading...