| 2026 | FSCD | Saturation-Guided Inductive Synthesis (Invited Talk). | Laura Kovcs |
| 2026 | IJCAR | Completeness of Synthesis Under Realizability Assumptions Using Superposition. | Mrton Hajd, Petra Hozzov, Laura Kovcs, Eva Maria Wagner |
| 2026 | ITP | Lean on Vampire Proofs (Short Paper). | Jonas Bodingbauer, Mrton Hajd, Laura Kovcs, Axel Polaczek, Michael Rawson |
| 2026 | STACS | Moments in Time: Algebraic Analysis for Solvable Loops (Invited Talk). | Laura Kovcs |
| 2026 | SAT | Generalizing CDCL with Graph Backtracking. | Robin Coutelier, Thomas Hader, Laura Kovcs |
| 2026 | SAT | SAT in Saturation: A Satisfied Match (Invited Talk). | Laura Kovcs |
| 2025 | CADE | Term Ordering Diagrams. | Mrton Hajd, Robin Coutelier, Laura Kovcs, Andrei Voronkov |
| 2025 | CADE | Partial Redundancy in Saturation. | Mrton Hajd, Laura Kovcs, Andrei Voronkov |
| 2025 | CAV | The Vampire Diary. | Filip Brtek, Ahmed Bhayat, Robin Coutelier, Mrton Hajd, Matthias Hetzenberger, Petra Hozzov, Laura Kovcs, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov |
| 2025 | IFM | Game Modeling of Blockchain Protocols. | Sophie Rain, Anja Petkovic Komel, Michael Rawson, Laura Kovcs |
| 2025 | TABLEAUX | Finding Connections via Satisfiability Solving. | Clemens Eisenhofer, Michael Rawson, Laura Kovcs |
| 2025 | TABLEAUX | On Solving String Equations via Powers and Parikh Images. | Clemens Eisenhofer, Theodor Seiser, Nikolaj S. Bjrner, Laura Kovcs |
| 2025 | TABLEAUX | Constraint Learning for Non-confluent Proof Search. | Michael Rawson, Clemens Eisenhofer, Laura Kovcs |
| 2024 | IJCAR | MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). | Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stphane Graham-Lengrand, Laura Kovcs |
| 2024 | IJCAR | Reducibility Constraints in Superposition. | Mrton Hajd, Laura Kovcs, Michael Rawson, Andrei Voronkov |
| 2024 | IJCAR | Synthesis of Recursive Programs in Saturation. | Petra Hozzov, Daneshvar Amrollahi, Mrton Hajd, Laura Kovcs, Andrei Voronkov, Eva Maria Wagner |
| 2024 | IJCAR | Induction in Saturation. | Laura Kovcs, Petra Hozzov, Mrton Hajd, Andrei Voronkov |
| 2024 | LPAR | Saturating Sorting without Sorts. | Pamina Georgiou, Mrton Hajd, Laura Kovcs |
| 2024 | LPAR | Rewriting and Inductive Reasoning. | Mrton Hajd, Laura Kovcs, Michael Rawson |
| 2024 | LPAR | Scaling CheckMate for Game-Theoretic Security. | Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovcs, Michael Rawson |
| 2024 | LPAR | VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. | Johannes Schoisswohl, Laura Kovcs, Konstantin Korovin |
| 2024 | SP | CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. | Simon Jeanteur, Laura Kovcs, Matteo Maffei, Michael Rawson |
| 2024 | STACS | Linear Loop Synthesis for Quadratic Invariants. | S. Hitarth, George Kenison, Laura Kovcs, Anton Varonka |
| 2024 | SAT | Lazy Reimplication in Chronological Backtracking. | Robin Coutelier, Mathias Fleury, Laura Kovcs |
| 2023 | CADE | SAT-Based Subsumption Resolution. | Robin Coutelier, Laura Kovcs, Michael Rawson, Jakob Rath |
| 2023 | CADE | Program Synthesis in Saturation. | Petra Hozzov, Laura Kovcs, Chase Norman, Andrei Voronkov |
| 2023 | CCS | CheckMate: Automated Game-Theoretic Security Reasoning. | Lea Salome Brugger, Laura Kovcs, Anja Petkovic Komel, Sophie Rain, Michael Rawson |
| 2023 | FM | Symbolic Computation in Automated Program Reasoning. | Laura Kovcs |
| 2023 | IFM | Automated Sensitivity Analysis for Probabilistic Loops. | Marcel Moosbrugger, Julian Mllner, Laura Kovcs |
| 2023 | ISSAC | From Polynomial Invariants to Linear Loops. | George Kenison, Laura Kovcs, Anton Varonka |
| 2023 | ISSAC | Algebra-Based Loop Analysis. | Laura Kovcs |
| 2023 | LPAR | Refining Unification with Abstraction. | Ahmed Bhayat, Konstantin Korovin, Laura Kovcs, Johannes Schoisswohl |
| 2023 | LPAR | SMT Solving over Finite Field Arithmetic. | Thomas Hader, Daniela Kaufmann, Laura Kovcs |
| 2023 | MFCS | Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). | Laura Kovcs |
| 2023 | TABLEAUX | Non-Classical Logics in Satisfiability Modulo Theories. | Clemens Eisenhofer, Ruba Alassaf, Michael Rawson, Laura Kovcs |
| 2023 | TACAS | ALASCA: Reasoning in Quantified Linear Arithmetic. | Konstantin Korovin, Laura Kovcs, Giles Reger, Johannes Schoisswohl, Andrei Voronkov |
| 2023 | VMCAI | Satisfiability Modulo Custom Theories in Z3. | Nikolaj S. Bjrner, Clemens Eisenhofer, Laura Kovcs |
| 2022 | FMCAD | The Rapid Software Verification Framework. | Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovcs, Giles Reger |
| 2022 | FMCAD | First-Order Subsumption via SAT Solving. | Jakob Rath, Armin Biere, Laura Kovcs |
| 2022 | SAS | Solving Invariant Generation for Unsolvable Loops. | Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovcs, Marcel Moosbrugger, Miroslav Stankovic |
| 2021 | CADE | Integer Induction in Saturation. | Petra Hozzov, Laura Kovcs, Andrei Voronkov |
| 2021 | CAV | Summing up Smart Transitions. | Neta Elad, Sophie Rain, Neil Immerman, Laura Kovcs, Mooly Sagiv |
| 2021 | ESOP | Automated Termination Analysis of Polynomial Probabilistic Programs. | Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovcs |
| 2021 | FM | The Probabilistic Termination Tool Amber. | Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovcs |
| 2021 | FMCAD | Induction with Recursive Definitions in Superposition. | Mrton Hajd, Petra Hozzov, Laura Kovcs, Andrei Voronkov |
| 2021 | VMCAI | Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). | Andreas Humenberger, Laura Kovcs |
| 2020 | CADE | Subsumption Demodulation in First-Order Theorem Proving. | Bernhard Gleiss, Laura Kovcs, Jakob Rath |
| 2020 | FMCAD | Trace Logic for Inductive Loop Reasoning. | Pamina Georgiou, Bernhard Gleiss, Laura Kovcs |
| 2020 | ICTAC | Analysis of Bayesian Networks via Prob-Solvable Loops. | Ezio Bartocci, Laura Kovcs, Miroslav Stankovic |
| 2020 | IFM | Algebra-Based Loop Synthesis. | Andreas Humenberger, Nikolaj S. Bjrner, Laura Kovcs |
| 2020 | TACAS | Mora - Automatic Generation of Moment-Based Invariants. | Ezio Bartocci, Laura Kovcs, Miroslav Stankovic |
| 2019 | ATVA | Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. | Ezio Bartocci, Laura Kovcs, Miroslav Stankovic |
| 2019 | FMCAD | Verifying Relational Properties using Trace Logic. | Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovcs, Matteo Maffei |
| 2019 | IFM | Interactive Visualization of Saturation Attempts in Vampire. | Bernhard Gleiss, Laura Kovcs, Lena Schnedlitz |
| 2019 | SYNASC | Superposition Reasoning about Quantified Bitvector Formulas. | David Damestani, Laura Kovcs, Martin Suda |
| 2019 | SYNASC | Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. | Gergely Kovsznai, Krisztin Gajdr, Laura Kovcs |
| 2018 | CADE | A FOOLish Encoding of the Next State Relations of Imperative Programs. | Evgenii Kotelnikov, Laura Kovcs, Andrei Voronkov |
| 2018 | LPAR | Loop Analysis by Quantification over Iterations. | Bernhard Gleiss, Laura Kovcs, Simon Robillard |
| 2018 | VMCAI | Invariant Generation for Multi-Path Loops with Polynomial Assignments. | Andreas Humenberger, Maximilian Jaroschek, Laura Kovcs |
| 2017 | CADE | Splitting Proofs for Interpolation. | Bernhard Gleiss, Laura Kovcs, Martin Suda |
| 2017 | CSL | First-Order Interpolation and Grey Areas of Proofs (Invited Talk). | Laura Kovcs |
| 2017 | ISSAC | Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. | Andreas Humenberger, Maximilian Jaroschek, Laura Kovcs |
| 2017 | LPAR | First-Order Interpolation and Interpolating Proof Systems. | Laura Kovcs, Andrei Voronkov |
| 2017 | POPL | Coming to terms with quantified reasoning. | Laura Kovcs, Simon Robillard, Andrei Voronkov |
| 2016 | CADE | Theory-Specific Reasoning about Loops with Arrays using Vampire. | Yuting Chen, Laura Kovcs, Simon Robillard |
| 2016 | CPP | The vampire and the FOOL. | Evgenii Kotelnikov, Laura Kovcs, Giles Reger, Andrei Voronkov |
| 2016 | IFM | Symbolic Computation and Automated Reasoning for Program Analysis. | Laura Kovcs |
| 2015 | CADE | Reasoning About Loops Using Vampire. | Laura Kovcs, Simon Robillard |
| 2015 | ESOP | Segment Abstraction for Worst-Case Execution Time Analysis. | Pavol Cern, Thomas A. Henzinger, Laura Kovcs, Arjun Radhakrishna, Jakob Zwirchmayr |
| 2015 | LPAR | Reasoning About Loops Using Vampire in KeY. | Wolfgang Ahrendt, Laura Kovcs, Simon Robillard |
| 2014 | ATVA | Extensional Crisis and Proving Identity. | Ashutosh Gupta, Laura Kovcs, Bernhard Kragl, Andrei Voronkov |
| 2014 | CADE | SAT solving experiments in Vampire. | Armin Biere, Ioan Dragan, Laura Kovcs, Andrei Voronkov |
| 2013 | ATVA | SmacC: A Retargetable Symbolic Execution Engine. | Armin Biere, Jens Knoop, Laura Kovcs, Jakob Zwirchmayr |
| 2013 | CAV | First-Order Theorem Proving and Vampire. | Laura Kovcs, Andrei Voronkov |
| 2013 | LPAR | Tree Interpolation in Vampire. | Rgis Blanc, Ashutosh Gupta, Laura Kovcs, Bernhard Kragl |
| 2013 | RTNS | WCET squeezing: on-demand feasibility refinement for proven precise WCET-bounds. | Jens Knoop, Laura Kovcs, Jakob Zwirchmayr |
| 2013 | SYNASC | Bound Propagation for Arithmetic Reasoning in Vampire. | Ioan Dragan, Konstantin Korovin, Laura Kovcs, Andrei Voronkov |
| 2012 | APLAS | Vinter: A Vampire-Based Tool for Interpolation. | Krystof Hoder, Andreas Holzer, Laura Kovcs, Andrei Voronkov |
| 2012 | LPAR | r-TuBound: Loop Bounds for WCET Analysis (Tool Paper). | Jens Knoop, Laura Kovcs, Jakob Zwirchmayr |
| 2012 | POPL | Playing in the grey area of proofs. | Krystof Hoder, Laura Kovcs, Andrei Voronkov |
| 2012 | RTNS | FFX: a portable WCET annotation language. | Armelle Bonenfant, Hugues Cass, Marianne De Michiel, Jens Knoop, Laura Kovcs, Jakob Zwirchmayr |
| 2012 | SYNASC | Solving Robust Glucose-Insulin Control by Dixon Resultant Computations. | Laura Kovcs, Bla Palncz, Levente Kovcs |
| 2011 | CADE | On Transfinite Knuth-Bendix Orders. | Laura Kovcs, Georg Moser, Andrei Voronkov |
| 2011 | SYNASC | Symbol Elimination in Program Analysis. | Laura Kovcs |
| 2011 | TACAS | Invariant Generation in Vampire. | Krystof Hoder, Laura Kovcs, Andrei Voronkov |
| 2010 | CADE | Interpolation and Symbol Elimination in Vampire. | Krystof Hoder, Laura Kovcs, Andrei Voronkov |
| 2010 | LPAR | ABC: Algebraic Bound Computation for Loops. | Rgis Blanc, Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs |
| 2010 | LPAR | Aligators for Arrays (Tool Paper). | Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs, Andrey Rybalchenko |
| 2010 | VMCAI | Invariant and Type Inference for Matrices. | Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs, Andrei Voronkov |
| 2009 | CADE | Interpolation and Symbol Elimination. | Laura Kovcs, Andrei Voronkov |
| 2009 | FASE | Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. | Laura Kovcs, Andrei Voronkov |
| 2009 | SYNASC | Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. | Laura Kovcs, Andrei Voronkov |
| 2008 | CADE | Aligator: A Mathematica Package for Invariant Generation (System Description). | Laura Kovcs |
| 2008 | CSR | Invariant Generation for P-Solvable Loops with Assignments. | Laura Kovcs |
| 2008 | LPAR | Valigator: A Verification Tool with Bound and Invariant Generation. | Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs |
| 2008 | TACAS | Reasoning Algebraically About P-Solvable Loops. | Laura Kovcs |
| 2006 | ISoLA | Combining Logic and Algebraic Techniques for Program Verification in Theorema. | Laura Kovcs, Nikolaj Popov, Tudor Jebelean |
| 2004 | ISoLA | Experimental Program Verification in the Theorema System. | Tudor Jebelean, Laura Kovcs, Nikolaj Popov |