Parosh Abdulla
Professor at Department of Information Technology; Division of Computer Systems
- Telephone:
- +46 18 471 31 63
- Mobile phone:
- +46 70 425 02 16
- E-mail:
- Parosh.Abdulla@it.uu.se
- Visiting address:
- Hus 10, Lägerhyddsvägen 1
- Postal address:
- Box 337
751 05 UPPSALA
Publications
Recent publications
When GNNs Met a Word Equations Solver: Learning to Rank Equations
2025
Parsimonious Optimal Dynamic Partial Order Reduction
2024
Guiding Word Equation Solving using Graph Neural Networks
Part of Automated Technology for Verification and Analysi, p. 279-301, 2024
Boosting Constrained Horn Solving by Unsat Core Learning
Part of Verification, Model Checking, and Abstract Interpretation, p. 280-302, 2024
Parsimonious Optimal Dynamic Partial Order Reduction
Part of COMPUTER AIDED VERIFICATION, PT II, CAV 2024, p. 19-43, 2024
- DOI for Parsimonious Optimal Dynamic Partial Order Reduction
- Download full text (pdf) of Parsimonious Optimal Dynamic Partial Order Reduction
All publications
Articles in journal
Verification under Intel-x86 with Persistency
Part of Proceedings of the ACM on Programming Languages, 2024
- DOI for Verification under Intel-x86 with Persistency
- Download full text (pdf) of Verification under Intel-x86 with Persistency
Optimal Reads-From Consistency Checking for C11-Style Memory Models
Part of Proceedings of the ACM on Programming Languages, p. 761-785, 2023
- DOI for Optimal Reads-From Consistency Checking for C11-Style Memory Models
- Download full text (pdf) of Optimal Reads-From Consistency Checking for C11-Style Memory Models
Deciding Reachability under Persistent x86-TSO
Part of Proceedings of the ACM on Programming Languages, 2021
- DOI for Deciding Reachability under Persistent x86-TSO
- Download full text (pdf) of Deciding Reachability under Persistent x86-TSO
Parameterized verification under TSO is PSPACE-complete
Part of Proceedings of the ACM on Programming Languages, 2020
- DOI for Parameterized verification under TSO is PSPACE-complete
- Download full text (pdf) of Parameterized verification under TSO is PSPACE-complete
Optimal stateless model checking for reads-from equivalence under sequential consistency
Part of Proceedings of the ACM on Programming Languages, 2019
- DOI for Optimal stateless model checking for reads-from equivalence under sequential consistency
- Download full text (pdf) of Optimal stateless model checking for reads-from equivalence under sequential consistency
Part of Computing, p. 1-2, 2019
Mending fences with self-invalidation and self-downgrade
Part of Logical Methods in Computer Science, 2018
A load-buffer semantics for total store ordering
Part of Logical Methods in Computer Science, 2018
Optimal Stateless Model Checking under the Release-Acquire Semantics
Part of Proceedings of the ACM on Programming Languages, p. 1-29, 2018
- DOI for Optimal Stateless Model Checking under the Release-Acquire Semantics
- Download full text (pdf) of Optimal Stateless Model Checking under the Release-Acquire Semantics
Part of International Journal on Software Tools for Technology Transfer, p. 549-563, 2017
Flatten and Conquer: A Framework for Efficient Analysis of String Constraints
Part of SIGPLAN notices, p. 602-617, 2017
Stateless model checking for TSO and PSO
Part of Acta Informatica, p. 789-818, 2017
Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction
Part of Journal of the ACM, 2017
Verification of heap manipulating programs with ordered data by extended forest automata
Part of Acta Informatica, p. 357-385, 2016
Parameterized verification through view abstraction
Part of International Journal on Software Tools for Technology Transfer, p. 495-516, 2016
Part of International Journal on Software Tools for Technology Transfer, p. 469-473, 2016
Parameterized verification of time-sensitive models of ad hoc network protocols
Part of Theoretical Computer Science, p. 1-22, 2016
Well Structured Transition Systems with History
Part of Electronic Proceedings in Theoretical Computer Science, p. 115-128, 2015
Stochastic Parity Games on Lossy Channel Systems
Part of Logical Methods in Computer Science, 2014
- DOI for Stochastic Parity Games on Lossy Channel Systems
- Download full text (pdf) of Stochastic Parity Games on Lossy Channel Systems
Mediating for reduction (on minimizing alternating Buchi automata)
Part of Theoretical Computer Science, p. 26-43, 2014
Budget-bounded model-checking pushdown systems
Part of Formal methods in system design, p. 273-301, 2014
Part of Logical Methods in Computer Science, 2013
Monotonic abstraction for programs with multiply-linked structures
Part of International Journal of Foundations of Computer Science, p. 187-210, 2013
- DOI for Monotonic abstraction for programs with multiply-linked structures
- Download full text (pdf) of Monotonic abstraction for programs with multiply-linked structures
Part of International Journal on Software Tools for Technology Transfer, p. 109-118, 2012
Regular model checking for LTL(MSO)
Part of International Journal on Software Tools for Technology Transfer, p. 223-241, 2012
Automatic verification of directory-based consistency protocols with graph constraints
Part of International Journal of Foundations of Computer Science, p. 761-782, 2011
A classification of the expressive power of well-structured transition systems
Part of Information and Computation, p. 248-279, 2011
Sampled semantics of timed automata
Part of Logical Methods in Computer Science, 2010
Well (and better) quasi-ordered transition systems
Part of Bulletin of Symbolic Logic, p. 457-515, 2010
A uniform (bi-)simulation-based framework for reducing tree automata
Part of Electronic Notes in Theoretical Computer Science, p. 27-48, 2009
Universality of R-automata with value copying
Part of Electronic Notes in Theoretical Computer Science, p. 131-141, 2009
Composed bisimulation for tree automata
Part of International Journal of Foundations of Computer Science, p. 685-700, 2009
Monotonic Abstraction: on Efficient Verification of Parameterized Systems
Part of International Journal of Foundations of Computer Science, p. 779-801, 2009
Approximated parameterized verification of infinite-state processes with global conditions
Part of Formal methods in system design, p. 126-156, 2009
Monotonic Abstraction in Parameterized Verification
Part of Electronic Notes in Theoretical Computer Science, p. 3-14, 2008
Part of SIGARCH Computer Architecture News, p. 72-79, 2008
Universality Analysis for One-Clock Timed Automata
Part of Fundamenta Informaticae, p. 419-450, 2008
Monotonic and downward closed games
Part of Journal of logic and computation (Print), p. 153-169, 2008
Part of Logical Methods in Computer Science, p. 1-32, 2007
Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness
Part of Logical Methods in Computer Science, p. 1-61, 2007
Using Forward Reachability Analysis for Verification of Timed Petri Nets
Part of Nordic Journal of Computing, p. 1-42, 2007
Bisimulation minimization of tree automata
Part of International Journal of Foundations of Computer Science, p. 699-713, 2007
Simulating perfect channels with probabilistic lossy channels
Part of Information and Computation, p. 22-40, 2005
Using Forward Reachability Analysis for Verification of Lossy Channel Systems
Part of Formal methods in system design, p. 39-65, 2004
SAT-solving the Coverability Problem for Unbounded Petri Nets
Part of Formal methods in system design, p. 25-43, 2004
Algorithmic analysis of programs with well quasi-ordered domains
Part of INFORMATION AND COMPUTATION, p. 109-127, 2000
Verifying programs with unreliable channels
Part of Information and Computation, p. 91-101, 1996
Articles, review/survey
Part of International Journal on Software Tools for Technology Transfer, p. 85-88, 2013
Chapters in book
Trading Space for Simplicity in Stateless Model Checking
Part of Real Time and Such, p. 79-97, Springer, 2024
Consistency and Persistency in Program Verification: Challenges and Opportunities
Part of Principles of Systems Design, p. 494-510, Springer, 2022
Model checking parameterized systems
Part of Handbook of Model Checking, p. 685-725, Springer, 2018
Comparing source sets and persistent sets for partial order reduction
Part of Models, Algorithms, Logics and Tools, p. 516-536, Springer, 2017
On the existence of network invariants for verifying parameterized systems
Part of Correct System Design, p. 180-197, Springer-Verlag, Berlin, 1999
Conference papers
Parsimonious Optimal Dynamic Partial Order Reduction
2024
Guiding Word Equation Solving using Graph Neural Networks
Part of Automated Technology for Verification and Analysi, p. 279-301, 2024
Boosting Constrained Horn Solving by Unsat Core Learning
Part of Verification, Model Checking, and Abstract Interpretation, p. 280-302, 2024
Parsimonious Optimal Dynamic Partial Order Reduction
Part of COMPUTER AIDED VERIFICATION, PT II, CAV 2024, p. 19-43, 2024
- DOI for Parsimonious Optimal Dynamic Partial Order Reduction
- Download full text (pdf) of Parsimonious Optimal Dynamic Partial Order Reduction
Concurrent Stochastic Lossy Channel Games
Part of 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), 2024
- DOI for Concurrent Stochastic Lossy Channel Games
- Download full text (pdf) of Concurrent Stochastic Lossy Channel Games
Verification under TSO with an infinite Data Domain
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 276-295, 2024
- DOI for Verification under TSO with an infinite Data Domain
- Download full text (pdf) of Verification under TSO with an infinite Data Domain
Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs
2023
Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs
Part of Automated Technology for Verification and Analysis, 21st International Symposium, ATVA 2023, Singapore, Oct. 2023. Proceedings., 2023
Part of Computer Aided Verification - 35th International Conference, {CAV} 2023, Paris, France, July 17-22, 2023, Proceedings, Part {I}}, p. 184-205, 2023
Parameterized Verification under TSO with Data Types
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 588-606, 2023
- DOI for Parameterized Verification under TSO with Data Types
- Download full text (pdf) of Parameterized Verification under TSO with Data Types
Optimal Stateless Model Checking for Causal Consistency
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 105-125, 2023
- DOI for Optimal Stateless Model Checking for Causal Consistency
- Download full text (pdf) of Optimal Stateless Model Checking for Causal Consistency
Probabilistic Total Store Ordering
Part of Programming Languages And Systems, ESOP 2022, p. 317-345, 2022
- DOI for Probabilistic Total Store Ordering
- Download full text (pdf) of Probabilistic Total Store Ordering
Verifying Reachability for TSO Programs with Dynamic Thread Creation
Part of Networked Systems, NETYS 2022, p. 283-300, 2022
On the State Reachability Problem for Concurrent Programs Under Power
Part of Networked Systems - 8th International Conference, {NETYS} 2020, Morocco, Revised Selected Papers, p. 47-59, 2021
The Decidability of Verification under PS 2.0
Part of Programming Languages And Systems, ESOP 2021, p. 1-29, 2021
- DOI for The Decidability of Verification under PS 2.0
- Download full text (pdf) of The Decidability of Verification under PS 2.0
Solving Not-Substring Constraint with Flat Abstraction
Part of Programming Languages And Systems, APLAS 2021, p. 305-320, 2021
On the Separability Problem of String Constraints
Part of 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), 2020
On the Formalization of Decentralized Contact Tracing Protocols
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
Part of PLDI 2020, p. 943-957, 2020
Verification of programs under the release-acquire semantics
Part of Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, p. 1117-1132, 2019
Part of Automated Technology for Verification and Analysis, p. 277-293, 2019
Reachability in database-driven systems with numerical attributes under recency bounding
Part of PODS '19, p. 335-352, 2019
Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)
Part of Networked Systems, p. 3-18, 2019
Replacing store buffers by load buffers in TSO
Part of Verification and Evaluation of Computer and Communication Systems, p. 22-28, 2018
Trau: SMT solver for string constraints
Part of Proceedings of the 2018 18th Conference on Formal Methods in Computer Aided Design (FMCAD), 2018
Verification of timed asynchronous programs
Part of IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018
Universal safety for timed Petri nets is PSPACE-complete
Part of 29th International Conference on Concurrency Theory, 2018
Complexity of reachability for data-aware dynamic systems
Part of Proc. 18th International Conference on Application of Concurrency to System Design, p. 11-20, 2018
Optimal Stateless Model Checking under the Release-Acquire Semantics
Part of SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018, 2018
Fragment abstraction for concurrent shape analysis
Part of Programming Languages and Systems, p. 442-471, 2018
Perfect timed communication is hard
Part of Formal Modeling and Analysis of Timed Systems, p. 91-107, 2018
Context-bounded analysis for POWER
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 56-74, 2017
Part of The 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, 2017
Automated Verification of Linearization Policies
Part of Automated Verification of Linearization Policies, 2016
The benefits of duality in verifying concurrent programs under TSO
Part of 27th International Conference on Concurrency Theory, 2016
Recency-Bounded Verification of Dynamic Database-Driven Systems
Part of PODS'16, p. 195-210, 2016
Fencing programs with self-invalidation and self-downgrade
Part of Formal Techniques for Distributed Objects, Components, and Systems, p. 19-35, 2016
Data Communicating Processes with Unreliable Channels
Part of Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016), p. 166-175, 2016
Qualitative Analysis of VASS-Induced MDPs
Part of Foundations Of Software Science And Computation Structures (FOSSACS 2016), p. 319-334, 2016
Stateless model checking for POWER
Part of Computer Aided Verification, p. 134-156, 2016
Counter-Example Guided Program Verification
Part of FM 2016, p. 25-42, 2016
Precise and sound automatic fence insertion procedure under PSO
Part of Networked Systems, p. 32-47, 2015
The Best of Both Worlds: Trading efficiency and optimality in fence insertion for TSO
Part of Programming Languages and Systems, p. 308-332, 2015
Verification of Cache Coherence Protocols wrt. Trace Filters
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
Part of Formal Aspects of Component Software, p. 198-206, 2015
Stateless model checking for TSO and PSO
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 353-367, 2015
Verification of buffered dynamic register automata
Part of Networked Systems, p. 15-31, 2015
What's decidable about availability languages?
Part of Proc. 35th IARCS Conference on Foundation of Software Technology and Theoretical Computer Science, p. 192-205, 2015
Norn: An SMT solver for string constraints
Part of Computer Aided Verification, p. 462-469, 2015
Verification of Dynamic Register Automata
Part of Leibniz International Proceedings in Informatics, 2014
Optimal dynamic partial order reduction
Part of Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 373-384, 2014
Block me if you can!: Context-sensitive parameterized verification
Part of Static Analysis, p. 1-17, 2014
- DOI for Block me if you can!: Context-sensitive parameterized verification
- Download full text (pdf) of Block me if you can!: Context-sensitive parameterized verification
Computing optimal reachability costs in priced dense-timed pushdown automata
Part of Language and Automata Theory and Applications, p. 62-75, 2014
String Constraints for Verification
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
Zenoness for Timed Pushdown Automata
Part of Proceedings 15th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2013, Hanoi, Vietnam, 14th October 2013., 2014
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
Verifying safety and liveness for the FlexTM hybrid transactional memory
p. 785-790, 2013
MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 530-536, 2013
- DOI for MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO
- Download full text (pdf) of MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO
Analysis of message passing programs using SMT-solvers
Part of Automated Technology for Verification and Analysis, p. 272-286, 2013
Verification of heap manipulating programs with ordered data by extended forest automata
Part of Automated Technology for Verification and Analysis, p. 224-239, 2013
- DOI for Verification of heap manipulating programs with ordered data by extended forest automata
- Download full text (pdf) of Verification of heap manipulating programs with ordered data by extended forest automata
Solving parity games on integer vectors
Part of CONCUR 2013 – Concurrency Theory, p. 106-120, 2013
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
Part of Tools and Algorithms for the Construction and Analysis of Systems, 2013
Push-down automata with gap-order constraints
Part of Fundamentals of Software Engineering, p. 199-216, 2013
Verification of Directed Acyclic Ad Hoc Networks
Part of Formal Techniques for Distributed Systems, p. 193-208, 2013
- DOI for Verification of Directed Acyclic Ad Hoc Networks
- Download full text (pdf) of Verification of Directed Acyclic Ad Hoc Networks
All for the price of few: (Parameterized verification through view abstraction)
Part of Verification, Model Checking, and Abstract Interpretation, p. 476-495, 2013
- DOI for All for the price of few: (Parameterized verification through view abstraction)
- Download full text (pdf) of All for the price of few: (Parameterized verification through view abstraction)
Part of Proc. 27th ACM/IEEE Symposium on Logic in Computer Science, p. 35-44, 2012
The minimal cost reachability problem in priced timed pushdown systems
Part of Language and Automata Theory and Applications, p. 58-69, 2012
Automatic fence insertion in integer programs via predicate abstraction
Part of Static Analysis, p. 164-180, 2012
Counter-Example Guided Fence Insertion under TSO
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 204-219, 2012
- DOI for Counter-Example Guided Fence Insertion under TSO
- Download full text (pdf) of Counter-Example Guided Fence Insertion under TSO
Multi-Pushdown Systems with Budgets
Part of Formal Methods in Computer-Aided Design, p. 24-33, 2012
2012
Adding time to pushdown automata
Part of Quantities in Formal Methods, p. 1-16, 2012
Part of IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, p. 374-386, 2012
Carrying Probabilities to the Infinite World
Part of CONCUR'2011, 22nd International Conference on Concurrency Theory., 2011
Advanced Ramsey-based Büchi automata inclusion testing
Part of CONCUR 2011 — Concurrency Theory, p. 187-202, 2011
Computing Optimal Coverability Costs in Priced Timed Petri Nets
Part of LICS'2011, Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, p. 399-408, 2011
On the verification of timed ad hoc networks
Part of Formal Modeling and Analysis of Timed Systems, p. 256-270, 2011
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 158-174, 2010
Forcing monotonicity in parameterized verification: From multisets to words
Part of SOFSEM 2010, p. 1-15, 2010
Constrained monotonic abstraction: A CEGAR for parameterized verification
Part of CONCUR 2010 – Concurrency Theory, p. 86-101, 2010
Simulation subsumption in Ramsey-based Büchi automata universality and inclusion testing
Part of Computer Aided Verification, p. 132-147, 2010
Analyzing the security in the GSM radio network using attack jungles
Part of Leveraging Applications of Formal Methods, Verification, and Validation, p. 60-74, 2010
Automatic Verification of Directory-Based Consistency Protocols
Part of Reachability Problems, p. 36-50, 2009
Approximated Context-Sensitive Analysis for Parameterized Verification
Part of Formal Techniques for Distributed Systems, p. 41-56, 2009
Part of Formal Techniques for Networked and Distributed Systems, p. 69-83, 2008
Monotonic abstraction in action: Automatic verification of distributed mutex algorithms
Part of Theoretical Aspects of Computing - ICTAC 2008, p. 50-65, 2008
Monotonic abstraction for programs with dynamic memory heaps
Part of Computer Aided Verification, p. 341-354, 2008
Handling parameterized systems with non-atomic global conditions
Part of Verification, Model Checking, and Abstract Interpretation, p. 22-36, 2008
Stochastic games with lossy channels
Part of Foundations of Software Science and Computational Structures, p. 35-49, 2008
Part of CONCUR 2008 - Concurrency Theory, p. 67-81, 2008
Part of Proc. 1st Swedish Workshop on Multi-Core Computing, p. 89-96, 2008
Composed Bisimulation for Tree Automata
Part of Implementation and Application of Automata, p. 212-222, 2008
Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 93-108, 2008
Zone-Based Universality Analysis for Single-Clock Timed Automata
Part of International Symposium on Fundamentals of Software Engineering, Proceedings, p. 98-112, 2007
Parameterized Verification of Infinite-state Processes with Global Conditions
Part of Computer Aided Verification, Proceedings, p. 145-157, 2007
Sampled universality of timed automata
Part of Foundations of Software Science and Computational Structures, Proceedings, p. 2-16, 2007
Regular Model Checking without Transducers
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
Part of Third International Conference on the Quantitative Evaluation of Systems (QEST), p. 253-262, 2006
Minimization of Non-deterministic Automata with Large Alphabets
Part of Implementation and Application of Automata, p. 31-42, 2006
Bisimulation Minimization of Tree Automata
Part of Implementation and Application of Automata, p. 173-185, 2006
Proving Liveness by Backwards Reachability
2006
Part of LICS'2004, 18th IEEE Int. Symp. on Logic in Computer Science, 2004
Open, Closed and Robust Timed Networks.
Part of CONCUR 2004 -- Concurrency Theory, p. 529, 2004
Regular Model Checking for LTL(MSO)
Part of Computer Aided Verification, p. 348-360, 2004
A Survey of Regular Model Checking.
Part of CONCUR 2004 - Concurrency Theory, p. 35-48, 2004
Report on Dataflow Dependencies in Billing Processing Systems
Part of Proc. ISoLA '04: 1st International Symposium on Leveraging Applications of Formal Methods, 2004
Designing Safe, Reliable Systems using Scade
Part of Proc. ISoLA '04: International Symposium on Leveraging Applications of Formal Methods, 2004
Effective Lossy Queue Languages.
Part of ICALP'2001, 28th Int. Colloquium on Automata, Languages and Programmming., 2001
Handling Global Conditions in Parameterized System Verification
Part of Proc. 11th Int. Conf. on Computer Aided Verification, p. 134-145, 1999
Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 208-222, 1999
Simulation is decidable for one-counter nets
Part of CONCUR'98 Concurrency Theory, p. 253-268, 1998
Verifying networks of timed processes
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 298-312, 1998
A general approach to partial order reductions in symbolic verification
Part of Computer Aided Verification, p. 379-390, 1998
Undecidable verification problems for programs with unreliable channels
Part of Automata, Languages and Programming, p. 71-90, 1996