Search Results

Documents authored by Kovács, Laura

Found 2 Possible Name Variants:

Kovacs, Laura

Document
DOI: 10.4230/LIPIcs.SAT.2024.9
Lazy Reimplication in Chronological Backtracking

Authors: Robin Coutelier, Mathias Fleury, and Laura Kovács

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose.
Cite as

Robin Coutelier, Mathias Fleury, and Laura Kovács. Lazy Reimplication in Chronological Backtracking. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{coutelier_et_al:LIPIcs.SAT.2024.9,
  author =	{Coutelier, Robin and Fleury, Mathias and Kov\'{a}cs, Laura},
  title =	{{Lazy Reimplication in Chronological Backtracking}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9},
  URN =		{urn:nbn:de:0030-drops-205313},
  doi =		{10.4230/LIPIcs.SAT.2024.9},
  annote =	{Keywords: Chronological Backtracking, CDCL, Invariants, Watcher Lists}
}
Document
DOI: 10.4230/LIPIcs.STACS.2024.41
Linear Loop Synthesis for Quadratic Invariants

Authors: S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.
Cite as

S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka. Linear Loop Synthesis for Quadratic Invariants. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 41:1-41:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hitarth_et_al:LIPIcs.STACS.2024.41,
  author =	{Hitarth, S. and Kenison, George and Kov\'{a}cs, Laura and Varonka, Anton},
  title =	{{Linear Loop Synthesis for Quadratic Invariants}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{41:1--41:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.41},
  URN =		{urn:nbn:de:0030-drops-197512},
  doi =		{10.4230/LIPIcs.STACS.2024.41},
  annote =	{Keywords: program synthesis, loop invariants, verification, Diophantine equations}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2023.4
Algebraic Reasoning for (Un)Solvable Loops (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Loop invariants describe valid program properties that hold before and after every loop iteration. As such, loop invariants are the workhorses in formalizing loop semantics and automating the formal analysis and verification of programs with loops. While automatically synthesizing loop invariants is, in general, an uncomputable problem, when considering only single-path loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus Müller-Olm and Helmut Seidl, 2004; Laura Kovács, 2008; Ehud Hrushovski et al., 2018]. Yet, already for loops with "only" polynomial updates, computing the strongest invariant has been an open challenge since 2004 [Markus Müller-Olm and Helmut Seidl, 2004]. In this invited talk, we first present computability results on polynomial invariant synthesis for restricted polynomial loops, called solvable loops [Rodríguez-Carbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closed-form solutions of algebraic recurrence equations that model the loop behaviour [Laura Kovács, 2008; Andreas Humenberger et al., 2017]. We also establish a technique for invariant synthesis for classes of loops that are not solvable, termed unsolvable loops [Daneshvar Amrollahi et al., 2022]. We next study the limits of computability in deriving the (strongest) polynomial invariants for arbitrary polynomial loops. We prove that computing the strongest polynomial invariant of arbitrary, single-path polynomial loops is very hard [Julian Müllner, 2023] - namely, it is at least as hard as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008], a prominent algebraic problem in the theory of linear recurrences. Going beyond single-path loops, we show that the strongest polynomial invariant is uncomputable already for multi-path polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].
Cite as

Laura Kovács. Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.MFCS.2023.4,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Algebraic Reasoning for (Un)Solvable Loops}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.4},
  URN =		{urn:nbn:de:0030-drops-185385},
  doi =		{10.4230/LIPIcs.MFCS.2023.4},
  annote =	{Keywords: Symbolic Computation, Formal Methods, Loop Analysis, Polynomial Invariants}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2020
LIPIcs, Volume 171, CONCUR 2020, Complete Volume

Authors: Igor Konnov and Laura Kovács

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
LIPIcs, Volume 171, CONCUR 2020, Complete Volume
Cite as

31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 1-984, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Proceedings{konnov_et_al:LIPIcs.CONCUR.2020,
  title =	{{LIPIcs, Volume 171, CONCUR 2020, Complete Volume}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{1--984},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020},
  URN =		{urn:nbn:de:0030-drops-128115},
  doi =		{10.4230/LIPIcs.CONCUR.2020},
  annote =	{Keywords: LIPIcs, Volume 171, CONCUR 2020, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2020.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Igor Konnov and Laura Kovács

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{konnov_et_al:LIPIcs.CONCUR.2020.0,
  author =	{Konnov, Igor and Kov\'{a}cs, Laura},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.0},
  URN =		{urn:nbn:de:0030-drops-128125},
  doi =		{10.4230/LIPIcs.CONCUR.2020.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2017.3
First-Order Interpolation and Grey Areas of Proofs (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
Interpolation is an important technique in computer aided verification and static analysis of programs. In particular, interpolants extracted from so-called local proofs are used in invariant generation and bounded model checking. An interpolant extracted from such a proof is a boolean combination of formulas occurring in the proof. In this talk we first describe a technique of generating and optimizing interpolants based on transformations of what we call the “grey area” of local proofs. Local changes in proofs can change the extracted interpolant. Our method can describe properties of extracted interpolants obtained by such proof changes as a pseudo-boolean constraint. By optimizing solutions of this constraint we also improve the extracted interpolants. Unlike many other interpolation techniques, our technique is very general and applies to arbitrary theories. Our approach is implemented in the theorem prover Vampire and evaluated on a large number of benchmarks coming from first-order theorem proving and bounded model checking using logic with equality, uninterpreted functions and linear integer arithmetic. Our experiments demonstrate the power of the new techniques: for example, it is not unusual that our proof transformation gives more than a tenfold reduction in the size of interpolants. While local proofs admit efficient interpolation algorithms, standard complete proof systems, such as superposition, for theories having the interpolation property are not necessarily complete for local proofs. In this talk we therefore also investigate interpolant extraction from non-local proofs in the superposition calculus and prove a number of general results about interpolant extraction and complexity of extracted interpolants. In particular, we prove that the number of quantifier alternations in first-order interpolants of formulas without quantifier alternations is unbounded. This result has far-reaching consequences for using local proofs as a foundation for interpolating proof systems - any such proof system should deal with formulas of arbitrary quantifier complexity.
Cite as

Laura Kovács. First-Order Interpolation and Grey Areas of Proofs (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.CSL.2017.3,
  author =	{Kov\'{a}cs, Laura},
  title =	{{First-Order Interpolation and Grey Areas of Proofs}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.3},
  URN =		{urn:nbn:de:0030-drops-76912},
  doi =		{10.4230/LIPIcs.CSL.2017.3},
  annote =	{Keywords: theorem proving, interpolation, proof transformations, constraint solving, program analysis}
}
Document
DOI: 10.4230/OASIcs.WCET.2013.53
The Auspicious Couple: Symbolic Execution and WCET Analysis

Authors: Armin Biere, Jens Knoop, Laura Kovács, and Jakob Zwirchmayr

Published in: OASIcs, Volume 30, 13th International Workshop on Worst-Case Execution Time Analysis (2013)

Abstract
We have recently shown that symbolic execution together with the implicit path enumeration technique can successfully be applied in the Worst-Case Execution Time (WCET) analysis of programs. Symbolic execution offers a precise framework for program analysis and tracks complex program properties by analyzing single program paths in isolation. This path-wise program exploration of symbolic execution is, however, computationally expensive, which often prevents full symbolic analysis of larger applications: the number of paths in a program increases exponentially with the number of conditionals, a situation denoted as the path explosion problem. Therefore, for applying symbolic execution in the timing analysis of programs, we propose to use WCET analysis as a guidance for symbolic execution in order to avoid full symbolic coverage of the program. By focusing only on paths or program fragments that are relevant for WCET analysis, we keep the computational costs of symbolic execution low. Our WCET analysis also profits from the precise results derived via symbolic execution. In this article we describe how use-cases of symbolic execution are materialized in the r-TuBound toolchain and present new applications of WCET-guided symbolic execution for WCET analysis. The new applications of selective symbolic execution are based on reducing the effort of symbolic analysis by focusing only on relevant program fragments. By using partial symbolic program coverage obtained by selective symbolic execution, we improve the WCET analysis and keep the effort for symbolic execution low.
Cite as

Armin Biere, Jens Knoop, Laura Kovács, and Jakob Zwirchmayr. The Auspicious Couple: Symbolic Execution and WCET Analysis. In 13th International Workshop on Worst-Case Execution Time Analysis. Open Access Series in Informatics (OASIcs), Volume 30, pp. 53-63, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{biere_et_al:OASIcs.WCET.2013.53,
  author =	{Biere, Armin and Knoop, Jens and Kov\'{a}cs, Laura and Zwirchmayr, Jakob},
  title =	{{The Auspicious Couple: Symbolic Execution and WCET Analysis}},
  booktitle =	{13th International Workshop on Worst-Case Execution Time Analysis},
  pages =	{53--63},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-54-5},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{30},
  editor =	{Maiza, Claire},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2013.53},
  URN =		{urn:nbn:de:0030-drops-41225},
  doi =		{10.4230/OASIcs.WCET.2013.53},
  annote =	{Keywords: WCET analysis, Symbolic execution, WCET refinement, Flow Facts}
}
Document
DOI: 10.4230/DagRep.2.11.45
Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461)

Authors: Nikolaj Bjorner, Krishnendu Chatterjee, Laura Kovacs, and Rupak M. Majumdar

Published in: Dagstuhl Reports, Volume 2, Issue 11 (2013)

Abstract
This report documents the program and the outcomes of the Dagstuhl Seminar 12461 "Games and Decisions for Rigorous Systems Engineering". The seminar brought together researchers working in rigorous software engineering, with a special focus on the interaction between synthesis and automated deduction. This event was the first seminar of this kind and a kickoff of a series of seminars organised on rigorous systems engineering. The theme of the seminar was close in spirit to many events that have been held over the last decades. The talks scheduled during the seminar naturally reflected fundamental research themes of the involved communities.
Cite as

Nikolaj Bjorner, Krishnendu Chatterjee, Laura Kovacs, and Rupak M. Majumdar. Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). In Dagstuhl Reports, Volume 2, Issue 11, pp. 45-65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.2.11.45,
  author =	{Bjorner, Nikolaj and Chatterjee, Krishnendu and Kovacs, Laura and Majumdar, Rupak M.},
  title =	{{Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461)}},
  pages =	{45--65},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{11},
  editor =	{Bjorner, Nikolaj and Chatterjee, Krishnendu and Kovacs, Laura and Majumdar, Rupak M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.2.11.45},
  URN =		{urn:nbn:de:0030-drops-39092},
  doi =		{10.4230/DagRep.2.11.45},
  annote =	{Keywords: Systems Engineering, Software Verification, Reactive Synthesis, Automated Deduction}
}

Kovács, Laura

Document
DOI: 10.4230/LIPIcs.SAT.2024.9
Lazy Reimplication in Chronological Backtracking

Authors: Robin Coutelier, Mathias Fleury, and Laura Kovács

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose.
Cite as

Robin Coutelier, Mathias Fleury, and Laura Kovács. Lazy Reimplication in Chronological Backtracking. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{coutelier_et_al:LIPIcs.SAT.2024.9,
  author =	{Coutelier, Robin and Fleury, Mathias and Kov\'{a}cs, Laura},
  title =	{{Lazy Reimplication in Chronological Backtracking}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9},
  URN =		{urn:nbn:de:0030-drops-205313},
  doi =		{10.4230/LIPIcs.SAT.2024.9},
  annote =	{Keywords: Chronological Backtracking, CDCL, Invariants, Watcher Lists}
}
Document
DOI: 10.4230/LIPIcs.STACS.2024.41
Linear Loop Synthesis for Quadratic Invariants

Authors: S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.
Cite as

S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka. Linear Loop Synthesis for Quadratic Invariants. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 41:1-41:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hitarth_et_al:LIPIcs.STACS.2024.41,
  author =	{Hitarth, S. and Kenison, George and Kov\'{a}cs, Laura and Varonka, Anton},
  title =	{{Linear Loop Synthesis for Quadratic Invariants}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{41:1--41:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.41},
  URN =		{urn:nbn:de:0030-drops-197512},
  doi =		{10.4230/LIPIcs.STACS.2024.41},
  annote =	{Keywords: program synthesis, loop invariants, verification, Diophantine equations}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2023.4
Algebraic Reasoning for (Un)Solvable Loops (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Loop invariants describe valid program properties that hold before and after every loop iteration. As such, loop invariants are the workhorses in formalizing loop semantics and automating the formal analysis and verification of programs with loops. While automatically synthesizing loop invariants is, in general, an uncomputable problem, when considering only single-path loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus Müller-Olm and Helmut Seidl, 2004; Laura Kovács, 2008; Ehud Hrushovski et al., 2018]. Yet, already for loops with "only" polynomial updates, computing the strongest invariant has been an open challenge since 2004 [Markus Müller-Olm and Helmut Seidl, 2004]. In this invited talk, we first present computability results on polynomial invariant synthesis for restricted polynomial loops, called solvable loops [Rodríguez-Carbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closed-form solutions of algebraic recurrence equations that model the loop behaviour [Laura Kovács, 2008; Andreas Humenberger et al., 2017]. We also establish a technique for invariant synthesis for classes of loops that are not solvable, termed unsolvable loops [Daneshvar Amrollahi et al., 2022]. We next study the limits of computability in deriving the (strongest) polynomial invariants for arbitrary polynomial loops. We prove that computing the strongest polynomial invariant of arbitrary, single-path polynomial loops is very hard [Julian Müllner, 2023] - namely, it is at least as hard as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008], a prominent algebraic problem in the theory of linear recurrences. Going beyond single-path loops, we show that the strongest polynomial invariant is uncomputable already for multi-path polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].
Cite as

Laura Kovács. Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.MFCS.2023.4,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Algebraic Reasoning for (Un)Solvable Loops}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.4},
  URN =		{urn:nbn:de:0030-drops-185385},
  doi =		{10.4230/LIPIcs.MFCS.2023.4},
  annote =	{Keywords: Symbolic Computation, Formal Methods, Loop Analysis, Polynomial Invariants}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2020
LIPIcs, Volume 171, CONCUR 2020, Complete Volume

Authors: Igor Konnov and Laura Kovács

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
LIPIcs, Volume 171, CONCUR 2020, Complete Volume
Cite as

31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 1-984, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Proceedings{konnov_et_al:LIPIcs.CONCUR.2020,
  title =	{{LIPIcs, Volume 171, CONCUR 2020, Complete Volume}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{1--984},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020},
  URN =		{urn:nbn:de:0030-drops-128115},
  doi =		{10.4230/LIPIcs.CONCUR.2020},
  annote =	{Keywords: LIPIcs, Volume 171, CONCUR 2020, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2020.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Igor Konnov and Laura Kovács

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{konnov_et_al:LIPIcs.CONCUR.2020.0,
  author =	{Konnov, Igor and Kov\'{a}cs, Laura},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.0},
  URN =		{urn:nbn:de:0030-drops-128125},
  doi =		{10.4230/LIPIcs.CONCUR.2020.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2017.3
First-Order Interpolation and Grey Areas of Proofs (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
Interpolation is an important technique in computer aided verification and static analysis of programs. In particular, interpolants extracted from so-called local proofs are used in invariant generation and bounded model checking. An interpolant extracted from such a proof is a boolean combination of formulas occurring in the proof. In this talk we first describe a technique of generating and optimizing interpolants based on transformations of what we call the “grey area” of local proofs. Local changes in proofs can change the extracted interpolant. Our method can describe properties of extracted interpolants obtained by such proof changes as a pseudo-boolean constraint. By optimizing solutions of this constraint we also improve the extracted interpolants. Unlike many other interpolation techniques, our technique is very general and applies to arbitrary theories. Our approach is implemented in the theorem prover Vampire and evaluated on a large number of benchmarks coming from first-order theorem proving and bounded model checking using logic with equality, uninterpreted functions and linear integer arithmetic. Our experiments demonstrate the power of the new techniques: for example, it is not unusual that our proof transformation gives more than a tenfold reduction in the size of interpolants. While local proofs admit efficient interpolation algorithms, standard complete proof systems, such as superposition, for theories having the interpolation property are not necessarily complete for local proofs. In this talk we therefore also investigate interpolant extraction from non-local proofs in the superposition calculus and prove a number of general results about interpolant extraction and complexity of extracted interpolants. In particular, we prove that the number of quantifier alternations in first-order interpolants of formulas without quantifier alternations is unbounded. This result has far-reaching consequences for using local proofs as a foundation for interpolating proof systems - any such proof system should deal with formulas of arbitrary quantifier complexity.
Cite as

Laura Kovács. First-Order Interpolation and Grey Areas of Proofs (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.CSL.2017.3,
  author =	{Kov\'{a}cs, Laura},
  title =	{{First-Order Interpolation and Grey Areas of Proofs}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.3},
  URN =		{urn:nbn:de:0030-drops-76912},
  doi =		{10.4230/LIPIcs.CSL.2017.3},
  annote =	{Keywords: theorem proving, interpolation, proof transformations, constraint solving, program analysis}
}
Document
DOI: 10.4230/OASIcs.WCET.2013.53
The Auspicious Couple: Symbolic Execution and WCET Analysis

Authors: Armin Biere, Jens Knoop, Laura Kovács, and Jakob Zwirchmayr

Published in: OASIcs, Volume 30, 13th International Workshop on Worst-Case Execution Time Analysis (2013)

Abstract
We have recently shown that symbolic execution together with the implicit path enumeration technique can successfully be applied in the Worst-Case Execution Time (WCET) analysis of programs. Symbolic execution offers a precise framework for program analysis and tracks complex program properties by analyzing single program paths in isolation. This path-wise program exploration of symbolic execution is, however, computationally expensive, which often prevents full symbolic analysis of larger applications: the number of paths in a program increases exponentially with the number of conditionals, a situation denoted as the path explosion problem. Therefore, for applying symbolic execution in the timing analysis of programs, we propose to use WCET analysis as a guidance for symbolic execution in order to avoid full symbolic coverage of the program. By focusing only on paths or program fragments that are relevant for WCET analysis, we keep the computational costs of symbolic execution low. Our WCET analysis also profits from the precise results derived via symbolic execution. In this article we describe how use-cases of symbolic execution are materialized in the r-TuBound toolchain and present new applications of WCET-guided symbolic execution for WCET analysis. The new applications of selective symbolic execution are based on reducing the effort of symbolic analysis by focusing only on relevant program fragments. By using partial symbolic program coverage obtained by selective symbolic execution, we improve the WCET analysis and keep the effort for symbolic execution low.
Cite as

Armin Biere, Jens Knoop, Laura Kovács, and Jakob Zwirchmayr. The Auspicious Couple: Symbolic Execution and WCET Analysis. In 13th International Workshop on Worst-Case Execution Time Analysis. Open Access Series in Informatics (OASIcs), Volume 30, pp. 53-63, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{biere_et_al:OASIcs.WCET.2013.53,
  author =	{Biere, Armin and Knoop, Jens and Kov\'{a}cs, Laura and Zwirchmayr, Jakob},
  title =	{{The Auspicious Couple: Symbolic Execution and WCET Analysis}},
  booktitle =	{13th International Workshop on Worst-Case Execution Time Analysis},
  pages =	{53--63},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-54-5},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{30},
  editor =	{Maiza, Claire},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2013.53},
  URN =		{urn:nbn:de:0030-drops-41225},
  doi =		{10.4230/OASIcs.WCET.2013.53},
  annote =	{Keywords: WCET analysis, Symbolic execution, WCET refinement, Flow Facts}
}
Document
DOI: 10.4230/DagRep.2.11.45
Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461)

Authors: Nikolaj Bjorner, Krishnendu Chatterjee, Laura Kovacs, and Rupak M. Majumdar

Published in: Dagstuhl Reports, Volume 2, Issue 11 (2013)

Abstract
This report documents the program and the outcomes of the Dagstuhl Seminar 12461 "Games and Decisions for Rigorous Systems Engineering". The seminar brought together researchers working in rigorous software engineering, with a special focus on the interaction between synthesis and automated deduction. This event was the first seminar of this kind and a kickoff of a series of seminars organised on rigorous systems engineering. The theme of the seminar was close in spirit to many events that have been held over the last decades. The talks scheduled during the seminar naturally reflected fundamental research themes of the involved communities.
Cite as

Nikolaj Bjorner, Krishnendu Chatterjee, Laura Kovacs, and Rupak M. Majumdar. Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). In Dagstuhl Reports, Volume 2, Issue 11, pp. 45-65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.2.11.45,
  author =	{Bjorner, Nikolaj and Chatterjee, Krishnendu and Kovacs, Laura and Majumdar, Rupak M.},
  title =	{{Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461)}},
  pages =	{45--65},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{11},
  editor =	{Bjorner, Nikolaj and Chatterjee, Krishnendu and Kovacs, Laura and Majumdar, Rupak M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.2.11.45},
  URN =		{urn:nbn:de:0030-drops-39092},
  doi =		{10.4230/DagRep.2.11.45},
  annote =	{Keywords: Systems Engineering, Software Verification, Reactive Synthesis, Automated Deduction}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact