Papers archive | Algorithms, Theory & Logic

Markov Decision Processes with Time-Varying Geometric Discounting.

Jiarui Gan, Annika Hennes, Rupak Majumdar, Debmalya Mandal, Goran Radanovic.
AAAI 2023.

A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.

Rupak Majumdar, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, Sadegh Soudjani.
CAV 2023.

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

Eszter Couillard, Philipp Czerner, Javier Esparza, Rupak Majumdar.
CAV 2023.

Solving String Constraints Using SAT.

Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Rupak Majumdar, Dirk Nowotka.
CAV 2023.

Synthesizing Permissive Winning Strategy Templates for Parity Games.

Ashwani Anand, Satya Prakash Nayak, Anne-Kathrin Schmuck.
CAV 2023.

Unboundedness Problems for Machines with Reversal-Bounded Counters.

Pascal Baumann, Flavio D'Alessandro, Moses Ganardi, Oscar H. Ibarra, Ian McQuillan, Lia Schütze, Georg Zetzsche.
FoSSaCS 2023.

Lazy Synthesis of Symbolic Output-Feedback Controllers for State-Based Safety Specifications.

Mehrdad Zareian, Anne-Kathrin Schmuck.
HSCC 2023.

Poster Abstract: A Toolchain for Accelerated Symbolic Control.

Rupak Majumdar, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, Sadegh Soudjani.
HSCC 2023.

Poster Abstract: Permissiveness for Strategy Adaptation.

Ashwani Anand, Satya Prakash Nayak, Anne-Kathrin Schmuck.
HSCC 2023.

Poster Abstract: Towards Seamless Reactivity of Hybrid Control.

Lucas Neves Egidio, Satya Prakash Nayak, Matteo Della Rossa, Anne-Kathrin Schmuck, Raphaël M. Jungers.
HSCC 2023.

Checking Refinement of Asynchronous Programs Against Context-Free Specifications.

Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
ICALP 2023.

Context-Bounded Analysis of Concurrent Programs (Invited Talk).

Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
ICALP 2023.

Positivity Problems for Reversible Linear Recurrence Sequences.

George Kenison, Joris Nieuwveld, Joël Ouaknine, James Worrell.
ICALP 2023.

Supervisory Controller Synthesis for Nonterminating Processes Is an Obliging Game.

Rupak Majumdar, Anne-Kathrin Schmuck.
IEEE Trans. Autom. Control. 2023.

Knapsack and the power word problem in solvable Baumslag-Solitar groups.

Moses Ganardi, Markus Lohrey, Georg Zetzsche.
Int. J. Algebra Comput. 2023.

Reachability in Injective Piecewise Affine Maps.

Faraz Ghahremani, Edon Kelmendi, Joël Ouaknine.
LICS 2023.

Simulating Logspace-Recursion with Logarithmic Quantifier Depth.

Steffen van Bergerem, Martin Grohe, Sandra Kiefer, Luca Oeljeklaus.
LICS 2023.

The Power of Positivity.

Toghrul Karimov, Edon Kelmendi, Joris Nieuwveld, Joël Ouaknine, James Worrell.
LICS 2023.

Context-Bounded Verification of Context-Free Specifications.

Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
POPL 2023.

Regular Separability in Büchi VASS.

Pascal Baumann, Roland Meyer, Georg Zetzsche.
STACS 2023.

Computing Adequately Permissive Assumptions for Synthesis.

Ashwani Anand, Kaushik Mallik, Satya Prakash Nayak, Anne-Kathrin Schmuck.
TACAS 2023.

Model Checking Linear Dynamical Systems under Floating-point Rounding.

Engel Lefaucheux, Joël Ouaknine, David Purser, Mohammadamin Sharifi.
TACAS 2023.

Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness.

Tamajit Banerjee, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani.
TheoretiCS 2023.

Report on women in logic 2020 & 2021.

Sandra Alves, Sandra Kiefer, Ana Sokolova.
ACM SIGLOG News 2022.

Graphs Identified by Logics with Counting.

Sandra Kiefer, Pascal Schweitzer, Erkal Selman.
ACM Trans. Comput. Log. 2022.

O-Minimal Invariants for Discrete-Time Dynamical Systems.

Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, James Worrell.
ACM Trans. Comput. Log. 2022.

Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications.

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Markus A. Whiteland, James Worrell.
CONCUR 2022.

Algebraic Model Checking for Discrete Linear Dynamical Systems.

Florian Luca, Joël Ouaknine, James Worrell.
FORMATS 2022.

BOCoSy: Small but Powerful Symbolic Output-Feedback Control.

Bernd Finkbeiner, Kaushik Mallik, Noemi Passing, Malte Schledjewski, Anne-Kathrin Schmuck.
HSCC 2022.

A Study of Weisfeiler-Leman Colorings on Planar Graphs.

Sandra Kiefer, Daniel Neuen.
ICALP 2022.

Reachability in Bidirected Pushdown VASS.

Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, Georg Zetzsche.
ICALP 2022.

SpeqNets: Sparsity-aware permutation-equivariant graph networks.

Christopher Morris, Gaurav Rattan, Sandra Kiefer, Siamak Ravanbakhsh.
ICML 2022.

On the Skolem Problem and the Skolem Conjecture.

Richard Lipton, Florian Luca, Joris Nieuwveld, Joël Ouaknine, David Purser, James Worrell.
LICS 2022.

Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification.

Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, Georg Zetzsche.
LICS 2022.

The Complexity of Bidirected Reachability in Valence Systems.

Moses Ganardi, Rupak Majumdar, Georg Zetzsche.
LICS 2022.

Treelike Decompositions for Transductions of Sparse Graphs.

Jan Dreier, Jakub Gajarský, Sandra Kiefer, Michal Pilipczuk, Szymon Torunczyk.
LICS 2022.

General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond.

Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
Log. Methods Comput. Sci. 2022.

Sequential Relational Decomposition.

Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi.
Log. Methods Comput. Sci. 2022.

A Universal Skolem Set of Positive Lower Density.

Florian Luca, Joël Ouaknine, James Worrell.
MFCS 2022.

Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set.

Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, James Worrell.
MFCS 2022.

Membership Problems in Finite Groups.

Markus Lohrey, Andreas Rosowski, Georg Zetzsche.
MFCS 2022.

Skolem Meets Schanuel.

Yuri Bilu, Florian Luca, Joris Nieuwveld, Joël Ouaknine, David Purser, James Worrell.
MFCS 2022.

The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems.

Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, James Worrell.
MFCS 2022.

Context-bounded verification of thread pools.

Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
POPL 2022.

Subcubic certificates for CFL reachability.

Dmitry Chistikov, Rupak Majumdar, Philipp Schepper.
POPL 2022.

What's decidable about linear loops?

Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, James Worrell.
POPL 2022.

What's Decidable About Discrete Linear Dynamical Systems?

Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, James Worrell.
Principles of Systems Design 2022.

The Power of the Weisfeiler-Leman Algorithm to Decompose Graphs.

Sandra Kiefer, Daniel Neuen.
SIAM J. Discret. Math. 2022.

Existential Definability over the Subword Ordering.

Pascal Baumann, Moses Ganardi, Ramanathan S. Thinniyam, Georg Zetzsche.
STACS 2022.

A Direct Symbolic Algorithm for Solving Stochastic Rabin Games.

Tamajit Banerjee, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani.
TACAS 2022.

Choosing the Initial State for Online Replanning.

Maximilian Fickert, Ivan Gavran, Ivan Fedotov, Jörg Hoffmann, Rupak Majumdar, Wheeler Ruml.
AAAI 2021.

Responsibility Attribution in Parameterized Markovian Models.

Christel Baier, Florian Funke, Rupak Majumdar.
AAAI 2021.

Symbolic Qualitative Control for Stochastic Systems via Finite Parity Games.

Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani.
ADHS 2021.

Porous Invariants.

Engel Lefaucheux, Joël Ouaknine, David Purser, James Worrell.
CAV 2021.

Generalising Projection in Asynchronous Multiparty Session Types.

Rupak Majumdar, Madhavan Mukund, Felix Stutz, Damien Zufferey.
CONCUR 2021.

Scope-Bounded Reachability in Valence Systems.

Aneesh K. Shetty, Shankara Narayanan Krishna, Georg Zetzsche.
CONCUR 2021.

The Orbit Problem for Parametric Linear Dynamical Systems.

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland, James Worrell.
CONCUR 2021.

Paracosm: A Test Framework for Autonomous Driving Simulations.

Rupak Majumdar, Aman Shankar Mathur, Marcus Pirron, Laura Stegner, Damien Zufferey.
FASE 2021.

The computability of LQR and LQG control.

Rupak Majumdar, Sadegh Soudjani.
HSCC 2021.

Decision Problems for Second-Order Holonomic Recurrences.

Eike Neumann, Joël Ouaknine, James Worrell.
ICALP 2021.

From Verification to Causality-Based Explications (Invited Talk).

Christel Baier, Clemens Dubslaff, Florian Funke, Simon Jantsch, Rupak Majumdar, Jakob Piribauer, Robin Ziemek.
ICALP 2021.

Logarithmic Weisfeiler-Leman Identifies All Planar Graphs.

Martin Grohe, Sandra Kiefer.
ICALP 2021.

Symbolic reach-avoid control of multi-agent systems.

Rupak Majumdar, Kaushik Mallik, Mahmoud Salamati, Sadegh Soudjani, Mehrdad Zareian.
ICCPS 2021.

Verifying Asymptotic Temporal Properties of Continuous-State Probabilistic Systems.

Natsuki Urabe, Rupak Majumdar.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2021.

A Game-Theoretic Account of Responsibility Allocation.

Christel Baier, Florian Funke, Rupak Majumdar.
IJCAI 2021.

Preface.

Mikolaj Bojanczyk, Thomas Brihaye, Christoph Haase, Slawomir Lasota, Joël Ouaknine, Igor Potapov.
Inf. Comput. 2021.

The emptiness problem for valence automata over graph monoids.

Georg Zetzsche.
Inf. Comput. 2021.

Universal Skolem Sets.

Florian Luca, Joël Ouaknine, James Worrell.
LICS 2021.

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility.

Anthony W. Lin, Rupak Majumdar.
Log. Methods Comput. Sci. 2021.

Holonomic Techniques, Periods, and Decision Problems (Invited Talk).

Joël Ouaknine.
MFCS 2021.

On Positivity and Minimality for Second-Order Holonomic Sequences.

George Kenison, Oleksiy Klurman, Engel Lefaucheux, Florian Luca, Pieter Moree, Joël Ouaknine, Markus A. Whiteland, James Worrell.
MFCS 2021.

On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets.

Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, James Worrell.
MFCS 2021.

The Pseudo-Skolem Problem is Decidable.

Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, Sadegh Soudjani, James Worrell.
MFCS 2021.

Context-bounded verification of liveness properties for multithreaded shared-memory programs.

Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
POPL 2021.

Deciding ω-regular properties on linear recurrence sequences.

Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, James Worrell.
POPL 2021.

Recent Advances on Reachability Problems for Valence Systems (Invited Talk).

Georg Zetzsche.
RP 2021.

A Characterization of Wreath Products Where Knapsack Is Decidable.

Pascal Bergsträßer, Moses Ganardi, Georg Zetzsche.
STACS 2021.

General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond.

Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
TACAS 2021.

First-Order Orbit Queries.

Shaull Almagor, Joël Ouaknine, James Worrell.
Theory Comput. Syst. 2021.

The Weisfeiler-Leman algorithm: an exploration of its power.

Sandra Kiefer.
ACM SIGLOG News 2020.

A Lyapunov Approach for Time-Bounded Reachability of CTMCs and CTMDPs.

Mahmoud Salamati, Sadegh Soudjani, Rupak Majumdar.
ACM Trans. Model. Perform. Evaluation Comput. Syst. 2020.

Resilient Abstraction-Based Controller Design.

Stanly Samuel, Kaushik Mallik, Anne-Kathrin Schmuck, Daniel Neider.
CDC 2020.

Algebraic Invariants for Linear Hybrid Automata.

Rupak Majumdar, Joël Ouaknine, Amaury Pouly, James Worrell.
CONCUR 2020.

On Ranking Function Synthesis and Termination for Polynomial Programs.

Eike Neumann, Joël Ouaknine, James Worrell.
CONCUR 2020.

On the relation between reactive synthesis and supervisory control of non-terminating processes.

Anne-Kathrin Schmuck, Thomas Moor, Rupak Majumdar.
Discret. Event Dyn. Syst. 2020.

Holonomic Techniques, Periods, and Decision Problems (Invited Talk).

Joël Ouaknine.
FSTTCS 2020.

Reachability in Dynamical Systems with Rounding.

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, Markus A. Whiteland.
FSTTCS 2020.

On abstraction-based controller design with output feedback.

Rupak Majumdar, Necmiye Ozay, Anne-Kathrin Schmuck.
HSCC 2020.

Resilient abstraction-based controller design.

Stanly Samuel, Kaushik Mallik, Anne-Kathrin Schmuck, Daniel Neider.
HSCC 2020.

Symbolic controller synthesis for Büchi specifications on stochastic systems.

Rupak Majumdar, Kaushik Mallik, Sadegh Soudjani.
HSCC 2020.

Invariants for Continuous Linear Dynamical Systems.

Shaull Almagor, Edon Kelmendi, Joël Ouaknine, James Worrell.
ICALP 2020.

On Decidability of Time-Bounded Reachability in CTMDPs.

Rupak Majumdar, Mahmoud Salamati, Sadegh Soudjani.
ICALP 2020.

Rational Subsets of Baumslag-Solitar Groups.

Michaël Cadilhac, Dmitry Chistikov, Georg Zetzsche.
ICALP 2020.

The Complexity of Bounded Context Switching with Dynamic Thread Creation.

Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
ICALP 2020.

The Complexity of Knapsack Problems in Wreath Products.

Michael Figelius, Moses Ganardi, Markus Lohrey, Georg Zetzsche.
ICALP 2020.

The Iteration Number of Colour Refinement.

Sandra Kiefer, Brendan D. McKay.
ICALP 2020.

DeepEquaL: Deep Learning Based Mathematical Equation to Latex Generation.

Ghaith Bilbeisi, Sheraz Ahmed, Rupak Majumdar.
ICONIP 2020.

Assume-Guarantee Distributed Synthesis.

Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Damien Zufferey.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2020.

On the skolem problem and prime powers.

George Kenison, Richard Lipton, Joël Ouaknine, James Worrell.
ISSAC 2020.

An Approach to Regular Separability in Vector Addition Systems.

Wojciech Czerwinski, Georg Zetzsche.
LICS 2020.

Extensions of ω-Regular Languages.

Mikolaj Bojanczyk, Edon Kelmendi, Rafal Stefanski, Georg Zetzsche.
LICS 2020.

Knapsack and the Power Word Problem in Solvable Baumslag-Solitar Groups.

Markus Lohrey, Georg Zetzsche.
MFCS 2020.

On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems.

Toghrul Karimov, Joël Ouaknine, James Worrell.
MFCS 2020.

Multiparty motion coordination: from choreographies to robotics programs.

Rupak Majumdar, Nobuko Yoshida, Damien Zufferey.
OOPSLA 2020.

Testing consensus implementations using communication closure.

Cezara Dragoi, Constantin Enea, Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic.
OOPSLA 2020.

How Fast Can You Escape a Compact Polytope?

Julian D'Costa, Engel Lefaucheux, Joël Ouaknine, James Worrell.
STACS 2020.

Lazy Abstraction-Based Controller Synthesis.

Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck.
ATVA 2019.

Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols).

Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer.
CAV 2019.

Incremental Abstraction Computation for Symbolic Controller Synthesis in a Changing Environment.

Yunjun Bai, Kaushik Mallik, Anne-Kathrin Schmuck, Damien Zufferey, Rupak Majumdar.
CDC 2019.

Motion Session Types for Robotic Interactions (Brave New Idea Paper).

Rupak Majumdar, Marcus Pirron, Nobuko Yoshida, Damien Zufferey.
ECOOP 2019.

The Geometry of Rank Decompositions of Matrix Multiplication I: 2 × 2 Matrices.

Luca Chiantini, Christian Ikenmeyer, J. M. Landsberg, Giorgio Ottaviani.
Experimental Mathematics 2019.

Languages Ordered by the Subword Order.

Dietrich Kuske, Georg Zetzsche.
FoSSaCS 2019.

Regular Separability and Intersection Emptiness Are Independent Problems.

Ramanathan S. Thinniyam, Georg Zetzsche.
FSTTCS 2019.

On the decidability of reachability in linear time-invariant systems.

Nathanaël Fijalkow, Joël Ouaknine, Amaury Pouly, João Sousa Pinto, James Worrell.
HSCC 2019.

A Linear Upper Bound on the Weisfeiler-Leman Dimension of Graphs of Bounded Genus.

Martin Grohe, Sandra Kiefer.
ICALP 2019.

On Geometric Complexity Theory: Multiplicity Obstructions Are Stronger Than Occurrence Obstructions.

Julian Dörfler, Christian Ikenmeyer, Greta Panova.
ICALP 2019.

On Reachability Problems for Low-Dimensional Matrix Semigroups.

Thomas Colcombet, Joël Ouaknine, Pavel Semukhin, James Worrell.
ICALP 2019.

String-to-String Interpretations With Polynomial-Size Output.

Mikolaj Bojanczyk, Sandra Kiefer, Nathan Lhote.
ICALP 2019.

Termination of Linear Loops over the Integers.

Mehran Hosseini, Joël Ouaknine, James Worrell.
ICALP 2019.

PGCD: robot programming and verification with geometry, concurrency, and dynamics.

Gregor B. Banusic, Rupak Majumdar, Marcus Pirron, Anne-Kathrin Schmuck, Damien Zufferey.
ICCPS 2019.

Programming event processors with thingflow.

Jeffrey M. Fischer, Rupak Majumdar.
ICCPS 2019.

Compositional Synthesis of Finite-State Abstractions.

Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani, Rupak Majumdar.
IEEE Trans. Autom. Control. 2019.

Shrinking Horizon Model Predictive Control With Signal Temporal Logic Constraints Under Stochastic Disturbances.

Samira S. Farahani, Rupak Majumdar, Vinayak S. Prabhu, Sadegh Soudjani.
IEEE Trans. Autom. Control. 2019.

On the Decidability of Membership in Matrix-exponential Semigroups.

Joël Ouaknine, Amaury Pouly, João Sousa Pinto, James Worrell.
J. ACM 2019.

The Weisfeiler-Leman Dimension of Planar Graphs Is at Most 3.

Sandra Kiefer, Ilia Ponomarenko, Pascal Schweitzer.
J. ACM 2019.

Cyclic-routing of Unmanned Aerial Vehicles.

Nir Drucker, Hsi-Ming Ho, Joël Ouaknine, Michal Penn, Ofer Strichman.
J. Comput. Syst. Sci. 2019.

Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests.

Christoph Haase, Georg Zetzsche.
LICS 2019.

On the Expressiveness and Monitoring of Metric Temporal Logic.

Hsi-Ming Ho, Joël Ouaknine, James Worrell.
Log. Methods Comput. Sci. 2019.

Upper Bounds on the Quantifier Depth for Graph Differentiation in First-Order Logic.

Sandra Kiefer, Pascal Schweitzer.
Log. Methods Comput. Sci. 2019.

The Power of the Weisfeiler-Leman Algorithm to Decompose Graphs.

Sandra Kiefer, Daniel Neuen.
MFCS 2019.

Trace aware random testing for distributed systems.

Burcu Kulahcioglu Ozkan, Rupak Majumdar, Simin Oraee.
OOPSLA 2019.

Checking linearizability using hitting families.

Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic.
PPoPP 2019.

Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets.

Sylvain Schmitz, Georg Zetzsche.
RP 2019.

On the Monniaux Problem in Abstract Interpretation.

Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell.
SAS 2019.

The Semialgebraic Orbit Problem.

Shaull Almagor, Joël Ouaknine, James Worrell.
STACS 2019.

Environmentally-Friendly GR(1) Synthesis.

Rupak Majumdar, Nir Piterman, Anne-Kathrin Schmuck.
TACAS 2019.

Complete Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem.

Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell.
Theory Comput. Syst. 2019.

Environmentally-friendly GR(1) Synthesis

Rupak Majumdar, Nir Piterman, Anne-Kathrin Schmuck.
Technical Report MPI-SWS-2018-008 2018.

Reachability analysis of reversal-bounded automata on series-parallel graphs.

Rayna Dimitrova, Rupak Majumdar.
Acta Informatica 2018.

Concentration of Measure for Chance-Constrained Optimization.

Sadegh Soudjani, Rupak Majumdar.
ADHS 2018.

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility.

Anthony W. Lin, Rupak Majumdar.
ATVA 2018.

Lazy Abstraction-Based Control for Safety Specifications.

Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck.
CDC 2018.

DebugAR: Mixed Dimensional Displays for Immersive Debugging of Distributed Systems.

Patrick Reipschläger, Burcu Kulahcioglu Ozkan, Aman Shankar Mathur, Stefan Gumhold, Rupak Majumdar, Raimund Dachselt.
CHI Extended Abstracts 2018.

Bounded Context Switching for Valence Systems.

Roland Meyer, Sebastian Muskalla, Georg Zetzsche.
CONCUR 2018.

Effective Divergence Analysis for Linear Recurrence Sequences.

Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, James Worrell.
CONCUR 2018.

Verification of Immediate Observation Population Protocols.

Javier Esparza, Pierre Ganty, Rupak Majumdar, Chana Weil-Kennedy.
CONCUR 2018.

Causality Analysis for Concurrent Reactive Systems (Extended Abstract).

Rayna Dimitrova, Rupak Majumdar, Vinayak S. Prabhu.
CREST@ETAPS 2018.

Embedded software for robotics: challenges and future directions: special session.

Houssam Abbas, Indranil Saha, Yasser Shoukry, Rüdiger Ehlers, Georgios Fainekos, Rajesh Gupta, Rupak Majumdar, Dogan Ulus.
EMSOFT 2018.

iDeA: an immersive debugger for actors.

Aman Shankar Mathur, Burcu Kulahcioglu Ozkan, Rupak Majumdar.
Erlang Workshop 2018.

Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper).

Rupak Majumdar.
FSTTCS 2018.

Model Checking Real-Time Systems.

Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Joël Ouaknine, James Worrell.
Handbook of Model Checking 2018.

Symbolic Model Checking in Non-Boolean Domains.

Rupak Majumdar, Jean-François Raskin.
Handbook of Model Checking 2018.

Multi-Layered Abstraction-Based Controller Synthesis for Continuous-Time Systems.

Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck.
HSCC 2018.

O-Minimal Invariants for Linear Loops.

Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, James Worrell.
ICALP 2018.

Unboundedness Problems for Languages of Vector Addition Systems.

Wojciech Czerwinski, Piotr Hofman, Georg Zetzsche.
ICALP 2018.

Parameter optimization in control software using statistical fault localization techniques.

Jyotirmoy V. Deshmukh, Xiaoqing Jin, Rupak Majumdar, Vinayak S. Prabhu.
ICCPS 2018.

Convex Language Semantics for Nondeterministic Probabilistic Automata.

Gerco van Heerdt, Justin Hsu, Joël Ouaknine, Alexandra Silva.
ICTAC 2018.

Polynomial Invariants for Affine Programs.

Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, James Worrell.
LICS 2018.

Separability by piecewise testable languages and downward closures beyond subwords.

Georg Zetzsche.
LICS 2018.

Sequential Relational Decomposition.

Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi.
LICS 2018.

Model Checking Flat Freeze LTL on One-Counter Automata.

Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell.
Log. Methods Comput. Sci. 2018.

Randomized testing of distributed systems with probabilistic guarantees.

Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, Georg Weissenbacher.
OOPSLA 2018.

Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach.

Mahmoud Salamati, Sadegh Soudjani, Rupak Majumdar.
QEST 2018.

Knapsack Problems for Wreath Products.

Moses Ganardi, Daniel König, Markus Lohrey, Georg Zetzsche.
STACS 2018.

On the complexity of hazard-free circuits.

Christian Ikenmeyer, Balagopal Komarath, Christoph Lenzen, Vladimir Lysikov, Andrey Mokhov, Karteek Sreenivasaiah.
STOC 2018.

Knapsack in Graph Groups.

Markus Lohrey, Georg Zetzsche.
Theory Comput. Syst. 2018.

Antlab: A Multi-Robot Task Server.

Ivan Gavran, Rupak Majumdar, Indranil Saha.
ACM Trans. Embed. Comput. Syst. 2017.

Testing Cyber-Physical Systems through Bayesian Optimization.

Jyotirmoy V. Deshmukh, Marko Horvat, Xiaoqing Jin, Rupak Majumdar, Vinayak S. Prabhu.
ACM Trans. Embed. Comput. Syst. 2017.

Approximate counting in SMT and value estimation for probabilistic programs.

Dmitry Chistikov, Rayna Dimitrova, Rupak Majumdar.
Acta Informatica 2017.

Dynamic Bayesian networks for formal verification of structured stochastic processes.

Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, Rupak Majumdar.
Acta Informatica 2017.

Verification of population protocols.

Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
Acta Informatica 2017.

Compositional abstractions of interconnected discrete-time stochastic control systems.

Abolfazl Lavaei, Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, Majid Zamani.
CDC 2017.

Compositional construction of finite state abstractions for stochastic control systems.

Kaushik Mallik, Sadegh Esmaeil Zadeh Soudjani, Anne-Kathrin Schmuck, Rupak Majumdar.
CDC 2017.

Dynamic hierarchical reactive controller synthesis.

Anne-Kathrin Schmuck, Rupak Majumdar, Adrian Leva.
Discret. Event Dyn. Syst. 2017.

A Characterization for Decidable Separability by Piecewise Testable Languages.

Wojciech Czerwinski, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, Georg Zetzsche.
Discret. Math. Theor. Comput. Sci. 2017.

Synthesis of Solutions for Shaded Area Geometry Problems.

Chris Alvin, Sumit Gulwani, Rupak Majumdar, Supratik Mukhopadhyay.
FLAIRS 2017.

Model checking parameterized asynchronous shared-memory systems.

Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar.
Formal Methods Syst. Des. 2017.

Quantifying conformance using the Skorokhod metric.

Jyotirmoy V. Deshmukh, Rupak Majumdar, Vinayak S. Prabhu.
Formal Methods Syst. Des. 2017.

On the Polytope Escape Problem for Continuous Linear Dynamical Systems.

Joël Ouaknine, João Sousa Pinto, James Worrell.
HSCC 2017.

The Polytope-Collision Problem.

Shaull Almagor, Joël Ouaknine, James Worrell.
ICALP 2017.

On parametric timed automata and one-counter machines.

Daniel Bundala, Joël Ouaknine.
Inf. Comput. 2017.

Decidability, complexity, and expressiveness of first-order logic over the subword ordering.

Simon Halfon, Philippe Schnoebelen, Georg Zetzsche.
LICS 2017.

The Weisfeiler-Leman dimension of planar graphs is at most 3.

Sandra Kiefer, Ilia Ponomarenko, Pascal Schweitzer.
LICS 2017.

Timed Temporal Logics.

Patricia Bouyer, François Laroussinie, Nicolas Markey, Joël Ouaknine, James Worrell.
Models, Algorithms, Logics and Tools 2017.

Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem.

Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell.
STACS 2017.

The Complexity of Knapsack in Graph Groups.

Markus Lohrey, Georg Zetzsche.
STACS 2017.

On Boolean Closed Full Trios and Rational Kripke Frames.

Georg Zetzsche, Dietrich Kuske, Markus Lohrey.
Theory Comput. Syst. 2017.

Computing Distances between Reach Flowpipes.

Rupak Majumdar, Vinayak S. Prabhu.
HSCC 2016.

Hitting Families of Schedules for Asynchronous Programs.

Dmitry Chistikov, Rupak Majumdar, Filip Niksic.
CAV 2016.

Algorithms and Tools for Verification and Testing of Asynchronous Programs

Zilong Wang.
Technical Report MPI-SWS-2016-001 2016.

Zeno, Hercules, and the Hydra: Safety Metric Temporal Logic is Ackermann-Complete.

Ranko Lazic, Joël Ouaknine, James Worrell.
ACM Trans. Comput. Log. 2016.

Knapsack and subset sum problems in nilpotent, polycyclic, and co-context-free groups.

Daniel König, Markus Lohrey, Georg Zetzsche.
AMS-EMS-SPM Joint Meeting 2016.

Symbolic Model Checking for Factored Probabilistic Models.

David Deininger, Rayna Dimitrova, Rupak Majumdar.
ATVA 2016.

Monoids as Storage Mechanisms.

Georg Zetzsche.
Bull. EATCS 2016.

Model Checking Flat Freeze LTL on One-Counter Automata.

Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell.
CONCUR 2016.

Supervisory control synthesis for deterministic context free specification languages - Enforcing controllability least restrictively.

Anne-Kathrin Schmuck, Sven Schneider, Jörg Raisch, Uwe Nestmann.
Discret. Event Dyn. Syst. 2016.

Permutations of context-free, ET0L and indexed languages.

Tara Brough, Laura Ciobanu, Murray Elder, Georg Zetzsche.
Discret. Math. Theor. Comput. Sci. 2016.

Relating Reachability Problems in Timed and Counter Automata.

Christoph Haase, Joël Ouaknine, James Worrell.
Fundam. Informaticae 2016.

On the Skolem Problem for Continuous Linear Dynamical Systems.

Ventsislav Chonev, Joël Ouaknine, James Worrell.
ICALP 2016.

Proving the Herman-Protocol Conjecture.

Maria Bruna, Radu Grigore, Stefan Kiefer, Joël Ouaknine, James Worrell.
ICALP 2016.

The Complexity of Downward Closure Comparisons.

Georg Zetzsche.
ICALP 2016.

On the Complexity of the Orbit Problem.

Ventsislav Chonev, Joël Ouaknine, James Worrell.
J. ACM 2016.

Parameterized Verification of Asynchronous Shared-Memory Systems.

Javier Esparza, Pierre Ganty, Rupak Majumdar.
J. ACM 2016.

First-order logic with reachability for infinite-state systems.

Emanuele D'Osualdo, Roland Meyer, Georg Zetzsche.
LICS 2016.

On Recurrent Reachability for Continuous Linear Dynamical Systems.

Ventsislav Chonev, Joël Ouaknine, James Worrell.
LICS 2016.

Solvability of Matrix-Exponential Equations.

Joël Ouaknine, Amaury Pouly, João Sousa Pinto, James Worrell.
LICS 2016.

The complexity of regular abstractions of one-counter languages.

Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, Georg Zetzsche.
LICS 2016.

Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic.

Sandra Kiefer, Pascal Schweitzer.
LICS 2016.

Monoids as Storage Mechanisms.

Georg Zetzsche.
Monoids as Storage Mechanisms. 2016.

Knapsack in Graph Groups, HNN-Extensions and Amalgamated Products.

Markus Lohrey, Georg Zetzsche.
STACS 2016.

Partial Order Reduction for Event-Driven Multi-threaded Programs.

Pallavi Maiya, Rahul Gupta, Aditya Kanade, Rupak Majumdar.
TACAS 2016.

Probabilistic CTL: The Deductive Way.

Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns, Rupak Majumdar.
TACAS 2016.

Robots at the Edge of the Cloud.

Rupak Majumdar.
TACAS 2016.

Safety Verification of Continuous-Space Pure Jump Markov Processes.

Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, Alessandro Abate.
TACAS 2016.

Supervisory controller synthesis for decomposable deterministic context free specification languages.

Kaushik Mallik, Anne-Kathrin Schmuck.
WODES 2016.

On linear recurrence sequences and loop termination.

Joël Ouaknine, James Worrell.
ACM SIGLOG News 2015.

Bbs: A Phase-Bounded Model Checker for Asynchronous Programs.

Rupak Majumdar, Zilong Wang.
CAV 2015.

Comparing asynchronous l-complete approximations and quotient based abstractions.

Anne-Kathrin Schmuck, Paulo Tabuada, Jörg Raisch.
CDC 2015.

Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes.

Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, Rupak Majumdar.
CONCUR 2015.

Rely/Guarantee Reasoning for Asynchronous Programs.

Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis.
CONCUR 2015.

Verification of Population Protocols.

Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
CONCUR 2015.

Asynchronous Liquid Separation Types.

Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis.
ECOOP 2015.

Analysis of Asynchronous Programs with Event-Based Synchronization.

Michael Emmi, Pierre Ganty, Rupak Majumdar, Fernando Rosa-Velardo.
ESOP 2015.

The Cyclic-Routing UAV Problem is PSPACE-Complete.

Hsi-Ming Ho, Joël Ouaknine.
FoSSaCS 2015.

Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs.

Rayna Dimitrova, Rupak Majumdar.
GandALF 2015.

Computing the Skorokhod distance between polygonal traces.

Rupak Majumdar, Vinayak S. Prabhu.
HSCC 2015.

Dynamic scheduling for networked control systems.

Indranil Saha, Sanjoy Baruah, Rupak Majumdar.
HSCC 2015.

An Approach to Computing Downward Closures.

Georg Zetzsche.
ICALP 2015.

Rational subsets and submonoids of wreath products.

Markus Lohrey, Benjamin Steinberg, Georg Zetzsche.
Inf. Comput. 2015.

Reachability problems for Markov chains.

S. Akshay, Timos Antonopoulos, Joël Ouaknine, James Worrell.
Inf. Process. Lett. 2015.

On the Complexity of Linear Arithmetic with Divisibility.

Antonia Lechner, Joël Ouaknine, James Worrell.
LICS 2015.

Graphs Identified by Logics with Counting.

Sandra Kiefer, Pascal Schweitzer, Erkal Selman.
MFCS 2015.

The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets.

Georg Zetzsche.
RP 2015.

On Termination of Integer Linear Loops.

Joël Ouaknine, João Sousa Pinto, James Worrell.
SODA 2015.

The Polyhedron-Hitting Problem.

Ventsislav Chonev, Joël Ouaknine, James Worrell.
SODA 2015.

Computing Downward Closures for Stacked Counter Automata.

Georg Zetzsche.
STACS 2015.

On Matrix Powering in Low Dimensions.

Esther Galby, Joël Ouaknine, James Worrell.
STACS 2015.

Approximate Counting in SMT and Value Estimation for Probabilistic Programs.

Dmitry Chistikov, Rayna Dimitrova, Rupak Majumdar.
TACAS 2015.

Synthesis of Geometry Proof Problems.

Chris Alvin, Sumit Gulwani, Rupak Majumdar, Supratik Mukhopadhyay.
AAAI 2014.

Abstractions from proofs.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan.
ACM SIGPLAN Notices 2014.

An SMT-Based Approach to Coverability Analysis.

Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, Filip Niksic.
CAV 2014.

Regression Test Selection for Distributed Software Histories.

Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi, Darko Marinov.
CAV 2014.

Constructing (Bi)similar finite state abstractions using asynchronous l-complete approximations.

Anne-Kathrin Schmuck, Jörg Raisch.
CDC 2014.

Bounds on Mobility.

Reiner Hüchting, Rupak Majumdar, Roland Meyer.
CONCUR 2014.

Verification of Cyber-Physical Systems (Dagstuhl Seminar 14122).

Rupak Majumdar, Richard M. Murray, Pavithra Prabhakar.
Dagstuhl Reports 2014.

Deductive control synthesis for alternating-time logics.

Rayna Dimitrova, Rupak Majumdar.
EMSOFT 2014.

Dynamic Package Interfaces.

Shahram Esmaeilsabzali, Rupak Majumdar, Thomas Wies, Damien Zufferey.
FASE 2014.

Kuai: A model checker for software-defined networks.

Rupak Majumdar, Sai Deep Tetali, Zilong Wang.
FMCAD 2014.

Foundations for Decision Problems in Separation Logic with General Inductive Predicates.

Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, Joël Ouaknine.
FoSSaCS 2014.

Model checking Timed CSP.

Philip J. Armstrong, Gavin Lowe, Joël Ouaknine, Bill Roscoe.
HOWARD-60 2014.

Edit distance for timed automata.

Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Rupak Majumdar.
HSCC 2014.

On the Complexity of Temporal-Logic Path Checking.

Daniel Bundala, Joël Ouaknine.
ICALP 2014.

On the Positivity Problem for Simple Linear Recurrence Sequences, .

Joël Ouaknine, James Worrell.
ICALP 2014.

Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences.

Joël Ouaknine, James Worrell.
ICALP 2014.

Unary Pushdown Automata and Straight-Line Programs.

Dmitry Chistikov, Rupak Majumdar.
ICALP 2014.

Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions.

Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, John Lygeros.
IEEE Trans. Autom. Control. 2014.

Towards Robustness for Cyber-Physical Systems.

Paulo Tabuada, Sina Yamac Caliskan, Matthias Rungger, Rupak Majumdar.
IEEE Trans. Autom. Control. 2014.

Simulation and bisimulation over multiple time scales in a behavioral setting.

Anne-Kathrin Schmuck, Jörg Raisch.
MED 2014.

Advances in Parametric Real-Time Reasoning.

Daniel Bundala, Joël Ouaknine.
MFCS 2014.

The Monoid of Queue Actions.

Martin Huschenbett, Dietrich Kuske, Georg Zetzsche.
MFCS 2014.

Race detection for Android applications.

Pallavi Maiya, Aditya Kanade, Rupak Majumdar.
PLDI 2014.

Online Monitoring of Metric Temporal Logic.

Hsi-Ming Ho, Joël Ouaknine, James Worrell.
RV 2014.

Positivity Problems for Low-Order Linear Recurrence Sequences.

Joël Ouaknine, James Worrell.
SODA 2014.

Foundations of Infinite-State Verification.

Rupak Majumdar.
Software Systems Safety 2014.

On Boolean closed full trios and rational Kripke frames.

Markus Lohrey, Georg Zetzsche.
STACS 2014.

Asynchronous I-complete approximations.

Anne-Kathrin Schmuck, Jörg Raisch.
Syst. Control. Lett. 2014.

Extending Supervisory Controller Synthesis to Deterministic Pushdown Automata - Enforcing Controllability Least Restrictively.

Anne-Kathrin Schmuck, Sven Schneider, Jörg Raisch, Uwe Nestmann.
WODES 2014.

Reducing an Operational Supervisory Control Problem by Decomposition for Deterministic Pushdown Automata.

Sven Schneider, Anne-Kathrin Schmuck, Uwe Nestmann, Jörg Raisch.
WODES 2014.

A Uniformization Theorem for Nested Word to Word Transductions

Dmitry Chistikov, Rupak Majumdar.
Technical Report MPI-SWS-2013-002 2013.

A theory of robust omega-regular software synthesis.

Rupak Majumdar, Elaine Render, Paulo Tabuada.
ACM Trans. Embed. Comput. Syst. 2013.

Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points.

Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Joël Ouaknine, Jean-François Raskin, James Worrell.
ATVA 2013.

Incremental, Inductive Coverability.

Johannes Kloos, Rupak Majumdar, Filip Niksic, Ruzica Piskac.
CAV 2013.

SeLoger: A Tool for Graph-Based Reasoning in Separation Logic.

Christoph Haase, Samin Ishtiaq, Joël Ouaknine, Matthew J. Parkinson.
CAV 2013.

The first workshop on language support for privacy-enhancing technologies (PETShop'13).

Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith.
CCS 2013.

Bisimilar finite abstractions of stochastic control systems.

Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, John Lygeros.
CDC 2013.

Compositional equivalence checking for models and code of control systems.

Rupak Majumdar, Indranil Saha, Koichi Ueda, Hakan Yazarel.
CDC 2013.

A Uniformization Theorem for Nested Word to Word Transductions.

Dmitry Chistikov, Rupak Majumdar.
CIAA 2013.

A Theory of Name Boundedness.

Reiner Hüchting, Rupak Majumdar, Roland Meyer.
CONCUR 2013.

Expand, Enlarge, and Check for Branching Vector Addition Systems.

Rupak Majumdar, Zilong Wang.
CONCUR 2013.

Supervisor synthesis for controller upgrades.

Johannes Kloos, Rupak Majumdar.
DATE 2013.

Synthesis of Fixed-point Programs

Eva Darulova, Viktor Kuncak, Rupak Majumdar, Indranil Saha.
EMSOFT 2013.

Decision Problems for Linear Recurrence Sequences.

Joël Ouaknine.
FCT 2013.

Verifying multi-threaded software with impact.

Björn Wachter, Daniel Kroening, Joël Ouaknine.
FMCAD 2013.

Algorithmic probabilistic game semantics - Playing games with automata.

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell.
Formal Methods Syst. Des. 2013.

Code aware resource management.

Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Rupak Majumdar, Vishwanath Raman.
Formal Methods Syst. Des. 2013.

Specification and Verification of Linear Dynamical Systems: Advances and Challenges.

Joël Ouaknine.
FroCos 2013.

A Theory of Partitioned Global Address Spaces.

Georgel Calin, Egor Derevenetc, Rupak Majumdar, Roland Meyer.
FSTTCS 2013.

Rational Subsets and Submonoids of Wreath Products.

Markus Lohrey, Benjamin Steinberg, Georg Zetzsche.
ICALP 2013.

Silent Transitions in Automata with Storage.

Georg Zetzsche.
ICALP 2013.

The Complexity of Coverage.

Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar.
Int. J. Found. Comput. Sci. 2013.

From tests to proofs.

Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko.
Int. J. Softw. Tools Technol. Transf. 2013.

Discrete Linear Dynamical Systems.

Joël Ouaknine.
LATA 2013.

Expressive Completeness for Metric Temporal Logic.

Paul Hunter, Joël Ouaknine, James Worrell.
LICS 2013.

A Static Analysis Framework for Livelock Freedom in CSP

Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell.
Log. Methods Comput. Sci. 2013.

On the Complexity of Equivalence and Minimisation for Q-weighted Automata

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell.
Log. Methods Comput. Sci. 2013.

Semilinearity and Context-Freeness of Languages Accepted by Valence Automata.

P. Buckheister, Georg Zetzsche.
MFCS 2013.

Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian.

Ranko Lazic, Joël Ouaknine, James Worrell.
MFCS 2013.

MrCrypt: static analysis for secure cloud computations.

Sai Deep Tetali, Mohsen Lesani, Rupak Majumdar, Todd D. Millstein.
OOPSLA 2013.

Provenance Verification.

Rupak Majumdar, Roland Meyer, Zilong Wang.
RP 2013.

Static Provenance Verification for Message Passing Programs.

Rupak Majumdar, Roland Meyer, Zilong Wang.
SAS 2013.

Decision Problems for Linear Recurrence Sequences.

Joël Ouaknine.
SCSS 2013.

The orbit problem in higher dimensions.

Ventsislav Chonev, Joël Ouaknine, James Worrell.
STOC 2013.

Backstepping controller synthesis and characterizations of incremental stability.

Majid Zamani, Nathan van de Wouw, Rupak Majumdar.
Syst. Control. Lett. 2013.

Model Checking Database Applications.

Milos Gligoric, Rupak Majumdar.
TACAS 2013.

Automatic predicate abstraction of C programs.

Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani.
ACM SIGPLAN Notices 2012.

Equivalence of Games with Probabilistic Uncertainty and Partial-Observation Games.

Krishnendu Chatterjee, Martin Chmelik, Rupak Majumdar.
ATVA 2012.

APEX: An Analyzer for Open Probabilistic Programs.

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell.
CAV 2012.

Approximately Bisimilar Symbolic Models for Digital Control Systems.

Rupak Majumdar, Majid Zamani.
CAV 2012.

Recent Developments in FDR.

Philip J. Armstrong, Michael Goldsmith, Gavin Lowe, Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell.
CAV 2012.

Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461).

Nikolaj Bjørner, Krishnendu Chatterjee, Laura Kovács, Rupak Majumdar.
Dagstuhl Reports 2012.

Input-output robustness for discrete systems.

Paulo Tabuada, Ayca Balkan, Sina Y. Caliskan, Yasser Shoukry, Rupak Majumdar.
EMSOFT 2012.

Synthesis of minimal-error control software.

Rupak Majumdar, Indranil Saha, Majid Zamani.
EMSOFT 2012.

Trigger memoization in self-triggered control.

Indranil Saha, Rupak Majumdar.
EMSOFT 2012.

Language-Theoretic Abstraction Refinement.

Zhenyue Long, Georgel Calin, Rupak Majumdar, Roland Meyer.
FASE 2012.

On termination and invariance for faulty channel machines.

Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, James Worrell.
Formal Aspects Comput. 2012.

Three tokens in Herman's algorithm.

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell.
Formal Aspects Comput. 2012.

Bounded underapproximations.

Pierre Ganty, Rupak Majumdar, Benjamin Monmege.
Formal Methods Syst. Des. 2012.

Branching-Time Model Checking of Parametric One-Counter Automata.

Stefan Göller, Christoph Haase, Joël Ouaknine, James Worrell.
FoSSaCS 2012.

On the Complexity of the Equivalence Problem for Probabilistic Automata.

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell.
FoSSaCS 2012.

Discounting and Averaging in Games across Time scales.

Krishnendu Chatterjee, Rupak Majumdar.
Int. J. Found. Comput. Sci. 2012.

A Perfect Model for Bounded Verification.

Javier Esparza, Pierre Ganty, Rupak Majumdar.
LICS 2012.

Countermodels from Sequent Calculi in Multi-Modal Logics

Deepak Garg, Valerio Genovese, Sara Negri.
LICS 2012.

On the Magnitude of Completeness Thresholds in Bounded Model Checking.

Daniel Bundala, Joël Ouaknine, James Worrell.
LICS 2012.

CLSE: Closed-Loop Symbolic Execution.

Rupak Majumdar, Indranil Saha, K. C. Shashidhar, Zilong Wang.
NASA Formal Methods 2012.

Engage: a deployment management system.

Jeffrey Fischer, Rupak Majumdar, Shahram Esmaeilsabzali.
PLDI 2012.

Decision Problems for Linear Recurrence Sequences.

Joël Ouaknine, James Worrell.
RP 2012.

On the Relationship between Reachability Problems in Timed and Counter Automata.

Christoph Haase, Joël Ouaknine, James Worrell.
RP 2012.

Efficient May Happen in Parallel Analysis for Async-Finish Parallelism.

Jonathan K. Lee, Jens Palsberg, Rupak Majumdar, Hong Hong.
SAS 2012.

SAT-solving in CSP trace refinement.

Hristina Palikareva, Joël Ouaknine, A. W. Roscoe.
Sci. Comput. Program. 2012.

Lecture Notes on Software Model Checking.

Rupak Majumdar.
Software Safety and Security 2012.

The Marriage of Exploration and Deduction.

Rupak Majumdar.
VSTTE 2012.

Bug-Assist: Assisting Fault Localization in ANSI-C Programs.

Manu Jose, Rupak Majumdar.
CAV 2011.

HMC: Verifying Functional Programs Using Abstract Interpreters.

Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko.
CAV 2011.

Language Equivalence for Probabilistic Automata.

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell.
CAV 2011.

Linear Completeness Thresholds for Bounded Model Checking.

Daniel Kroening, Joël Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell.
CAV 2011.

A Lyapunov approach in incremental stability.

Majid Zamani, Rupak Majumdar.
CDC/ECC 2011.

Static Livelock Analysis in CSP.

Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell.
CONCUR 2011.

Tractable Reasoning in a Fragment of Separation Logic.

Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, James Worrell.
CONCUR 2011.

The Church Synthesis Problem with Metric.

Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, James Worrell.
CSL 2011.

A Sufficient Condition for Erasing Productions to Be Avoidable.

Georg Zetzsche.
Developments in Language Theory 2011.

Performance-aware scheduler synthesis for control systems.

Rupak Majumdar, Indranil Saha, Majid Zamani.
EMSOFT 2011.

End-to-End Guarantees in Embedded Control Systems - (Abstract).

Rupak Majumdar.
Ershov Memorial Conference 2011.

Minimum Attention Controller Synthesis for Omega-Regular Objectives.

Krishnendu Chatterjee, Rupak Majumdar.
FORMATS 2011.

Pessoa 2.0: a controller synthesis tool for cyber-physical systems.

Pritam Roy, Paulo Tabuada, Rupak Majumdar.
HSCC 2011.

Robust discrete synthesis against unspecified disturbances.

Rupak Majumdar, Elaine Render, Paulo Tabuada.
HSCC 2011.

On Reachability for Hybrid Automata over Bounded Time.

Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Joël Ouaknine, Jean-François Raskin, James Worrell.
ICALP 2011.

On Stabilization in Herman's Algorithm.

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, James Worrell, Lijun Zhang.
ICALP 2011.

On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids.

Georg Zetzsche.
ICALP 2011.

VCG with Communities on Random Ad Hoc Networks.

Gunes Ercal, Rafit Izhak-Ratzin, Rupak Majumdar, Adam Meyerson.
Int. J. Distributed Sens. Networks 2011.

Toward Understanding the Generative Capacity of Erasing Rules in Matrix Grammars.

Georg Zetzsche.
Int. J. Found. Comput. Sci. 2011.

Preface.

Michael W. Mislove, Joël Ouaknine.
MFPS 2011.

Cause clue clauses: error localization using maximum satisfiability.

Manu Jose, Rupak Majumdar.
PLDI 2011.

On Searching for Small Kochen-Specker Vector Systems.

Felix Arends, Joël Ouaknine, Charles W. Wampler.
WG 2011.

Computing Rational Radical Sums in Uniform TC^0.

Paul Hunter, Patricia Bouyer, Nicolas Markey, Joël Ouaknine, James Worrell.
FSTTCS 2010.

Discounting in Games across Time Scales

Krishnendu Chatterjee, Rupak Majumdar.
GANDALF 2010.

Model Checking Succinct and Parametric One-Counter Automata.

Stefan Göller, Christoph Haase, Joël Ouaknine, James Worrell.
ICALP 2010.

On Erasing Productions in Random Context Grammars.

Georg Zetzsche.
ICALP 2010.

Towards a Theory of Time-Bounded Verification.

Joël Ouaknine, James Worrell.
ICALP 2010.

Alternating Timed Automata over Bounded Time.

Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, James Worrell.
LICS 2010.

Algorithms for Game Metrics (Full Version)

Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar, Vishwanath Raman.
Log. Methods Comput. Sci. 2010.

Systematic testing for control applications.

Rupak Majumdar, Indranil Saha, Zilong Wang.
MEMOCODE 2010.

On Process-Algebraic Extensions of Metric Temporal Logic.

Christoph Haase, Joël Ouaknine, James Worrell.
Reflections on the Work of C. A. R. Hoare 2010.

Shape Analysis with Reference Set Relations.

Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur.
VMCAI 2010.

Software model checking.

Ranjit Jhala, Rupak Majumdar.
ACM Comput. Surv. 2009.

Reducing Test Inputs Using Information Partitions.

Rupak Majumdar, Ru-Gang Xu.
CAV 2009.

Reachability in Succinct and Parametric One-Counter Automata.

Christoph Haase, Stephan Kreutzer, Joël Ouaknine, James Worrell.
CONCUR 2009.

Time-Bounded Verification.

Joël Ouaknine, Alexander Rabinovich, James Worrell.
CONCUR 2009.

Erasing in Petri Net Languages and Matrix Grammars.

Georg Zetzsche.
Developments in Language Theory 2009.

Fine-Grained Access Control with Object-Sensitive Roles.

Jeffrey Fischer, Daniel Marino, Rupak Majumdar, Todd D. Millstein.
ECOOP 2009.

Faster FDR Counterexample Generation Using SAT-Solving.

Hristina Palikareva, Joël Ouaknine, Bill Roscoe.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 2009.

Analyzing Real-Time Event-Driven Programs.

Pierre Ganty, Rupak Majumdar.
FORMATS 2009.

Multiset Pushdown Automata.

Manfred Kudlek, Patrick Totzke, Georg Zetzsche.
Fundam. Informaticae 2009.

Properties of Multiset Language Classes Defined by Multiset Pushdown Automata.

Manfred Kudlek, Patrick Totzke, Georg Zetzsche.
Fundam. Informaticae 2009.

IPR: In-Place Reconfiguration for FPGA fault tolerance.

Zhe Feng, Yu Hu, Lei He, Rupak Majumdar.
ICCAD 2009.

Team Incentives in BitTorrent Systems.

Rafit Izhak-Ratzin, Nikitas Liogkas, Rupak Majumdar.
ICCCN 2009.

An abstraction-based decision procedure for bit-vector arithmetic.

Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady.
Int. J. Softw. Tools Technol. Transf. 2009.

Simultaneous test pattern compaction, ordering and X-filling for testing power reduction.

Ju-Yueh Lee, Yu Hu, Rupak Majumdar, Lei He.
ISQED 2009.

Verifying liveness for asynchronous programs.

Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko.
POPL 2009.

Symbolic Robustness Analysis.

Rupak Majumdar, Indranil Saha.
RTSS 2009.

Verifying Reference Counting Implementations.

Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar.
TACAS 2009.

CSIsat: Interpolation for LA+EUF.

Dirk Beyer, Damien Zufferey, Rupak Majumdar.
CAV 2008.

FPGA area reduction by multi-output function based sequential resynthesis.

Yu Hu, Victor Shih, Rupak Majumdar, Lei He.
DAC 2008.

Some Recent Results in Metric Temporal Logic.

Joël Ouaknine, James Worrell.
FORMATS 2008.

Language Classes Defined by Concurrent Finite Automata.

Matthias Jantzen, Manfred Kudlek, Georg Zetzsche.
Fundam. Informaticae 2008.

Nets with Tokens which Carry Data.

Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell.
Fundam. Informaticae 2008.

Petri Net Controlled Finite Automata.

Berndt Farwer, Matthias Jantzen, Manfred Kudlek, Heiko Rölke, Georg Zetzsche.
Fundam. Informaticae 2008.

Universality Analysis for One-Clock Timed Automata.

Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, Karin Quaas, James Worrell.
Fundam. Informaticae 2008.

On Expressiveness and Complexity in Real-Time Model Checking.

Patricia Bouyer, Nicolas Markey, Joël Ouaknine, James Worrell.
ICALP 2008.

Exploiting Symmetries to Speed Up SAT-Based Boolean Matching for Logic Synthesis of FPGAs.

Yu Hu, Victor Shih, Rupak Majumdar, Lei He.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2008.

Stochastic limit-average games are in EXPTIME.

Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger.
Int. J. Game Theory 2008.

Game Refinement Relations and Metrics.

Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, Mariëlle Stoelinga.
Log. Methods Comput. Sci. 2008.

Labeled Step Sequences in Petri Nets.

Matthias Jantzen, Georg Zetzsche.
Petri Nets 2008.

On Termination for Faulty Channel Machines.

Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, James Worrell.
STACS 2008.

On Automated Verification of Probabilistic Programs.

Axel Legay, Andrzej S. Murawski, Joël Ouaknine, James Worrell.
TACAS 2008.

Directed test generation using symbolic grammars.

Rupak Majumdar, Ru-Gang Xu.
ASE 2007.

Undecidability of Universality for Timed Automata with Minimal Resources.

Sara Adams, Joël Ouaknine, James Worrell.
FORMATS 2007.

Zone-Based Universality Analysis for Single-Clock Timed Automata.

Parosh Aziz Abdulla, Joël Ouaknine, Karin Quaas, James Worrell.
FSEN 2007.

Nets with Tokens Which Carry Data.

Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell.
ICATPN 2007.

The software model checker Blast.

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar.
Int. J. Softw. Tools Technol. Transf. 2007.

The Cost of Punctuality.

Patricia Bouyer, Nicolas Markey, Joël Ouaknine, James Worrell.
LICS 2007.

On the decidability and complexity of Metric Temporal Logic over finite words.

Joël Ouaknine, James Worrell.
Log. Methods Comput. Sci. 2007.

Deciding Bit-Vector Arithmetic with Abstraction.

Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady.
TACAS 2007.

Sudoku as a SAT Problem.

Inês Lynce, Joël Ouaknine.
AI&M 2006.

On Timed Models and Full Abstraction.

Gavin Lowe, Joël Ouaknine.
Electr. Notes Theor. Comput. Sci. 2006.

Parallel Assignments in Software Model Checking.

Murray Stokely, Sagar Chaki, Joël Ouaknine.
Electron. Notes Theor. Comput. Sci. 2006.

Timed CSP: A Retrospective.

Joël Ouaknine, Steve Schneider.
Electron. Notes Theor. Comput. Sci. 2006.

On Metric Temporal Logic and Faulty Turing Machines.

Joël Ouaknine, James Worrell.
FoSSaCS 2006.

Sudoku as a SAT Problem.

Inês Lynce, Joël Ouaknine.
ISAIM 2006.

Safety Metric Temporal Logic Is Fully Decidable.

Joël Ouaknine, James Worrell.
TACAS 2006.

Timed CSP: A Retrospective.

Joël Ouaknine, Steve A. Schneider.
APC 25 2005.

On Probabilistic Program Equivalence and Refinement.

Andrzej S. Murawski, Joël Ouaknine.
CONCUR 2005.

Concurrent software verification with states, events, and deadlocks.

Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha.
Formal Aspects Comput. 2005.

Decidability and Complexity Results for Timed Automata via Channel Machines.

Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, James Worrell.
ICALP 2005.

State/Event Software Verification for Branching-Time Specifications.

Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith.
IFM 2005.

Computational challenges in bounded model checking.

Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman.
Int. J. Softw. Tools Technol. Transf. 2005.

On the Decidability of Metric Temporal Logic.

Joël Ouaknine, James Worrell.
LICS 2005.

On Timed Models and Full Abstraction.

Gavin Lowe, Joël Ouaknine.
MFPS 2005.

Verification of Reactive Systems: Formal Methods and Algorithms. By Klaus Schneider. Springer, Texts in Theoretical Computer Science Series, 2004, ISBN: 3-540-00296-0, pp 600.

Joël Ouaknine.
Softw. Test. Verification Reliab. 2005.

Cookie	Duration	Description
cookielawinfo-checkbox-analytics	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Analytics".
cookielawinfo-checkbox-functional	11 months	The cookie is set by GDPR cookie consent to record the user consent for the cookies in the category "Functional".
cookielawinfo-checkbox-necessary	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookies is used to store the user consent for the cookies in the category "Necessary".
cookielawinfo-checkbox-others	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Other.
cookielawinfo-checkbox-performance	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Performance".
viewed_cookie_policy	11 months	The cookie is set by the GDPR Cookie Consent plugin and is used to store whether or not user has consented to the use of cookies. It does not store any personal data.