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