Experimental Program Verification in the Theorema System. - Tudor Jebelean; Laura Kovács; Nikolaj Popov (ISoLA (Preliminary proceedings), 2004)

An Algorithm for Automated Generation of Invariants for Loops with Conditionals. - Laura Ildikó Kovács; Tudor Jebelean (SYNASC, 2005)

Combining Logic and Algebraic Techniques for Program Verification in Theorema. - Laura Kovács; Nikolaj Popov; Tudor Jebelean (ISoLA, 2006)

Theorema: Towards computer-aided mathematical theory exploration. - Bruno Buchberger; Adrian Craciun; Tudor Jebelean; Laura Kovács; Temur Kutsia; Koji Nakagawa; Florina Piroi; Nikolaj Popov; Judit Robu; Markus Rosenkranz; Wolfgang Windsteiger (J. Appl. Log., 2006)

Aligator: A Mathematica Package for Invariant Generation (System Description). - Laura Kovács (IJCAR, 2008)

Invariant Generation for P-Solvable Loops with Assignments. - Laura Kovács (CSR, 2008)

Valigator: A Verification Tool with Bound and Invariant Generation. - Thomas A. Henzinger; Thibaud Hottelier; Laura Kovács (LPAR, 2008)

Reasoning Algebraically About P-Solvable Loops. - Laura Kovács (TACAS, 2008)

Interpolation and Symbol Elimination. - Laura Kovács; Andrei Voronkov (CADE, 2009)

A Complete Invariant Generation Approach for P-solvable Loops. - Laura Kovács (Ershov Memorial Conference, 2009)

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. - Laura Kovács; Andrei Voronkov (FASE, 2009)

Interpolation and Symbol Elimination in Vampire. - Krystof Hoder; Laura Kovács; Andrei Voronkov (IJCAR, 2010)

ABC: Algebraic Bound Computation for Loops. - Régis Blanc; Thomas A. Henzinger; Thibaud Hottelier; Laura Kovács (LPAR (Dakar), 2010)

Aligators for Arrays (Tool Paper). - Thomas A. Henzinger; Thibaud Hottelier; Laura Kovács; Andrey Rybalchenko (LPAR (Yogyakarta), 2010)

Invariant and Type Inference for Matrices. - Thomas A. Henzinger; Thibaud Hottelier; Laura Kovács; Andrei Voronkov (VMCAI, 2010)

Introduction. - Martin Giese; Andrew Ireland; Laura Kovács (J. Symb. Comput., 2010)

On Transfinite Knuth-Bendix Orders. - Laura Kovács; Georg Moser; Andrei Voronkov (CADE, 2011)

Symbolic Loop Bound Computation for WCET Analysis. - Jens Knoop; Laura Kovács; Jakob Zwirchmayr (Ershov Memorial Conference, 2011)

Case Studies on Invariant Generation Using a Saturation Theorem Prover. - Krystof Hoder; Laura Kovács; Andrei Voronkov (MICAI (1), 2011)

Symbol Elimination in Program Analysis. - Laura Kovács (SYNASC, 2011)

Invariant Generation in Vampire. - Krystof Hoder; Laura Kovács; Andrei Voronkov (TACAS, 2011)

Vinter: A Vampire-Based Tool for Interpolation. - Krystof Hoder; Andreas Holzer; Laura Kovács; Andrei Voronkov (APLAS, 2012)

r-TuBound: Loop Bounds for WCET Analysis (Tool Paper). - Jens Knoop; Laura Kovács; Jakob Zwirchmayr (LPAR, 2012)

Playing in the grey area of proofs. - Krystof Hoder; Laura Kovács; Andrei Voronkov (POPL, 2012)

FFX: a portable WCET annotation language. - Armelle Bonenfant; Hugues Cassé; Marianne De Michiel; Jens Knoop; Laura Kovács; Jakob Zwirchmayr (RTNS, 2012)

Solving Robust Glucose-Insulin Control by Dixon Resultant Computations. - Laura Kovács; Béla Paláncz; Levente Kovács (SYNASC, 2012)

Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). - Nikolaj S. Bjørner; Krishnendu Chatterjee; Laura Kovács; Rupak Majumdar (Dagstuhl Reports, 2012)

Special issue on Automated Specification and Verification of Web Systems. - Laura Kovács; Temur Kutsia (J. Appl. Log., 2012)

Foreword. - Nikolaj S. Bjørner; Laura Kovács (J. Symb. Comput., 2012)

SmacC: A Retargetable Symbolic Execution Engine. - Armin Biere; Jens Knoop; Laura Kovács; Jakob Zwirchmayr (ATVA, 2013)

First-Order Theorem Proving and Vampire. - Laura Kovács; Andrei Voronkov (CAV, 2013)

Tree Interpolation in Vampire. - Régis Blanc; Ashutosh Gupta; Laura Kovács; Bernhard Kragl (LPAR, 2013)

The Inverse Method for Many-Valued Logics. - Laura Kovács; Andrei Mantsivoda; Andrei Voronkov (MICAI (1), 2013)

A Parametric Interpolation Framework for First-Order Theories. - Laura Kovács; Simone Fulvio Rollini; Natasha Sharygina (MICAI (1), 2013)

WCET squeezing: on-demand feasibility refinement for proven precise WCET-bounds. - Jens Knoop; Laura Kovács; Jakob Zwirchmayr (RTNS, 2013)

Bound Propagation for Arithmetic Reasoning in Vampire. - Ioan Dragan; Konstantin Korovin; Laura Kovács; Andrei Voronkov (SYNASC, 2013)

The Auspicious Couple: Symbolic Execution and WCET Analysis. - Armin Biere; Jens Knoop; Laura Kovács; Jakob Zwirchmayr (WCET, 2013)

Special issue on Automated Specification and Verification of Web Systems. - Laura Kovács; Rosario Pugliese; Josep Silva; Francesco Tiezzi 001 (J. Log. Algebraic Methods Program., 2013)

Extensional Crisis and Proving Identity. - Ashutosh Gupta; Laura Kovács; Bernhard Kragl; Andrei Voronkov (ATVA, 2014)

SAT solving experiments in Vampire. - Armin Biere; Ioan Dragan; Laura Kovács; Andrei Voronkov (Vampire Workshop, 2014)

Lingva: Generating and Proving Program Properties Using Symbol Elimination. - Ioan Dragan; Laura Kovács (Ershov Memorial Conference, 2014)

Supervisory Control of Discrete-Event Systems via IC3. - Mohammad Reza Shoaei; Laura Kovács; Bengt Lennartson (Haifa Verification Conference, 2014)

Experimenting with SAT Solvers in Vampire. - Armin Biere; Ioan Dragan; Laura Kovács; Andrei Voronkov (MICAI (1), 2014)

Symbol Elimination for Automated Generation of Program Properties. - Laura Kovács (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014)

Reasoning About Loops Using Vampire. - Laura Kovács; Simon Robillard (Vampire Workshop, 2015)

Segment Abstraction for Worst-Case Execution Time Analysis. - Pavol Cerný; Thomas A. Henzinger; Laura Kovács; Arjun Radhakrishna; Jakob Zwirchmayr (ESOP, 2015)

Reasoning About Loops Using Vampire in KeY. - Wolfgang Ahrendt; Laura Kovács; Simon Robillard (LPAR, 2015)

A First Class Boolean Sort in First-Order Theorem Proving and TPTP. - Evgenii Kotelnikov; Laura Kovács; Andrei Voronkov (CICM, 2015)

Special issue on symbolic computation in software science. - Adel Bouhoula; Bruno Buchberger; Laura Kovács; Temur Kutsia (J. Symb. Comput., 2015)

Theory-Specific Reasoning about Loops with Arrays using Vampire. - Yuting Chen; Laura Kovács; Simon Robillard (Vampire@IJCAR, 2016)

The vampire and the FOOL. - Evgenii Kotelnikov; Laura Kovács; Giles Reger; Andrei Voronkov (CPP, 2016)

A Clausal Normal Form Translation for FOOL. - Evgenii Kotelnikov; Laura Kovács; Martin Suda 001; Andrei Voronkov (GCAI, 2016)

Symbolic Computation and Automated Reasoning for Program Analysis. - Laura Kovács (IFM, 2016)

Splitting Proofs for Interpolation. - Bernhard Gleiss; Laura Kovács; Martin Suda 001 (CADE, 2017)

First-Order Interpolation and Grey Areas of Proofs (Invited Talk). - Laura Kovács (CSL, 2017)

A Supervisory Control Algorithm Based on Property-Directed Reachability. - Koen Claessen; Jonatan Kilhamn; Laura Kovács; Bengt Lennartson (Haifa Verification Conference, 2017)

Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. - Andreas Humenberger; Maximilian Jaroschek; Laura Kovács (ISSAC, 2017)

First-Order Interpolation and Interpolating Proof Systems. - Laura Kovács; Andrei Voronkov (LPAR, 2017)

Coming to terms with quantified reasoning. - Laura Kovács; Simon Robillard; Andrei Voronkov (POPL, 2017)

Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution. - Jens Knoop; Laura Kovács; Jakob Zwirchmayr (J. Symb. Comput., 2017)

A FOOLish Encoding of the Next State Relations of Imperative Programs. - Evgenii Kotelnikov; Laura Kovács; Andrei Voronkov (IJCAR, 2018)

Loop Analysis by Quantification over Iterations. - Bernhard Gleiss; Laura Kovács; Simon Robillard (LPAR, 2018)

Aligator.jl - A Julia Package for Loop Invariant Generation. - Andreas Humenberger; Maximilian Jaroschek; Laura Kovács (CICM, 2018)

Invariant Generation for Multi-Path Loops with Polynomial Assignments. - Andreas Humenberger; Maximilian Jaroschek; Laura Kovács (VMCAI, 2018)

Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. - Ezio Bartocci; Laura Kovács; Miroslav Stankovic (ATVA, 2019)

Verifying Relational Properties using Trace Logic. - Gilles Barthe; Renate Eilers; Pamina Georgiou; Bernhard Gleiss; Laura Kovács; Matteo Maffei (FMCAD, 2019)

Interactive Visualization of Saturation Attempts in Vampire. - Bernhard Gleiss; Laura Kovács; Lena Schnedlitz (IFM, 2019)

Superposition Reasoning about Quantified Bitvector Formulas. - David Damestani; Laura Kovács; Martin Suda 001 (SYNASC, 2019)

Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. - Gergely Kovásznai; Krisztián Gajdár; Laura Kovács (SYNASC, 2019)

Foreword - Formalization of geometry, automated and interactive geometric reasoning. - Pascal Schreck; Tetsuo Ida; Laura Kovács (Ann. Math. Artif. Intell., 2019)

Foreword. - James H. Davenport; Laura Kovács; Daniela Zaharie (Math. Comput. Sci., 2019)

Subsumption Demodulation in First-Order Theorem Proving. - Bernhard Gleiss; Laura Kovács; Jakob Rath (IJCAR (1), 2020)

Trace Logic for Inductive Loop Reasoning. - Pamina Georgiou; Bernhard Gleiss; Laura Kovács (FMCAD, 2020)

Analysis of Bayesian Networks via Prob-Solvable Loops. - Ezio Bartocci; Laura Kovács; Miroslav Stankovic (ICTAC, 2020)

Algebra-Based Loop Synthesis. - Andreas Humenberger; Nikolaj S. Bjørner; Laura Kovács (IFM, 2020)

Induction with Generalization in Superposition Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Johannes Schoisswohl; Andrei Voronkov (CICM, 2020)

Formalizing Graph Trail Properties in Isabelle/HOL. - Laura Kovács; Hanna Lachnitt; Stefan Szeider (CICM, 2020)

Mora - Automatic Generation of Moment-Based Invariants. - Ezio Bartocci; Laura Kovács; Miroslav Stankovic (TACAS (1), 2020)

Algebra-based Loop Synthesis. - Andreas Humenberger; Laura Kovács (CoRR, 2020)

Integer Induction in Saturation. - Petra Hozzová; Laura Kovács; Andrei Voronkov (CADE, 2021)

Summing up Smart Transitions. - Neta Elad; Sophie Rain; Neil Immerman; Laura Kovács; Mooly Sagiv (CAV (1), 2021)

Automated Termination Analysis of Polynomial Probabilistic Programs. - Marcel Moosbrugger; Ezio Bartocci; Joost-Pieter Katoen; Laura Kovács (ESOP, 2021)

Induction with Recursive Definitions in Superposition. - Márton Hajdú; Petra Hozzová; Laura Kovács; Andrei Voronkov (FMCAD, 2021)

Inductive Benchmarks for Automated Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Johannes Schoisswohl; Andrei Voronkov (CICM, 2021)

Automated Generation of Exam Sheets for Automated Deduction. - Petra Hozzová; Laura Kovács; Jakob Rath (CICM, 2021)

Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). - Andreas Humenberger; Laura Kovács (VMCAI, 2021)

Automating Induction by Reflection. - Johannes Schoisswohl; Laura Kovács (LFMTP, 2021)

Getting Saturated with Induction. - Márton Hajdú; Petra Hozzová; Laura Kovács; Giles Reger; Andrei Voronkov (Principles of Systems Design, 2022)

The Rapid Software Verification Framework. - Pamina Georgiou; Bernhard Gleiss; Ahmed Bhayat; Michael Rawson 001; Laura Kovács; Giles Reger (FMCAD, 2022)

First-Order Subsumption via SAT Solving. - Jakob Rath; Armin Biere; Laura Kovács (FMCAD, 2022)

Lemmaless Induction in Trace Logic. - Ahmed Bhayat; Pamina Georgiou; Clemens Eisenhofer; Laura Kovács; Giles Reger (CICM, 2022)

The Vampire Approach to Induction (short paper). - Márton Hajdú; Laura Kovács; Michael Rawson 001; Andrei Voronkov (PAAR@IJCAR, 2022)

Distribution Estimation for Probabilistic Loops. - Ahmad Karimi; Marcel Moosbrugger; Miroslav Stankovic; Laura Kovács; Ezio Bartocci; Efstathia Bura (QEST, 2022)

Solving Invariant Generation for Unsolvable Loops. - Daneshvar Amrollahi; Ezio Bartocci; George Kenison; Laura Kovács; Marcel Moosbrugger; Miroslav Stankovic (SAS, 2022)

User-Propagators for Custom Theories in SMT Solving. - Nikolaj S. Bjørner; Clemens Eisenhofer; Laura Kovács (SMT, 2022)

An SMT Approach for Solving Polynomials over Finite Fields. - Thomas Hader; Laura Kovács (SMT, 2022)

Algebra-Based Reasoning for Loop Synthesis. - Andreas Humenberger; Daneshvar Amrollahi; Nikolaj S. Bjørner; Laura Kovács (Formal Aspects Comput., 2022)

This is the moment for probabilistic loops. - Marcel Moosbrugger; Miroslav Stankovic; Ezio Bartocci; Laura Kovács (Proc. ACM Program. Lang., 2022)

Moment-based analysis of Bayesian network properties. - Miroslav Stankovic; Ezio Bartocci; Laura Kovács (Theor. Comput. Sci., 2022)

This is the Moment for Probabilistic Loops - Artifact (Polar). - Marcel Moosbrugger; Miroslav Stankovic; Ezio Bartocci; Laura Kovács (Zenodo, 2022)

This is the Moment for Probabilistic Loops - Artifact (Polar). - Marcel Moosbrugger; Miroslav Stankovic; Ezio Bartocci; Laura Kovács (Zenodo, 2022)

This is the Moment for Probabilistic Loops - Artifact (Polar). - Marcel Moosbrugger; Miroslav Stankovic; Ezio Bartocci; Laura Kovács (Zenodo, 2022)

This is the Moment for Probabilistic Loops - Artifact (Polar). - Marcel Moosbrugger; Miroslav Stankovic; Ezio Bartocci; Laura Kovács (Zenodo, 2022)

The probabilistic termination tool amber. - Marcel Moosbrugger; Ezio Bartocci; Joost-Pieter Katoen; Laura Kovács (Formal Methods Syst. Des., 2022)

What Else is Undecidable About Loops? - Laura Kovács; Anton Varonka (RAMiCS, 2023)

Embedding the Connection Calculus in Satisfiability Modulo Theories. - Clemens Eisenhofer; Laura Kovács; Michael Rawson 001 (AReCCa@TABLEAUX, 2023)

SAT-Based Subsumption Resolution. - Robin Coutelier; Laura Kovács; Michael Rawson 001; Jakob Rath (CADE, 2023)

Program Synthesis in Saturation. - Petra Hozzová; Laura Kovács; Chase Norman; Andrei Voronkov (CADE, 2023)

CheckMate: Automated Game-Theoretic Security Reasoning. - Lea Salome Brugger; Laura Kovács; Anja Petkovic Komel; Sophie Rain; Michael Rawson 001 (CCS, 2023)

Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. - Sophie Rain; Georgia Avarikioti; Laura Kovács; Matteo Maffei (CSF, 2023)

Symbolic Computation in Automated Program Reasoning. - Laura Kovács (FM, 2023)

Automated Sensitivity Analysis for Probabilistic Loops. - Marcel Moosbrugger; Julian Müllner; Laura Kovács (iFM, 2023)

From Polynomial Invariants to Linear Loops. - George Kenison; Laura Kovács; Anton Varonka (ISSAC, 2023)

Algebra-Based Loop Analysis. - Laura Kovács (ISSAC, 2023)

Reshaping Unplugged Computer Science Workshops for Primary School Education. - Martina Landman; Sophie Rain; Laura Kovács; Gerald Futschek (ISSEP, 2023)

Refining Unification with Abstraction. - Ahmed Bhayat; Konstantin Korovin; Laura Kovács; Johannes Schoisswohl (LPAR, 2023)

SMT Solving over Finite Field Arithmetic. - Thomas Hader; Daniela Kaufmann; Laura Kovács (LPAR, 2023)

Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). - Laura Kovács (MFCS, 2023)

Non-Classical Logics in Satisfiability Modulo Theories. - Clemens Eisenhofer; Ruba Alassaf; Michael Rawson 001; Laura Kovács (TABLEAUX, 2023)

ALASCA: Reasoning in Quantified Linear Arithmetic. - Konstantin Korovin; Laura Kovács; Giles Reger; Johannes Schoisswohl; Andrei Voronkov (TACAS (1), 2023)

Satisfiability Modulo Custom Theories in Z3. - Nikolaj S. Bjørner; Clemens Eisenhofer; Laura Kovács (VMCAI, 2023)

Lonely Points in Simplices. - Maximilian Jaroschek; Manuel Kauers; Laura Kovács (Discret. Comput. Geom., 2023)

Polar: An Algebraic Analyzer for (Probabilistic) Loops. - Marcel Moosbrugger; Julian Müllner; Ezio Bartocci; Laura Kovács (Principles of Verification (1), 2024)

MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). - Thomas Hader; Daniela Kaufmann; Ahmed Irfan; Stéphane Graham-Lengrand; Laura Kovács (IJCAR (1), 2024)

Reducibility Constraints in Superposition. - Márton Hajdú; Laura Kovács; Michael Rawson 001; Andrei Voronkov (IJCAR (1), 2024)

Synthesis of Recursive Programs in Saturation. - Petra Hozzová; Daneshvar Amrollahi; Márton Hajdú; Laura Kovács; Andrei Voronkov; Eva Maria Wagner (IJCAR (1), 2024)

Induction in Saturation. - Laura Kovács; Petra Hozzová; Márton Hajdú; Andrei Voronkov (IJCAR (1), 2024)

Saturating Sorting without Sorts. - Pamina Georgiou; Márton Hajdú; Laura Kovács (LPAR, 2024)

Rewriting and Inductive Reasoning. - Márton Hajdú; Laura Kovács; Michael Rawson 001 (LPAR, 2024)

Scaling CheckMate for Game-Theoretic Security. - Sophie Rain; Lea Salome Brugger; Anja Petkovic Komel; Laura Kovács; Michael Rawson 001 (LPAR, 2024)

VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. - Johannes Schoisswohl; Laura Kovács; Konstantin Korovin (LPAR, 2024)

Lazy Reimplication in Chronological Backtracking. - Robin Coutelier; Mathias Fleury; Laura Kovács (SAT, 2024)

Linear Loop Synthesis for Quadratic Invariants. - S. Hitarth; George Kenison; Laura Kovács; Anton Varonka (STACS, 2024)

PolySAT: Word-level Bit-vector Reasoning in Z3. - Jakob Rath; Clemens Eisenhofer; Daniela Kaufmann; Nikolaj S. Bjørner; Laura Kovács (VSTTE, 2024)

Spanning Matrices via Satisfiability Solving. - Clemens Eisenhofer; Michael Rawson 001; Laura Kovács (CoRR, 2024)

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver. - Thomas Hader; Daniela Kaufmann; Ahmed Irfan; Stéphane Graham-Lengrand; Laura Kovács (CoRR, 2024)

Scaling Game-Theoretic Security Reasoning. - Sophie Rain; Lea Salome Brugger; Anja Petkovic Komel; Laura Kovács; Michael Rawson 001 (CoRR, 2024)

SAT Solving for Variants of First-Order Subsumption. - Robin Coutelier; Jakob Rath; Michael Rawson 001; Armin Biere; Laura Kovács (CoRR, 2024)

SAT and Interactions (Dagstuhl Seminar 24421). - Olaf Beyersdorff; Laura Kovács; Meena Mahajan; Martina Seidl; Kaspar Kasche (Dagstuhl Reports, 2024)

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. - Simon Jeanteur; Laura Kovács; Matteo Maffei; Michael Rawson 001 (IACR Cryptol. ePrint Arch., 2024)

Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. - Julian Müllner; Marcel Moosbrugger; Laura Kovács (Proc. ACM Program. Lang., 2024)

Term Ordering Diagrams. - Márton Hajdú; Robin Coutelier; Laura Kovács; Andrei Voronkov (CADE, 2025)

Partial Redundancy in Saturation. - Márton Hajdú; Laura Kovács; Andrei Voronkov (CADE, 2025)

The Vampire Diary. - Filip Bártek; Ahmed Bhayat; Robin Coutelier; Márton Hajdú; Matthias Hetzenberger; Petra Hozzová; Laura Kovács; Jakob Rath; Michael Rawson 001; Giles Reger; Martin Suda 001; Johannes Schoisswohl; et al. (CAV (3), 2025)

Llm-Based Generation of Weakest Preconditions and Precise Array Invariants. - Daragh King; Vasileios Koutavas; Laura Kovács (FormaliSE, 2025)

Positive Almost-Sure Termination of Polynomial Random Walks. - Lorenz Winkler; Laura Kovács (CoRR, 2025)

(Un)Solvable loop analysis. - Daneshvar Amrollahi; Ezio Bartocci; George Kenison; Laura Kovács; Marcel Moosbrugger; Miroslav Stankovic (Formal Methods Syst. Des., 2025)

FuzzFeed: An Automatic Approach to Weakest Precondition Generation using LLMs and Fuzzing. - Daragh King; Vasileios Koutavas; Laura Kovács (CoRR, 2025)

Synthesis Benchmarks for Automated Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Andrei Voronkov; Eva Maria Wagner; Richard Steven Zilincík (CoRR, 2025)