2023
Learning a Neuron by a Shallow ReLU Network: Dynamics and Implicit Bias for Correlated Inputs.
Proceedings of the Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, 2023
2022
Adversarial Reprogramming Revisited.
Proceedings of the Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, 2022
2021
When are emptiness and containment decidable for probabilistic automata?
J. Comput. Syst. Sci., 2021
The Reachability Problem for Petri Nets Is Not Elementary.
J. ACM, 2021
The Reachability Problem for Two-Dimensional Vector Addition Systems with States.
J. ACM, 2021
A lower bound for the coverability problem in acyclic pushdown VAS.
Inf. Process. Lett., 2021
The ideal view on Rackoff's coverability technique.
Inf. Comput., 2021
Verifying higher-order concurrency with data automata.
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021
Leafy automata for higher-order concurrency.
Proceedings of the Foundations of Software Science and Computation Structures, 2021
2020
KReach: A Tool for Reachability in Petri Nets.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020
Reachability in Fixed Dimension Vector Addition Systems with States.
Proceedings of the 31st International Conference on Concurrency Theory, 2020
2019
Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems.
ACM Trans. Comput. Log., 2019
Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games.
Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms, 2019
Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk).
Proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2019
2018
The Reachability Problem for Petri Nets is Not Elementary (Extended Abstract).
CoRR, 2018
A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games.
CoRR, 2018
A pseudo-quasi-polynomial algorithm for mean-payoff parity games.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018
When is Containment Decidable for Probabilistic Automata?.
Proceedings of the 45th International Colloquium on Automata, Languages, and Programming, 2018
2017
Succinct progress measures for solving parity games.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017
Perfect half space games.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017
Timed pushdown automata and branching vector addition systems.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017
Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One.
Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017
What Makes Petri Nets Harder to Verify: Stack or Data?
Proceedings of the Concurrency, Security, and Puzzles, 2017
2016
Zeno, Hercules, and the Hydra: Safety Metric Temporal Logic is Ackermann-Complete.
ACM Trans. Comput. Log., 2016
The Complexity of Coverability in ν-Petri Nets.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016
Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016
A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One.
Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016
Contextual Approximation and Higher-Order Procedures.
Proceedings of the Foundations of Software Science and Computation Structures, 2016
Coverability Trees for Petri Nets with Unordered Data.
Proceedings of the Foundations of Software Science and Computation Structures, 2016
2015
Nonelementary Complexities for Branching VASS, MELL, and Extensions.
ACM Trans. Comput. Log., 2015
Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time.
Proceedings of the Automata, Languages, and Programming - 42nd International Colloquium, 2015
2014
Non-elementary complexities for branching VASS, MELL, and extensions.
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
2013
The covering and boundedness problems for branching vector addition systems.
J. Comput. Syst. Sci., 2013
The reachability problem for vector addition systems with a stack is not elementary.
CoRR, 2013
Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian.
Proceedings of the Mathematical Foundations of Computer Science 2013, 2013
2011
Safety alternating automata on data words.
ACM Trans. Comput. Log., 2011
Alternating automata on data trees and XPath satisfiability.
ACM Trans. Comput. Log., 2011
Average-price-per-reward games on hybrid automata with strong resets.
Int. J. Softw. Tools Technol. Transf., 2011
2010
Model checking memoryful linear-time logics over one-counter automata.
Theor. Comput. Sci., 2010
Data-abstraction refinement: a game semantic approach.
Int. J. Softw. Tools Technol. Transf., 2010
The reachability problem for branching vector addition systems requires doubly-exponential space.
Inf. Process. Lett., 2010
2009
LTL with the freeze quantifier and register automata.
ACM Trans. Comput. Log., 2009
2008
Nets with Tokens which Carry Data.
Fundam. Informaticae, 2008
Model Checking Freeze LTL over One-Counter Automata.
Proceedings of the Foundations of Software Science and Computational Structures, 2008
Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2008
2007
Compositional software verification based on game semantics and process algebra.
Int. J. Softw. Tools Technol. Transf., 2007
On the freeze quantifier in Constraint LTL: Decidability and complexity.
Inf. Comput., 2007
Formal Aspects Comput., 2007
Alternation-free modal mu-calculus for data trees.
Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
2006
A Counterexample-Guided Refinement Tool for Open Procedural Programs.
Proceedings of the Model Checking Software, 13th International SPIN Workshop, Vienna, Austria, March 30, 2006
Assume-Guarantee Software Verification Based on Game Semantics.
Proceedings of the Formal Methods and Software Engineering, 2006
Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 2006
2005
Proceedings of the 5th International Workshop on Automated Verification of Critical Systems, 2005
Data-Abstraction Refinement: A Game Semantic Approach.
Proceedings of the Static Analysis, 12th International Symposium, 2005
Abstraction-refinement for game-based model checking.
Proceedings of the 1st Workshop on Games for Logic and Programming Languages, 2005
2004
On model checking data-independent systems with arrays without reset.
Theory Pract. Log. Program., 2004
Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting.
Proceedings of the 6th International Workshop on Verification of Infinite-State Systems, 2004
Decidability of Reachability for Polymorphic Systems with Arrays: A Complete Classification.
Proceedings of the 6th International Workshop on Verification of Infinite-State Systems, 2004
Software Model Checking Based on Game Semantics and CSP.
Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems, 2004
Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption.
Proceedings of the Integrated Formal Methods, 4th International Conference, 2004
CSP Representation of Game Semantics for Second-Order Idealized Algol.
Proceedings of the Formal Methods and Software Engineering, 2004
On Model Checking Data-Independent Systems with Arrays with Whole-Array Operations.
Proceedings of the Communicating Sequential Processes: The First 25 Years, 2004
2003
On a Semantic Definition of Data Independence .
Proceedings of the Typed Lambda Calculi and Applications, 6th International Conference, 2003
2000
A Unifying Approach to Data-Independence.
Proceedings of the CONCUR 2000, 2000
1999
A semantic study of data independence with applications to model checking.
PhD thesis, 1999
Data Independence with Generalised Predicate Symbols.
Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999