Parosh Aziz Abdulla

Orcid: 0000-0001-6832-6611

Affiliations:
  • Uppsala University, Sweden


According to our database1, Parosh Aziz Abdulla authored at least 210 papers between 1988 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Verification under Intel-x86 with Persistency.
Proc. ACM Program. Lang., 2024

Boosting Constrained Horn Solving by Unsat Core Learning.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2024

Verification under TSO with an infinite Data Domain.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

Concurrent Stochastic Lossy Channel Games.
Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024

Parsimonious Optimal Dynamic Partial Order Reduction.
Proceedings of the Computer Aided Verification - 36th International Conference, 2024

Fairness and Liveness Under Weak Consistency.
Proceedings of the Taming the Infinities of Concurrency, 2024

2023
Optimal Reads-From Consistency Checking for C11-Style Memory Models.
Dataset, March, 2023

Optimal Reads-From Consistency Checking for C11-Style Memory Models.
Dataset, March, 2023

Optimal Reads-From Consistency Checking for C11-Style Memory Models.
Proc. ACM Program. Lang., 2023

Chain-Free String Constraints (Technical Report).
CoRR, 2023

Overcoming Memory Weakness with Unified Fairness.
CoRR, 2023

Optimal Stateless Model Checking for Causal Consistency.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Parameterized Verification under TSO with Data Types.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Overcoming Memory Weakness with Unified Fairness - Systematic Verification of Liveness in Weak Memory Models.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023

Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs.
Proceedings of the Automated Technology for Verification and Analysis, 2023

2022
Optimal SMC for Transactional Programs.
CoRR, 2022

Verifying Reachability for TSO Programs with Dynamic Thread Creation.
Proceedings of the Networked Systems - 10th International Conference, 2022

Probabilistic Total Store Ordering.
Proceedings of the Programming Languages and Systems, 2022

Consistency and Persistency in Program Verification: Challenges and Opportunities.
Proceedings of the Principles of Systems Design, 2022

2021
Correction to: An integrated specification and verification technique for highly concurrent data structures.
Int. J. Softw. Tools Technol. Transf., 2021

Deciding reachability under persistent x86-TSO.
Proc. ACM Program. Lang., 2021

The Decidability of Verification under PS 2.0.
Proceedings of the Programming Languages and Systems, 2021

Regular Model Checking: Evolution and Perspectives.
Proceedings of the Model Checking, Synthesis, and Learning, 2021

Solving Not-Substring Constraint withFlat Abstraction.
Proceedings of the Programming Languages and Systems - 19th Asian Symposium, 2021

2020
Parameterized verification under TSO is PSPACE-complete.
Proc. ACM Program. Lang., 2020

The Decidability of Verification under Promising 2.0.
CoRR, 2020

Efficient handling of string-number conversion.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

On the Formalization of Decentralized Contact Tracing Protocols.
Proceedings of the 2nd Workshop on Artificial Intelligence and Formal Verification, 2020

On the State Reachability Problem for Concurrent Programs Under Power.
Proceedings of the Networked Systems - 8th International Conference, 2020

On the Separability Problem of String Constraints.
Proceedings of the 31st International Conference on Concurrency Theory, 2020

2019
Optimal Stateless Model Checking for Reads-From Equivalence under Sequential Consistency.
Dataset, October, 2019

Optimal stateless model checking for reads-from equivalence under sequential consistency.
Proc. ACM Program. Lang., 2019

Special Issue on NETYS'2016.
Computing, 2019

Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding.
Proceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, 2019

Verification of programs under the release-acquire semantics.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial).
Proceedings of the Networked Systems - 7th International Conference, 2019

Chain-Free String Constraints.
Proceedings of the Automated Technology for Verification and Analysis, 2019

2018
Model Checking Parameterized Systems.
Proceedings of the Handbook of Model Checking., 2018

Optimal stateless model checking under the release-acquire semantics.
Proc. ACM Program. Lang., 2018

Mending Fences with Self-Invalidation and Self-Downgrade.
Log. Methods Comput. Sci., 2018

A Load-Buffer Semantics for Total Store Ordering.
Log. Methods Comput. Sci., 2018

Replacing Store Buffers by Load Buffers in TSO.
Proceedings of the Verification and Evaluation of Computer and Communication Systems, 2018

Verification of Timed Asynchronous Programs.
Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018

Perfect Timed Communication Is Hard.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2018

Trau: SMT solver for string constraints.
Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Fragment Abstraction for Concurrent Shape Analysis.
Proceedings of the Programming Languages and Systems, 2018

Universal Safety for Timed Petri Nets is PSPACE-complete.
Proceedings of the 29th International Conference on Concurrency Theory, 2018

Complexity of Reachability for Data-Aware Dynamic Systems.
Proceedings of the 18th International Conference on Application of Concurrency to System Design, 2018

2017
An integrated specification and verification technique for highly concurrent data structures.
Int. J. Softw. Tools Technol. Transf., 2017

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

What is Decidable about Perfect Timed Channels?
CoRR, 2017

Stateless model checking for TSO and PSO.
Acta Informatica, 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.
Int. J. Softw. Tools Technol. Transf., 2016

Parameterized verification.
Int. J. Softw. Tools Technol. Transf., 2016

Preface.
Fundam. Informaticae, 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 Informatica, 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

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 Syst. Des., 2014

Stochastic Parity Games on Lossy Channel Systems.
Log. Methods Comput. Sci., 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.
Int. J. Softw. Tools Technol. Transf., 2013

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

Priced Timed Petri Nets.
Log. Methods Comput. Sci., 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

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

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

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).
Int. J. Softw. Tools Technol. Transf., 2012

Regular model checking.
Int. J. Softw. Tools Technol. Transf., 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.
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
Log. Methods Comput. Sci., 2010

Well (and better) quasi-ordered transition systems.
Bull. Symb. Log., 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 Syst. Des., 2009

Universality of R-automata with Value Copying.
Proceedings of the Joint Proceedings of the 8th, 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

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 Comput. Archit. News, 2008

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

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

A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata.
Proceedings of the International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2008

Monotonic Abstraction in Parameterized Verification.
Proceedings of the Second Workshop on Reachability Problems in Computational Models, 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.
Log. Methods Comput. Sci., 2007

Decisive Markov Chains.
Log. Methods Comput. Sci., 2007

Bisimulation Minimization of Tree Automata.
Int. J. Found. Comput. Sci., 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. Algebraic Methods Program., 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

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 Syst. Des., 2004

Using Forward Reachability Analysis for Verification of Lossy Channel Systems.
Formal Methods Syst. Des., 2004

Closed, Open, and Robust Timed Networks.
Proceedings of the 6th International Workshop on Verification of Infinite-State Systems, 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

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

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

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

1990
Decision problems in systolic circuit verification.
PhD thesis, 1990

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


  Loading...