DROPS

Volume

LIPIcs, Volume 171

31st International Conference on Concurrency Theory (CONCUR 2020)

CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference)

Editors: Igor Konnov and Laura Kovács

Document

Short Paper

DOI: 10.4230/LIPIcs.ITP.2026.36

Lean on Vampire Proofs (Short Paper)

Authors: Jonas Bodingbauer, Márton Hajdu, Laura Kovács, Axel Polaczek, and Michael Rawson

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

Vampire proves theorems completely automatically in first- and higher-order logic extended with theories. Proof checking is increasingly demanded to consolidate user trust in Vampire’s output. We describe ongoing efforts in reconstructing Vampire proofs as trusted proofs in Lean. Our experiments showcase feasibility of generating trusted Vampire proofs that are validated in Lean.

Cite as

Jonas Bodingbauer, Márton Hajdu, Laura Kovács, Axel Polaczek, and Michael Rawson. Lean on Vampire Proofs (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 36:1-36:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bodingbauer_et_al:LIPIcs.ITP.2026.36,
  author =	{Bodingbauer, Jonas and Hajdu, M\'{a}rton and Kov\'{a}cs, Laura and Polaczek, Axel and Rawson, Michael},
  title =	{{Lean on Vampire Proofs}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{36:1--36:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.36},
  URN =		{urn:nbn:de:0030-drops-270102},
  doi =		{10.4230/LIPIcs.ITP.2026.36},
  annote =	{Keywords: Automated Reasoning, Interactive Theorem Provers, Automated Theorem Provers, Lean, Vampire, Proof Reconstruction}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.SAT.2026.1

SAT in Saturation: A Satisfied Match (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract

Saturation is the leading concept behind the proof-search algorithms of state-of-the-art first-order theorem provers [Filip Bártek et al., 2025; Christoph Weidenbach et al., 2009; Stephan Schulz et al., 2019]. The key idea behind saturation-based proof search is to reduce the problem of proving validity of a first-order formula to the problem of establishing unsatisfiability of the respective formula, by using a sound inference system, such as resolution and superposition [Leo Bachmair and Harald Ganzinger, 2001; Robert Nieuwenhuis and Albert Rubio, 2001]. Central to efficient saturation-based proof search is the implementation of redundancy in the form of simplification rules [John Alan Robinson, 1965; Laura Kovács and Andrei Voronkov, 2013]: such rules do not add new formulas to search space, but instead simplify/delete redundant formulas from the search space, while not loosing refutational completeness of superposition. Redundancy in first-order theorem proving is controlled via term/clause ordering and literal selection functions in extension of standard superposition: redundant clauses are logical consequences of smaller clauses with respect to the considered ordering. While redundancy is essential for efficient proof search, establishing whether an arbitrary first-order formula is redundant is as hard as proving whether it is valid. First-order provers therefore implement sufficient conditions towards proving redundancy, so that these conditions can be efficiently checked, ideally using only syntactic arguments over formulas. One such condition comes with the notion of subsumption, yielding one of the most important simplification rules in automated reasoners [Leo Bachmair and Harald Ganzinger, 1994]. It is common that millions of subsumption checks are performed during a single solver run [Jakob Rath et al., 2022]. However, in contrast to propositional subsumption as used by SAT solvers and implemented using sophisticated polynomial algorithms, first-order subsumption in first-order theorem proving involves NP-complete search queries, turning the efficient use of first-order subsumption into a huge practical burden. This talks presents a tailored integration of SAT solving for detecting variants of subsumption in superposition. Key to our approach is retrieving clauses from the search space and checking whether subsumption with retrieved clauses can be applied, using multi-literal matching. A solution to our SAT-based encoding gives a concrete application of (variants of) subsumption, allowing the first-order prover to apply that instance of subsumption as a simplification rule during saturation [Bernhard Gleiss et al., 2020; Jakob Rath et al., 2022; Robin Coutelier et al., 2025]. Our SAT encoding captures subset relations among literals/clauses and formalizes matching of literals between inference premises/conclusions. We show that SAT encodings improve literal matching, and thus subsumption, in first-order theorem proving. In particular, our experimental results using the Vampire prover demonstrate the practical benefits of using SAT solving for variants of first-order subsumption.

Cite as

Laura Kovács. SAT in Saturation: A Satisfied Match (Invited Talk). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.SAT.2026.1,
  author =	{Kov\'{a}cs, Laura},
  title =	{{SAT in Saturation: A Satisfied Match}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.1},
  URN =		{urn:nbn:de:0030-drops-263076},
  doi =		{10.4230/LIPIcs.SAT.2026.1},
  annote =	{Keywords: Automated Reasoning, First-Order Theorem Proving, Superposition, Subsumption, Redundancy, SAT Solving, Vampire}
}

Document

DOI: 10.4230/LIPIcs.SAT.2026.14

Generalizing CDCL with Graph Backtracking

Authors: Robin Coutelier, Thomas Hader, and Laura Kovács

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract

We present graph backtracking, a novel, fine-grained backtracking scheme for CDCL-based SAT solving, parametrized by a user-defined weight function. For conflict repair, we challenge the decision level abstraction and use the implication graph as a precise guiding structure to minimize the weight of literals that are unassigned. Graph backtracking is sound, complete, and terminating. We show that it is a generalization of chronological and non-chronological backtracking by simulating them with specific weight functions. Our approach is implemented in the experimental solver NapSAT. Empirical results show that graph backtracking requires fewer literal propagations than standard approaches, leading to improved solver runtime.

Cite as

Robin Coutelier, Thomas Hader, and Laura Kovács. Generalizing CDCL with Graph Backtracking. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{coutelier_et_al:LIPIcs.SAT.2026.14,
  author =	{Coutelier, Robin and Hader, Thomas and Kov\'{a}cs, Laura},
  title =	{{Generalizing CDCL with Graph Backtracking}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.14},
  URN =		{urn:nbn:de:0030-drops-263203},
  doi =		{10.4230/LIPIcs.SAT.2026.14},
  annote =	{Keywords: SAT Solving, Backtracking, Conflict Analysis, CDCL}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2026.2

Saturation-Guided Inductive Synthesis (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

Proof by induction is common-place in mathematics [Josef Urban and Geoff Sutcliffe, 2010; Martin Desharnais et al., 2022], formal verification [Raven Beutner and Bernd Finkbeiner, 2024; Wolfgang Ahrendt et al., 2000; Pamina Georgiou et al., 2022], cybersecurity [Simon Jeanteur et al., 2024; Evan Laufer et al., 2024], and many more areas. This talk overviews recent progress in automating inductive reasoning in quantified logic, with applications to code synthesis. Key to our work is saturation-based first-order theorem proving [Laura Kovács and Andrei Voronkov, 2013], using variants of the superposition calculus [Robert Nieuwenhuis and Albert Rubio, 2001]. We show that induction and synthesis are better together in saturation, allowing us not only to prove quantified properties F, but also generate a functional implementation of F during proof search. We showcase our results using the first-order theorem prover Vampire [Filip Bártek et al., 2025], a completely automatic push-button theorem prover for first-order logic with theories, including arithmetic, inductively defined datatypes, induction, and higher-order logic. We structure our talk within three inter-connected parts. First, we overview the main ingredients behind saturation provers [Filip Bártek et al., 2025; Stephan Schulz et al., 2019; Christoph Weidenbach et al., 2009] using superposition. Such provers work by negating an input conjecture F, transforming ¬ F into a clausal normal form, and using superposition inferences to derive new clauses from existing ones until a contradiction is reached; when a contradiction is derived, validity of F is established. Many years of development in saturation-based theorem proving have gone into making this process as efficient as possible, while deriving new clauses only when needed in order to tame growth of the search space. Doing so, highly-efficient superposition calculi parametrized by so-called clause selection functions have been proposed, in order to make as few inferences between clauses as possible. Redundancy elimination techniques further prune the search space. Next, we show how to formalize applications of induction in the saturation process [Márton Hajdú et al., 2022], without bringing drastic changes into the overall framework of first-order proving. A natural choice for implementing induction would be by reducing goals to subgoals, in particular by proving a base case and an inductive step case of a valid induction principle. For example, a goal ∀ x. F(x) over natural numbers x can be proven using structural induction: we prove F[0] (base case) and ∀ x. F(x) ⇒ F(x+1) (step case). However, saturation theorem proving is not about reducing goals to subgoals: in principle, each clause in the search space can be chosen during any step of saturation. We therefore automate induction in saturation as follows. When a clause F(x) is chosen and inductive reasoning over F should be applied (for example, because F uses inductively defined data types x, such as natural numbers), we combine the application of a valid induction schema over F(x) with resolution. Put it simply, induction and resolution are combined in one step of saturation, allowing us to use parts of F(x) as subgoals of F(x). Interestingly with this approach is that clauses generated during saturation may be stronger than the induction schema and, most importantly, are friendly to saturation provers: they are mostly quantifier-free Horn clauses and their (at most one) positive equality cannot be used in many inferences during saturation. Thus, applying many induction inferences during proof search would hardly affect the performance of a saturation prover. Figure 1 lists a property over natural numbers: every natural number x is the half of another natural number y. Proving this property in saturation, and in particular using Vampire, can be achieved by (structural) induction over x. Finally, we extend saturation proof search with code synthesis [Petra Hozzová et al., 2024]. While proving formula F, we track the constructive parts of the proof of F using so-called answer literals [Cordell Green, 1969]. We use these parts to synthesize a program satisfying F and use the applications of induction in saturation to construct recursive programs satisfying F. In a nutshell, the base case and inductive case steps of induction in saturation express how to construct the desired program for the next recursive step using the program for the previous recursive step; we capture this information via answer literals. When we apply induction in saturation, we introduce a special term into the answer literal and record the program corresponding to the induction step. As we prove induction steps, we capture their corresponding programs in the answer literal. Finally, we convert the special tracker terms from the answer literals into recursive functions, and obtain a program satisfying property F. For example, from the proof of property of Figure 1, our approach implemented in Vampire infers the following functional implementation of a recursive function r, while using only the signature of Figure 1: 𝗋(0) & := 0 𝗋(s(x)) & := s(s(𝗋(x))) The above inferred function r satisfies the property of Figure 1 and, for each input natural number x, computes a natural number 𝗋(x) such that x is half of 𝗋(x). In summary, induction and synthesis are better together in saturation-based theorem proving using the superposition calculus. Soundness and practical use of our work has been addressed and experimented using the Vampire theorem prover, both in the case of automating induction [Márton Hajdú et al., 2022; Márton Hajdú et al., 2024] and program synthesis [Petra Hozzová et al., 2023; Petra Hozzová et al., 2024]. Interesting questions regarding completeness arise: if a program satisfying a given property exists, can we derive it from saturation-based proof search? Our recent results [Hajdu et al., 2026] answer this question for recursion-free program using additional assumptions of realizability. A natural direction for future work is to identify realizability assumptions for recursive program synthesis and induction.

Cite as

Laura Kovács. Saturation-Guided Inductive Synthesis (Invited Talk). In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.FSCD.2026.2,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Saturation-Guided Inductive Synthesis}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{2:1--2:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.2},
  URN =		{urn:nbn:de:0030-drops-263521},
  doi =		{10.4230/LIPIcs.FSCD.2026.2},
  annote =	{Keywords: automated reasoning, first-order theorem proving, saturation, induction, program synthesis}
}

Document

DOI: 10.4230/LIPIcs.STACS.2026.64

One-Clock Synthesis Problems

Authors: Sławomir Lasota, Mathieu Lehaut, Julie Parreaux, and Radosław Piórkowski

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract

We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton, and one of the players can elapse time. We perform a systematic study of synthesis problems in all variants of timed games, depending on which player’s winning condition is specified, and which player’s strategy (or controller, a finite-memory strategy) is sought. As our main result we prove ubiquitous undecidability in all the variants, both for strategy and controller synthesis, already for winning conditions specified by one-clock automata. This strengthens and generalises previously known undecidability results. We also fully characterise those cases where finite memory is sufficient to win, namely existence of a strategy implies existence of a controller. All our results are stated in the timed setting, while analogous results hold in the data setting where one-clock automata are replaced by one-register ones.

Cite as

Sławomir Lasota, Mathieu Lehaut, Julie Parreaux, and Radosław Piórkowski. One-Clock Synthesis Problems. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 64:1-64:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lasota_et_al:LIPIcs.STACS.2026.64,
  author =	{Lasota, S{\l}awomir and Lehaut, Mathieu and Parreaux, Julie and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{One-Clock Synthesis Problems}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{64:1--64:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.64},
  URN =		{urn:nbn:de:0030-drops-255533},
  doi =		{10.4230/LIPIcs.STACS.2026.64},
  annote =	{Keywords: timed automata, register automata, B\"{u}chi-Landweber games, Church synthesis problem, reactive synthesis problem}
}

Document

DOI: 10.4230/LIPIcs.STACS.2026.60

The Asymptotic Size of Finite Irreducible Semigroups of Rational Matrices

Authors: Stefan Kiefer and Andrew Ryzhikov

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract

We study finite semigroups of n × n matrices with rational entries. Such semigroups provide a rich generalization of transition monoids of unambiguous (and, in particular, deterministic) finite automata. In this paper we determine the maximum size of finite semigroups of rational n × n matrices, with the goal of shedding more light on the structure of such matrix semigroups. While in general such semigroups can be arbitrarily large in terms of n, a classical result of Schützenberger from 1962 implies an upper bound of 2^{𝒪(n² log n)} for irreducible semigroups, i.e., the only subspaces of ℚⁿ that are invariant for all matrices in the semigroup are ℚⁿ and the subspace consisting only of the zero vector. Irreducible matrix semigroups can be viewed as the building blocks of general matrix semigroups, and as such play an important role in mathematics and computer science. From the point of view of automata theory, they generalize strongly connected automata. Using a very different technique from that of Schützenberger, we improve the upper bound on the cardinality to 3^{n²}. This is the main result of the paper. The bound is in some sense tight, as we show that there exists, for every n, a finite irreducible semigroup with 3^{⌊ n²/4 ⌋} rational matrices. Our main result also leads to an improvement of a bound, due to Almeida and Steinberg, on the mortality threshold. The mortality threshold is a number 𝓁 such that if the zero matrix is in the semigroup, then the zero matrix can be written as a product of at most 𝓁 matrices from any subset that generates the semigroup.

Cite as

Stefan Kiefer and Andrew Ryzhikov. The Asymptotic Size of Finite Irreducible Semigroups of Rational Matrices. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 60:1-60:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.STACS.2026.60,
  author =	{Kiefer, Stefan and Ryzhikov, Andrew},
  title =	{{The Asymptotic Size of Finite Irreducible Semigroups of Rational Matrices}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{60:1--60:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.60},
  URN =		{urn:nbn:de:0030-drops-255496},
  doi =		{10.4230/LIPIcs.STACS.2026.60},
  annote =	{Keywords: finite matrix semigroups, irreducible matrix semigroups, matrix mortality, aperiodic semigroups, unambiguous automata, transition monoids}
}

@InProceedings{kiefer_et_al:LIPIcs.STACS.2026.60,
  author =	{Kiefer, Stefan and Ryzhikov, Andrew},
  title =	{{The Asymptotic Size of Finite Irreducible Semigroups of Rational Matrices}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{60:1--60:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.60},
  URN =		{urn:nbn:de:0030-drops-255496},
  doi =		{10.4230/LIPIcs.STACS.2026.60},
  annote =	{Keywords: finite matrix semigroups, irreducible matrix semigroups, matrix mortality, aperiodic semigroups, unambiguous automata, transition monoids}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.STACS.2026.2

Moments in Time: Algebraic Analysis for Solvable Loops (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract

With substantial progress in automated reasoning, algebraic approaches emerged to automatically analyse program loops in an exact manner. In this invited talk, we discuss recent results in characterizing the functional behaviour of loops with polynomial arithmetic and probabilistic updates. This problem remains unsolved even when we restrict consideration to loops that are non-nested, without conditionals, and/or without exit conditions [Ehud Hrushovski et al., 2023; Julian Müllner and others, 2024]. We are motivated by applications of computer-aided verification, in particular to assess the safety, security, and sensitivity of computer systems [M. Z. Kwiatkowska et al., 2011; Gilles Barthe et al., 2012; Gilles Barthe and others, 2018; Marcel Moosbrugger et al., 2023; Alessandro Abate et al., 2023; Andrey Kofnov and others, 2024]. We are interested in modeling, deciding, and solving loop analysis. The key to our work are moment-computable loops [L. Kovács, 2008; Marcel Moosbrugger et al., 2022] which allow us to set limits on what is decidable and solvable in loop analysis. Our approach combines algebra, statistics, and automated reasoning to mechanize loop analysis. Various techniques, such as martingale theory and quantifier elimination, can be seen as examples of moment-computable loop analysis. This talk is structured within three inter-connected parts. We first bring moment-based loop analysis into the landscape of {loop invariant synthesis} and extend moment-computable loops with {termination guarantees}. We next automate the reasoning about (probabilistic) loops by summarizing loop semantics as (probabilistic) algebraic recurrences, whose closed-form solutions capture (higher-order) moments, and hence invariants, among loop variables. These recurrences together with loop tests yield moment-based (super)martingales necessary to prove loop termination and compute probability bounds on termination. We finally describe moment-computable loops whose invariant synthesis {decidable} or as {hard} as open problems, such as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008].

Cite as

Laura Kovács. Moments in Time: Algebraic Analysis for Solvable Loops (Invited Talk). In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.STACS.2026.2,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Moments in Time: Algebraic Analysis for Solvable Loops}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.2},
  URN =		{urn:nbn:de:0030-drops-254910},
  doi =		{10.4230/LIPIcs.STACS.2026.2},
  annote =	{Keywords: program analysis, algebraic reasoning, symbolic computation, loop invariants}
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.18

A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

We extend the existing HOL Light Library for Modal Systems (HOLMS) to support a modular implementation of modal reasoning within the HOL Light proof assistant. We deeply embed axiomatic calculi and relational semantics for seven normal modal logics (K, T, B, K4, S4, S5, GL) and formalise modal adequacy theorems for these systems. We then leverage those formalisations to implement a mechanism for automated reasoning via proof-search in the associated labelled sequent calculi, which we shallowly embed in HOL Light’s goal-stack mechanism. This way, we equip the general-purpose proof assistant with (semi)decision procedures for these logics that, in case of failure to construct a proof for the input formula, return a certified countermodel within the appropriate class for the logic under consideration. On the methodological side, we propose a precise measure of the modularity of our approach by systematically adopting Christopher Strachey’s distinction between ad hoc and parametric polymorphism throughout the library.

Cite as

Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bilotta_et_al:LIPIcs.CSL.2026.18,
  author =	{Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
  title =	{{A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{18:1--18:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.18},
  URN =		{urn:nbn:de:0030-drops-254427},
  doi =		{10.4230/LIPIcs.CSL.2026.18},
  annote =	{Keywords: Modal logic, HOL Light, Labelled sequent calculi, Logical verification, Interactive theorem proving, Automated proof-search}
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.16

On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions

Authors: Nicolas Peltier

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

Separation Logic (SL) is a well-established framework for reasoning about programs that manipulate dynamic memory. To express and verify properties of custom recursive data structures, SL is extended with spatial predicates defined by user-specified inductive rules. Many verification problems reduce to deciding entailments between formulas involving these predicates. While the general entailment problem is undecidable, a broad class of inductive rules - known as PCE (Progressing, Connected, and Established) - has been identified for which entailment is decidable. In this work, we extend the study of the entailment problem to Dynamic Separation Logic (DSL), an extension of SL that includes dynamic modalities for reasoning about actions on the heap and store. We show that entailment in DSL remains decidable for PCE rules by proving that dynamic modalities can be automatically eliminated.

Cite as

Nicolas Peltier. On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{peltier:LIPIcs.CSL.2026.16,
  author =	{Peltier, Nicolas},
  title =	{{On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{16:1--16:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.16},
  URN =		{urn:nbn:de:0030-drops-254402},
  doi =		{10.4230/LIPIcs.CSL.2026.16},
  annote =	{Keywords: Separation logic, Dynamic logic, Entailment problem}
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.31

Parametric Disjunctive Timed Networks

Authors: Étienne André, Swen Jacobs, and Engel Lefaucheux

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

We consider distributed systems with an arbitrary number of processes, modelled by timed automata that communicate through location guards: a process can take a guarded transition if at least one other process is in a given location. In this work, we introduce parametric disjunctive timed networks, where each timed automaton may contain timing parameters, i.e., unknown constants. We investigate two problems: deciding the emptiness of the set of parameter valuations for which 1) a given location is reachable for at least one process (local property), and 2) a global state is reachable where all processes are in a given location (global property). Our main positive result is that the first problem is decidable for networks of processes with a single clock and without invariants; this result holds for arbitrarily many timing parameters - a setting with few known decidability results. However, it becomes undecidable when invariants are allowed, or when considering global properties, even for systems with a single parameter. This highlights the significant expressive power of invariants in these networks. Additionally, we exhibit further decidable subclasses by restraining the syntax of guards and invariants.

Cite as

Étienne André, Swen Jacobs, and Engel Lefaucheux. Parametric Disjunctive Timed Networks. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 31:1-31:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:LIPIcs.CSL.2026.31,
  author =	{Andr\'{e}, \'{E}tienne and Jacobs, Swen and Lefaucheux, Engel},
  title =	{{Parametric Disjunctive Timed Networks}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{31:1--31:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.31},
  URN =		{urn:nbn:de:0030-drops-254562},
  doi =		{10.4230/LIPIcs.CSL.2026.31},
  annote =	{Keywords: parametrised verification, parametric timed automata, verification of infinite-state systems}
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.32

Mean-Payoff and Energy Discrete-Bidding Games

Authors: Guy Avni and Suman Sadhukhan

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

A bidding game is played on a graph as follows. A token is placed on an initial vertex and both players are allocated budgets. In each turn, the players simultaneously submit bids that do not exceed their available budgets, the higher bidder moves the token, and pays the bid to the lower bidder. We focus on discrete-bidding, which are motivated by practical applications and restrict the granularity of the players' bids, e.g, bids must be given in cents. We study, for the first time, discrete-bidding games with mean-payoff and energy objectives. In contrast, mean-payoff continuous-bidding games (i.e., no granularity restrictions) are understood and exhibit a rich mathematical structure. The threshold budget is a necessary and sufficient initial budget for winning an energy game or guaranteeing a target payoff in a mean-payoff game. We first establish existence of threshold budgets; a non-trivial property due to the concurrent moves of the players. Moreover, we identify the structure of the thresholds, which is key in obtaining compact strategies, and in turn, showing that finding threshold is in NP and coNP even in succinctly-represented games.

Cite as

Guy Avni and Suman Sadhukhan. Mean-Payoff and Energy Discrete-Bidding Games. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.CSL.2026.32,
  author =	{Avni, Guy and Sadhukhan, Suman},
  title =	{{Mean-Payoff and Energy Discrete-Bidding Games}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{32:1--32:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.32},
  URN =		{urn:nbn:de:0030-drops-254573},
  doi =		{10.4230/LIPIcs.CSL.2026.32},
  annote =	{Keywords: Bidding games, Discrete-bidding, Mean-payoff games, energy games}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSTTCS.2025.2

Unboundedness Problems for Formal Languages (Invited Talk)

Authors: Georg Zetzsche

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract

Informally, unboundedness problems are decision problems that ask about the existence of infinitely many words (satisfying certain properties) in a formal language. For example: Is a given language infinite? Or: Does a given language have super-polynomial growth? These came into focus in recent years because of their connections to downward closure computation and separability problems. Although unboundedness problems may seem difficult at first, it turns out that there are techniques that are at the same time conceptually very simple, but also apply to a surprisingly wide variety of language classes. The talk will survey recent results (and techniques) concerning unboundedness problems.

Cite as

Georg Zetzsche. Unboundedness Problems for Formal Languages (Invited Talk). In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zetzsche:LIPIcs.FSTTCS.2025.2,
  author =	{Zetzsche, Georg},
  title =	{{Unboundedness Problems for Formal Languages}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{2:1--2:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.2},
  URN =		{urn:nbn:de:0030-drops-250810},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.2},
  annote =	{Keywords: Decidability, formal languages, unifying frameworks, downward closure, separability}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2025.15

Extending EFX Allocations to Further Multi-Graph Classes

Authors: Umang Bhaskar and Yeshwant Pandit

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract

The existence of EFX allocations is one of the most significant open questions in fair division. Recent work by Christodoulou, Fiat, Koutsoupias, and Sgouritsa ("Fair allocation in graphs," EC 2023) establishes the existence of EFX allocations for graphical valuations, when agents are vertices in a graph, items are edges, and each item has zero value for all agents other than those at its endpoints. Thus, in this setting, each good has non-zero value for at most two agents, and there is at most one good valued by any pair of agents. This marks one of the few cases when an exact and complete EFX allocation is known to exist for more than three agents. In this work, we partially extend these results to multi-graphs, when each pair of vertices can have more than one edge between them. The existence of EFX allocations in multi-graphs is a natural open question given their existence in simple graphs. We show that EFX allocations exist, and can be computed in polynomial time, for agents with cancelable valuations in the following cases: (i) bipartite multi-graphs, (ii) multi-trees with monotone valuations, and (iii) multi-graphs with girth (2t-1), where t is the chromatic number of the multi-graph. The existence of EFX in cycle multi-graphs follows from (i), (iii), and the known existence of EFX for three agents.

Cite as

Umang Bhaskar and Yeshwant Pandit. Extending EFX Allocations to Further Multi-Graph Classes. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bhaskar_et_al:LIPIcs.FSTTCS.2025.15,
  author =	{Bhaskar, Umang and Pandit, Yeshwant},
  title =	{{Extending EFX Allocations to Further Multi-Graph Classes}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.15},
  URN =		{urn:nbn:de:0030-drops-250958},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.15},
  annote =	{Keywords: Fair Division, EFX, Multi-graphs}
}

Document

Invited Paper

DOI: 10.4230/OASIcs.RW.2024/2025.6

Explaining Reasoning Results for Description Logic Ontologies (Invited Paper)

Authors: Patrick Koopmann

Published in: OASIcs, Volume 138, Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025)

Abstract

The Web Ontology Language (OWL), grounded in description logics, enables reasoning systems to infer implicit knowledge in a transparent manner. However, the expressivity of description logics and the complexity of large ontologies often results in reasoning outcomes that are hard to understand without additional tool support. Explanations of these outcomes are essential for users to understand ontology content, communicate its structure and behavior effectively, and debug undesired or missing inferences. This chapter provides an overview of the central explanation techniques that have been developed for explaining reasoning with description logic ontologies. Here, we consider both explanations for positive entailments (explaining why something can be deduced), as well as negative entailments (why something cannot be deduced). More specifically, we discuss justifications, proofs and interpolation as a means to explain positive entailments, and abduction for explaining negative entailments, where we also have a closer look at practical algorithms as well as practical and theoretical challenges.

Cite as

Patrick Koopmann. Explaining Reasoning Results for Description Logic Ontologies (Invited Paper). In Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). Open Access Series in Informatics (OASIcs), Volume 138, pp. 6:1-6:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{koopmann:OASIcs.RW.2024/2025.6,
  author =	{Koopmann, Patrick},
  title =	{{Explaining Reasoning Results for Description Logic Ontologies}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{6:1--6:29},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-405-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{138},
  editor =	{Artale, Alessandro and Bienvenu, Meghyn and Garc{\'\i}a, Yazm{\'\i}n Ib\'{a}\~{n}ez and Murlak, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.RW.2024/2025.6},
  URN =		{urn:nbn:de:0030-drops-250514},
  doi =		{10.4230/OASIcs.RW.2024/2025.6},
  annote =	{Keywords: Explanations, Justifications, Proofs, Craig Interpolation, Contrastive Explanations}
}

54 Search Results for "Kovács, Laura"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message