Javier Esparza

J. ACM, April, 2024

Fast and succinct population protocols for Presburger arithmetic.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., March, 2024

Separators in Continuous Petri Nets.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2024

Validity of contextual formulas (extended version).

[BibT_eX]

[DOI]

CoRR, 2024

A Resolution-Based Interactive Proof System for UNSAT.

[BibT_eX]

[DOI]

Valentin Krasotin

Proceedings of the Foundations of Software Science and Computation Structures, 2024

Validity of Contextual Formulas.

[BibT_eX]

[DOI]

Proceedings of the 35th International Conference on Concurrency Theory, 2024

Computing Inductive Invariants of Regular Abstraction Frameworks.

[BibT_eX]

[DOI]

Valentin Krasotin

Christoph Welzel-Mohr

Proceedings of the 35th International Conference on Concurrency Theory, 2024

2023

Lower bounds on the state complexity of population protocols.

[BibT_eX]

[DOI]

Jérôme Leroux

Distributed Comput., September, 2023

Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy.

[BibT_eX]

[DOI]

A. R. Balasubramanian

Log. Methods Comput. Sci., 2023

Making IP=PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms.

[BibT_eX]

[DOI]

CoRR, 2023

Black-Box Testing Liveness Properties of Partially Observable Stochastic Systems.

[BibT_eX]

[DOI]

Vincent P. Grande

Proceedings of the 50th International Colloquium on Automata, Languages, and Programming, 2023

Geometry of Reachability Sets of Vector Addition Systems.

[BibT_eX]

[DOI]

Roland Guttenberg

Proceedings of the 34th International Conference on Concurrency Theory, 2023

Making sf IP=sf PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

Examples for submission to CONCUR'22.

[BibT_eX]

[DOI]

Dataset, April, 2022

Examples for submission to CONCUR'22.

[BibT_eX]

[DOI]

Dataset, April, 2022

From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2022

Computing Parameterized Invariants of Parameterized Petri Nets.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2022

Regular Model Checking Upside-Down: An Invariant-Based Approach.

[BibT_eX]

[DOI]

Proceedings of the 33rd International Conference on Concurrency Theory, 2022

A Simple Rewrite System for the Normalization of Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Principles of Systems Design, 2022

2021

The 2021 Alonzo Church award for outstanding contributions to logic and computation: call for nominations.

[BibT_eX]

[DOI]

ACM SIGLOG News, 2021

Towards efficient verification of population protocols.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2021

TheoretiCS.

[BibT_eX]

[DOI]

Uri Zwick

Bull. EATCS, 2021

2021 Alonzo Church Award for Outstanding Contributions to Logic and Computation.

[BibT_eX]

[DOI]

Bull. EATCS, 2021

The complexity of verifying population protocols.

[BibT_eX]

[DOI]

Distributed Comput., 2021

Abduction of trap invariants in parameterized systems.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 12th International Symposium on Games, 2021

Back to the Future: A Fresh Look at Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Implementation and Application of Automata, 2021

Population Protocols: Beyond Runtime Analysis.

[BibT_eX]

[DOI]

Proceedings of the Reachability Problems - 15th International Conference, 2021

Decision Power of Weak Asynchronous Models of Distributed Computing.

[BibT_eX]

[DOI]

Proceedings of the PODC '21: ACM Symposium on Principles of Distributed Computing, 2021

Lower Bounds on the State Complexity of Population Protocols.

[BibT_eX]

[DOI]

Proceedings of the PODC '21: ACM Symposium on Principles of Distributed Computing, 2021

State Complexity of Population Protocols (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2021

Enforcing ω-Regular Properties in Markov Chains by Restarting.

[BibT_eX]

[DOI]

Proceedings of the 32nd International Conference on Concurrency Theory, 2021

Verification.

[BibT_eX]

[DOI]

Orna Kupferman

Moshe Y. Vardi

Proceedings of the Handbook of Automata Theory., 2021

2020

heron.

[BibT_eX]

[DOI]

Dataset, October, 2020

heron.

[BibT_eX]

[DOI]

Dataset, October, 2020

heron.

[BibT_eX]

[DOI]

Dataset, October, 2020

heron.

[BibT_eX]

[DOI]

Dataset, October, 2020

heron.

[BibT_eX]

[DOI]

Dataset, July, 2020

ostrich.

[BibT_eX]

[DOI]

Dataset, February, 2020

ostrich.

[BibT_eX]

[DOI]

Dataset, February, 2020

A Unified Translation of Linear Temporal Logic to ω-Automata.

[BibT_eX]

[DOI]

J. ACM, 2020

Online Monitoring ω-Regular Properties in Unknown Markov Chains.

[BibT_eX]

[DOI]

CoRR, 2020

Structural Invariants for the Verification of Systems with Parameterized Architectures.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Succinct Population Protocols for Presburger Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the 37th International Symposium on Theoretical Aspects of Computer Science, 2020

An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata.

[BibT_eX]

[DOI]

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Flatness and Complexity of Immediate Observation Petri Nets.

[BibT_eX]

[DOI]

Chana Weil-Kennedy

Proceedings of the 31st International Conference on Concurrency Theory, 2020

A Classification of Weak Asynchronous Models of Distributed Computing.

[BibT_eX]

[DOI]

Fabian Reiter

Proceedings of the 31st International Conference on Concurrency Theory, 2020

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2020

Complexity of Verification and Synthesis of Threshold Automata.

[BibT_eX]

[DOI]

A. R. Balasubramanian

Marijana Lazic

Proceedings of the Automated Technology for Verification and Analysis, 2020

2019

Expressive Power of Oblivious Consensus Protocols.

[BibT_eX]

[DOI]

CoRR, 2019

Negotiation as concurrency primitive.

[BibT_eX]

[DOI]

Acta Informatica, 2019

Computing the Expected Execution Time of Probabilistic Workflow Nets.

[BibT_eX]

[DOI]

Philipp J. Meyer

Philip Offtermatt

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Expressive Power of Broadcast Consensus Protocols.

[BibT_eX]

[DOI]

Proceedings of the 30th International Conference on Concurrency Theory, 2019

Parameterized Analysis of Immediate Observation Petri Nets.

[BibT_eX]

[DOI]

Chana Weil-Kennedy

Proceedings of the Application and Theory of Petri Nets and Concurrency, 2019

Coffee and Cigarettes.

[BibT_eX]

[DOI]

Proceedings of the Carl Adam Petri: Ideas, Personality, Impact, 2019

2018

Model Checking Procedural Programs.

[BibT_eX]

[DOI]

Rajeev Alur

Proceedings of the Handbook of Model Checking., 2018

Soundness in negotiations.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2018

Alonzo Church Award 2018 - Call for Nominations.

[BibT_eX]

[DOI]

Bull. EATCS, 2018

Formal Methods and Fault-Tolerant Distributed Comp.: Forging an Alliance (Dagstuhl Seminar 18211).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2018

Preface for the special issue GandALF 2015.

[BibT_eX]

[DOI]

Enrico Tronci

Acta Informatica, 2018

Computing the Concurrency Threshold of Sound Free-Choice Workflow Nets.

[BibT_eX]

[DOI]

Philipp J. Meyer

Hagen Völzer

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Large Flocks of Small Birds: on the Minimal Size of Population Protocols.

[BibT_eX]

[DOI]

Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science, 2018

One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Black Ninjas in the Dark: Formal Analysis of Population Protocols.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Verification of Immediate Observation Population Protocols.

[BibT_eX]

[DOI]

Proceedings of the 29th International Conference on Concurrency Theory, 2018

Automatic Analysis of Expected Termination Time for Population Protocols.

[BibT_eX]

[DOI]

Proceedings of the 29th International Conference on Concurrency Theory, 2018

Peregrine: A Tool for the Analysis of Population Protocols.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

Minimizing Test Suites with Unfoldings of Multithreaded Programs.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2017

Polynomial analysis algorithms for free choice Probabilistic Workflow Nets.

[BibT_eX]

[DOI]

Ratul Saha

Perform. Evaluation, 2017

Model checking parameterized asynchronous shared-memory systems.

[BibT_eX]

[DOI]

Antoine Durand-Gasselin

Rupak Majumdar

Formal Methods Syst. Des., 2017

Quantitative Implementation Strategies for Safety Controllers.

[BibT_eX]

[DOI]

CoRR, 2017

Verification of population protocols.

[BibT_eX]

[DOI]

Acta Informatica, 2017

Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 24th International Symposium on Temporal Representation and Reasoning, 2017

From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Static analysis of deterministic negotiations.

[BibT_eX]

[DOI]

Anca Muscholl

Igor Walukiewicz

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Advances in Parameterized Verification of Population Protocols.

[BibT_eX]

[DOI]

Proceedings of the Computer Science - Theory and Applications, 2017

2016

Parameterized Verification of Crowds of Anonymous Processes.

[BibT_eX]

[DOI]

Proceedings of the Dependable Software Systems Engineering, 2016

Negotiations and Petri Nets.

[BibT_eX]

[DOI]

Trans. Petri Nets Other Model. Concurr., 2016

Parameterized Verification of Asynchronous Shared-Memory Systems.

[BibT_eX]

[DOI]

Rupak Majumdar

J. ACM, 2016

Existence of home states in Petri nets is decidable.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2016

From LTL to deterministic automata - A safraless compositional approach.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2016

Model Checking Population Protocols.

[BibT_eX]

[DOI]

Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

Reduction Rules for Colored Workflow Nets.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2016

Limit-Deterministic Büchi Automata for Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

FPSOLVE: A Generic Solver for Fixpoint Equations Over Semirings.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2015

Distributed Markov Chains.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

An SMT-based Approach to Fair Termination Analysis.

[BibT_eX]

[DOI]

Philipp J. Meyer

Proceedings of the Formal Methods in Computer-Aided Design, 2015

Negotiation Programs.

[BibT_eX]

[DOI]

Proceedings of the Application and Theory of Petri Nets and Concurrency, 2015

Unfolding Based Minimal Test Suites for Testing Multithreaded Programs.

[BibT_eX]

[DOI]

Proceedings of the 15th International Conference on Application of Concurrency to System Design, 2015

2014

Pattern-Based Verification for Multithreaded Programs.

[BibT_eX]

[DOI]

Tomás Poch

ACM Trans. Program. Lang. Syst., 2014

Reachability Problems for Infinite-State Systems (Dagstuhl Seminar 14141).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2014

Negotiation Games.

[BibT_eX]

[DOI]

CoRR, 2014

Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Corrected version).

[BibT_eX]

[DOI]

CoRR, 2014

A Fully Verified Executable LTL Model Checker.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2014

Message-Passing Algorithms for the Verification of Distributed Protocols.

[BibT_eX]

[DOI]

Loïg Jezequel

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), 2014

A Brief History of Strahler Numbers.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2014

On Negotiation as Concurrency Primitive II: Deterministic Cyclic Negotiations.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2014

Fast and Accurate Unlexicalized Parsing via Structural Annotations.

[BibT_eX]

[DOI]

Proceedings of the 14th Conference of the European Chapter of the Association for Computational Linguistics, 2014

Deterministic Negotiations: Concurrency for Free.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

An SMT-Based Approach to Coverability Analysis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

From LTL to Deterministic Automata: A Safraless Compositional Approach.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

A strongly polynomial algorithm for criticality of branching processes and consistency of stochastic context-free grammars.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2013

Analyzing probabilistic pushdown automata.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2013

Computation of Summaries Using Net Unfoldings.

[BibT_eX]

[DOI]

Loïg Jezequel

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2013

On Negotiation as Concurrency Primitive.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

2012

Space-efficient scheduling of stochastically generated tasks.

[BibT_eX]

[DOI]

Inf. Comput., 2012

A Perfect Model for Bounded Verification.

[BibT_eX]

[DOI]

Rupak Majumdar

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Deterministic Automata for the (F, G)-Fragment of LTL.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Proving Termination of Probabilistic Programs Using Patterns.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Rabinizer: Small Deterministic Automata for LTL(F, G).

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2012

Reactive and Proactive Diagnosis of Distributed Systems Using Net Unfoldings.

[BibT_eX]

[DOI]

Christian Kern

Proceedings of the 12th International Conference on Application of Concurrency to System Design, 2012

Three Case Studies on Verification of Infinite-State Systems.

[BibT_eX]

[DOI]

Jörg Kreiker

Proceedings of the Modern Applications of Automata Theory., 2012

2011

Derivation tree analysis for accelerated fixed-point computation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2011

Parikhʼs theorem: A simple and direct automaton construction.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2011

Learning Workflow Petri Nets.

[BibT_eX]

[DOI]

Martin Leucker

Fundam. Informaticae, 2011

Probabilistic Abstractions with Arbitrary Domains.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 18th International Symposium, 2011

Complexity of pattern-based verification for multithreaded programs.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Solving Fixed-Point Equations by Derivation Tree Analysis.

[BibT_eX]

[DOI]

Proceedings of the Algebra and Coalgebra in Computer Science, 2011

2010

Newtonian Program Analysis - An Introduction.

[BibT_eX]

[DOI]

Proceedings of the Logics and Languages for Reliability and Security, 2010

Computing the Least Fixed Point of Positive Polynomial Systems.

[BibT_eX]

[DOI]

SIAM J. Comput., 2010

Newtonian program analysis.

[BibT_eX]

[DOI]

J. ACM, 2010

Parikh's Theorem: A simple and direct construction

[BibT_eX]

[DOI]

CoRR, 2010

Analysis of Systems with Stochastic Process Creation.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2010

Computing Least Fixed Points of Probabilistic Systems of Polynomials.

[BibT_eX]

[DOI]

Proceedings of the 27th International Symposium on Theoretical Aspects of Computer Science, 2010

A False History of True Concurrency: From Petri to Tools.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2010

Verification of Graph Transformation Systems with Context-Free Specifications.

[BibT_eX]

[DOI]

Barbara König

Proceedings of the Graph Transformations - 5th International Conference, 2010

Automatic Error Correction of Java Programs.

[BibT_eX]

[DOI]

Christian Kern

Proceedings of the Formal Methods for Industrial Critical Systems, 2010

2009

FTOS-Verify: Analysis and Verification of Non-Functional Properties for Fault-Tolerant Systems

[BibT_eX]

[DOI]

CoRR, 2009

On least fixed points of systems of positive polynomials.

[BibT_eX]

[DOI]

ACM Commun. Comput. Algebra, 2009

Stochastic Process Creation.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2009, 2009

On the Memory Consumption of Probabilistic Pushdown Automata.

[BibT_eX]

[DOI]

Tomás Brázdil

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2009

Solving Fixed-Point Equations on omega-Continuous Semirings.

[BibT_eX]

[DOI]

Proceedings of the 6th Workshop on Fixed Points in Computer Science, 2009

Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness.

[BibT_eX]

[DOI]

Proceedings of the 13th IEEE/ACM International Symposium on Distributed Simulation and Real Time Applications, 2009

Examining robotic systems with shape-adjustable manipulators under dynamic environments: From simulation to verification.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Symposium on Computational Intelligence in Robotics and Automation, 2009

2008

Unfoldings - A Partial-Order Approach to Model Checking

[BibT_eX]

[DOI]

Keijo Heljanko

Monographs in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-540-77426-6, 2008

A negative result on depth-first net unfoldings.

[BibT_eX]

[DOI]

Pradeep Kanade

Int. J. Softw. Tools Technol. Transf., 2008

Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2008

On the Complexity of Consistency and Complete State Coding for Signal Transition Graphs.

[BibT_eX]

[DOI]

Petr Jancar

Alexander Miller

Fundam. Informaticae, 2008

SDSIrep: A Reputation System Based on SDSI.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Convergence Thresholds of Newton's Method for Monotone Polynomial Equations.

[BibT_eX]

[DOI]

Proceedings of the STACS 2008, 2008

Symbolic Context-Bounded Analysis of Multithreaded Java Programs.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2008

Solving Monotone Polynomial Equations.

[BibT_eX]

[DOI]

Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

Newton's Method for omega-Continuous Semirings.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

Approximative Methods for Monotone Systems of Min-Max-Polynomial Equations.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

2007

On the convergence of Newton's method for monotone systems of polynomial equations.

[BibT_eX]

[DOI]

Proceedings of the 39th Annual ACM Symposium on Theory of Computing, 2007

On Fixed Point Equations over Commutative Semirings.

[BibT_eX]

[DOI]

Proceedings of the STACS 2007, 2007

An Extension of Newton's Method to omega -Continuous Semirings.

[BibT_eX]

[DOI]

Proceedings of the Developments in Language Theory, 11th International Conference, 2007

jMoped: A Test Environment for Java Programs.

[BibT_eX]

[DOI]

Felix Berger

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Model Checking Probabilistic Pushdown Automata.

[BibT_eX]

[DOI]

Richard Mayr

Log. Methods Comput. Sci., 2006

Rewriting Models of Boolean Programs.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Separability in Conflict-Free Petri Nets.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of Systems Informatics, 2006

Reachability analysis of multithreaded software with asynchronous communication.

[BibT_eX]

[DOI]

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

Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2006

Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols.

[BibT_eX]

[DOI]

Giorgio Delzanno

Jirí Srba

Proceedings of the Automated Technology for Verification and Analysis, 2006

2005

jMoped: A Java Bytecode Checker Based on Moped.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

A Note on On-the-Fly Verification Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Locality-Based Abstractions.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 12th International Symposium, 2005

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances.

[BibT_eX]

[DOI]

Richard Mayr

Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion (Extended Abstract).

[BibT_eX]

[DOI]

Tomás Brázdil

Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), 2005

2004

A Polynomial-Time Algorithm for Checking Consistency of Free-Choice Signal Transition Graphs.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2004

Reachability Analysis of Synchronized PA Systems.

[BibT_eX]

[DOI]

Tayssir Touili

Proceedings of the 6th International Workshop on Verification of Infinite-State Systems, 2004

Verifying Probabilistic Procedural Programs.

[BibT_eX]

[DOI]

Kousha Etessami

Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

2003

A Logical Viewpoint on Process-algebraic Quotients.

[BibT_eX]

[DOI]

J. Log. Comput., 2003

A Generic Approach to the Static Analysis of Concurrent Programs with Procedures.

[BibT_eX]

[DOI]

Tayssir Touili

Int. J. Found. Comput. Sci., 2003

Model checking LTL with regular valuations for pushdown systems.

[BibT_eX]

[DOI]

Inf. Comput., 2003

Simple Representative Instantiations for Multicast Protocols.

[BibT_eX]

[DOI]

Monika Maidl

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

An Automata-Theoretic Approach to Software Verification.

[BibT_eX]

[DOI]

Proceedings of the Developments in Language Theory, 7th International Conference, 2003

Synthesis of Distributed Algorithms Using Asynchronous Automata.

[BibT_eX]

[DOI]

Alin Stefanescu

Anca Muscholl

Proceedings of the CONCUR 2003, 2003

The Model-Checking Kit.

[BibT_eX]

[DOI]

Claus Schröter

Proceedings of the Applications and Theory of Petri Nets 2003, 2003

2002

An Improvement of McMillan's Unfolding Algorithm.

[BibT_eX]

[DOI]

Stefan Römer

Walter Vogler

Formal Methods Syst. Des., 2002

An Algebraic Approach to the Static Analysis of Concurrent Software.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 9th International Symposium, 2002

Grammars as Processes.

[BibT_eX]

[DOI]

Proceedings of the Formal and Natural Computing, 2002

2001

Unfolding Based Algorithms for the Reachability Problem.

[BibT_eX]

[DOI]

Claus Schröter

Fundam. Informaticae, 2001

Implementing LTL Model Checking with Net Unfoldings.

[BibT_eX]

[DOI]

Keijo Heljanko

Proceedings of the Model Checking Software, 2001

Model Checking (with) Declarative Programs.

[BibT_eX]

[DOI]

Proceedings of the 3rd international ACM SIGPLAN conference on Principles and practice of declarative programming, 2001

Net Reductions for LTL Model-Checking.

[BibT_eX]

[DOI]

Claus Schröter

Proceedings of the Correct Hardware Design and Verification Methods, 2001

A BDD-Based Model Checker for Recursive Programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

More Infinite Results.

[BibT_eX]

Olaf Burkart

Proceedings of the Current Trends in Theoretical Computer Science, 2001

2000

An efficient automata approach to some problems on context-free grammars.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2000

Verification of Safety Properties Using Integer Programming: Beyond the State Equation.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2000

A Uniform Framework for Problems on Context-Free Grammars.

[BibT_eX]

Peter Rossmanith

Bull. EATCS, 2000

Efficient Algorithms for pre* and post* on Interprocedural Parallel Flow Graphs.

[BibT_eX]

[DOI]

Andreas Podelski

Proceedings of the POPL 2000, 2000

Verification of Systems with an Infinite State Space.

[BibT_eX]

[DOI]

Proceedings of the Modeling and Verification of Parallel Processes, 4th Summer School, 2000

Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL.

[BibT_eX]

[DOI]

Leonor Prensa Nieto

Proceedings of the Mathematical Foundations of Computer Science 2000, 2000

A New Unfolding Approach to LTL Model Checking.

[BibT_eX]

[DOI]

Keijo Heljanko

Proceedings of the Automata, Languages and Programming, 27th International Colloquium, 2000

Efficient Algorithms for Model Checking Pushdown Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999

Petri Nets and Regular Processes.

[BibT_eX]

[DOI]

Petr Jancar

Faron Moller

J. Comput. Syst. Sci., 1999

On the Verification of Broadcast Protocols.

[BibT_eX]

[DOI]

Alain Finkel

Richard Mayr

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis.

[BibT_eX]

[DOI]

Jens Knoop

Proceedings of the Foundations of Software Science and Computation Structure, 1999

Constraint-Based Analysis of Broadcast Protocols.

[BibT_eX]

[DOI]

Giorgio Delzanno

Andreas Podelski

Proceedings of the Computer Science Logic, 13th International Workshop, 1999

Proof-Checking Protocols Using Bisimulations.

[BibT_eX]

[DOI]

Christine Röckl

Proceedings of the CONCUR '99: Concurrency Theory, 1999

An Unfolding Algorithm for Synchronous Products of Transition Systems.

[BibT_eX]

[DOI]

Stefan Römer

Proceedings of the CONCUR '99: Concurrency Theory, 1999

1998

Reachability in Live and Safe Free-Choice Petri Nets is NP-Complete.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1998

1997

Petri Nets, Commutative Context-Free Grammars, and Basic Parallel Processes.

[BibT_eX]

[DOI]

Fundam. Informaticae, 1997

Decidability of Model Checking for Infinite-State Concurrent Systems.

[BibT_eX]

[DOI]

Acta Informatica, 1997

Reachability Analysis of Pushdown Automata: Application to Model-Checking.

[BibT_eX]

[DOI]

Oded Maler

Proceedings of the CONCUR '97: Concurrency Theory, 1997

An Automata Approach to Some Problems on Context-Free Grammars.

[BibT_eX]

[DOI]

Peter Rossmanith

Proceedings of the Foundations of Computer Science: Potential - Theory, 1997

Model Checking LTL Using Constraint Programming.

[BibT_eX]

[DOI]

Proceedings of the Application and Theory of Petri Nets 1997, 1997

1996

Trapping Mutual Exclusion in the Box Calculus.

[BibT_eX]

[DOI]

Glenn Bruns

Theor. Comput. Sci., 1996

More infinite results.

[BibT_eX]

[DOI]

Olaf Burkart

Proceedings of the First International Workshop on Verification of Infinite State Systems, 1996

Deciding Finiteness of Petri Nets Up To Bisimulation.

[BibT_eX]

[DOI]

Petr Jancar

Proceedings of the Automata, Languages and Programming, 23rd International Colloquium, 1996

An Effective Tableau System for the Linear Time µ-Calculus.

[BibT_eX]

[DOI]

Julian C. Bradfield

Angelika Mader

Proceedings of the Automata, Languages and Programming, 23rd International Colloquium, 1996

Checking System Properties via Integer Programming.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 1996

Verification Using PEP.

[BibT_eX]

[DOI]

Stefan Römer

Proceedings of the Algebraic Methodology and Software Technology, 1996

Decidability and Complexity of Petri Net Problems - An Introduction.

[BibT_eX]

[DOI]

Proceedings of the Lectures on Petri Nets I: Basic Models, 1996

1995

Complexity Results for 1-Safe Nets.

[BibT_eX]

[DOI]

Allan Cheng

Jens Palsberg

Theor. Comput. Sci., 1995

Shortest Paths in Reachability Graphs.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1995

On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes.

[BibT_eX]

[DOI]

Astrid Kiehn

Proceedings of the Computer Aided Verification, 1995

1994

Reduction and Synthesis of Live and Bounded Free Choice Petri Nets

[BibT_eX]

[DOI]

Inf. Comput., October, 1994

Model Checking Using Net Unfoldings.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1994

Decidability Issues for Petri Nets - a survey.

[BibT_eX]

Mogens Nielsen

J. Inf. Process. Cybern., 1994

Operational Semantics for the Petri Box Calculus.

[BibT_eX]

[DOI]

Maciej Koutny

Proceedings of the CONCUR '94, 1994

On the Decidability of Model Checking for Several µ-calculi and Petri Nets.

[BibT_eX]

[DOI]

Proceedings of the Trees in Algebra and Programming, 1994

1993

Reachability in Cyclic Extended Free-Choice Systems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1993

The Asynchronous Committee Meeting Problem.

[BibT_eX]

[DOI]

Bernhard von Stengel

Proceedings of the Graph-Theoretic Concepts in Computer Science, 1993

General Refinement and Recursion Operators for the Petri Box Calculus.

[BibT_eX]

[DOI]

Raymond R. Devillers

Proceedings of the STACS 93, 1993

1992

A Polynomial-Time Algorithm to Decide Liveness of Bounded Free Choice Nets.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1992

Traps Characterize Home States in Free Choice Systems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1992

A Solution to the Covering Problem for 1-Bounded Conflict-Free Petri Nets Using Linear Programming.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1992

1991

Model Checking of Persistent Petri Nets.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 5th Workshop, 1991

Compositional Synthesis of Live and Bounded Free Choice Petri Nets.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '91, 1991

1990

Reachability in reversible free-choice systems

[BibT_eX]

[DOI]

Forschungsberichte, TU Munich, 1990

Synthesis Rules for Petri Nets, and How they Lead to New Results.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '90, 1990

Top-down synthesis of live and bounded free choice nets.

[BibT_eX]

[DOI]

Proceedings of the Advances in Petri Nets 1991, 1990

1989

On the analysis and synthesis of free choice systems.

[BibT_eX]

[DOI]

Proceedings of the Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, 1989

Circuits, handles, bridges and nets.

[BibT_eX]

[DOI]