Laura Kovács - RankMe

225 papers A* 5A 20B 47C 12Misc 10Journal 81Unranked 38

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Constraint Learning for Non-confluent Proof Search. CoRR Michael Rawson, Clemens Eisenhofer, Laura Kovács
2026	J	`jnl`	Finding Connections via Satisfiability Solving. CoRR Clemens Eisenhofer, Michael Rawson, Laura Kovács
2026	J	`jnl`	Lean on Vampire Proofs (Short Paper). CoRR Jonas Bodingbauer, Márton Hajdú, Laura Kovács, Axel Polaczek, Michael Rawson
2026	A	`conf`	Moments in Time: Algebraic Analysis for Solvable Loops (Invited Talk). STACS Laura Kovács
2026	J	`jnl`	On Solving String Equations via Powers and Parikh Images. CoRR Clemens Eisenhofer, Theodor Seiser, Nikolaj S. Bjørner, Laura Kovács
2026	J	`jnl`	Polar: An Algebraic Analyzer for (Probabilistic) Loops. CoRR Marcel Moosbrugger, Julian Müllner, Ezio Bartocci, Laura Kovács
2025	J	`jnl`	(Un)Solvable loop analysis. Formal Methods Syst. Des. Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovic
2025	J	`jnl`	A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning. CoRR Daragh King, Vasileios Koutavas, Laura Kovács
2025	B	`conf`	Constraint Learning for Non-confluent Proof Search. TABLEAUX Michael Rawson, Clemens Eisenhofer, Laura Kovács
2025	J	`jnl`	Correction: (Un)Solvable loop analysis. Formal Methods Syst. Des. Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovic
2025	J	`jnl`	Divide and Conquer: A Compositional Approach to Game-Theoretic Security. Proc. ACM Program. Lang. Ivana Bocevska, Anja Petkovic Komel, Laura Kovács, Sophie Rain, Michael Rawson
2025	B	`conf`	Finding Connections via Satisfiability Solving. TABLEAUX Clemens Eisenhofer, Michael Rawson, Laura Kovács
2025	J	`jnl`	FuzzFeed: An Automatic Approach to Weakest Precondition Generation using LLMs and Fuzzing. CoRR Daragh King, Vasileios Koutavas, Laura Kovács
2025	B	`conf`	Game Modeling of Blockchain Protocols. iFM Sophie Rain, Anja Petkovic Komel, Michael Rawson, Laura Kovács
2025	B	`ed.`	Integrated Formal Methods - 19th International Conference, IFM 2024, Manchester, UK, November 13-15, 2024, Proceedings IFM Nikolai Kosmatov, Laura Kovács
2025	J	`jnl`	Lazy Reimplication in Chronological Backtracking. CoRR Robin Coutelier, Mathias Fleury, Laura Kovács
2025	—	`conf`	Llm-Based Generation of Weakest Preconditions and Precise Array Invariants. FormaliSE Daragh King, Vasileios Koutavas, Laura Kovács
2025	B	`conf`	On Solving String Equations via Powers and Parikh Images. TABLEAUX Clemens Eisenhofer, Theodor Seiser, Nikolaj S. Bjørner, Laura Kovács
2025	A	`conf`	Partial Redundancy in Saturation. CADE Márton Hajdú, Laura Kovács, Andrei Voronkov
2025	J	`jnl`	Partial Redundancy in Saturation. CoRR Márton Hajdú, Laura Kovács, Andrei Voronkov
2025	—	`conf`	Positive Almost-Sure Termination of Polynomial Random Walks. QEST+FORMATS Lorenz Winkler, Laura Kovács
2025	J	`jnl`	Positive Almost-Sure Termination of Polynomial Random Walks. CoRR Lorenz Winkler, Laura Kovács
2025	J	`jnl`	SAT solving for variants of first-order subsumption. Formal Methods Syst. Des. Robin Coutelier, Jakob Rath, Michael Rawson, Armin Biere, Laura Kovács
2025	C	`conf`	Synthesis Benchmarks for Automated Reasoning. CICM Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov, Eva Maria Wagner, Richard Steven Zilincík
2025	J	`jnl`	Synthesis Benchmarks for Automated Reasoning. CoRR Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov, Eva Maria Wagner, Richard Steven Zilincík
2025	A	`conf`	Term Ordering Diagrams. CADE Márton Hajdú, Robin Coutelier, Laura Kovács, Andrei Voronkov
2025	J	`jnl`	Term Ordering Diagrams. CoRR Márton Hajdú, Robin Coutelier, Laura Kovács, Andrei Voronkov
2025	—	`conf`	The Vampire Diary. CAV (3) Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
2025	J	`jnl`	The Vampire Diary. CoRR Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
2024	A*	`conf`	CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. SP Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson
2024	J	`jnl`	CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. IACR Cryptol. ePrint Arch. Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson
2024	J	`jnl`	Getting Saturated with Induction. CoRR Márton Hajdú, Petra Hozzová, Laura Kovács, Giles Reger, Andrei Voronkov
2024	—	`conf`	Induction in Saturation. IJCAR (1) Laura Kovács, Petra Hozzová, Márton Hajdú, Andrei Voronkov
2024	C	`ed.`	Intelligent Computer Mathematics - 17th International Conference, CICM 2024, Montréal, QC, Canada, August 5-9, 2024, Proceedings CICM Andrea Kohlhase, Laura Kovács
2024	A	`conf`	Lazy Reimplication in Chronological Backtracking. SAT Robin Coutelier, Mathias Fleury, Laura Kovács
2024	A	`conf`	Linear Loop Synthesis for Quadratic Invariants. STACS S. Hitarth, George Kenison, Laura Kovács, Anton Varonka
2024	—	`conf`	MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). IJCAR (1) Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács
2024	J	`jnl`	MCSat-based Finite Field Reasoning in the Yices2 SMT Solver. CoRR Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács
2024	—	`conf`	Polar: An Algebraic Analyzer for (Probabilistic) Loops. Principles of Verification (1) Marcel Moosbrugger, Julian Müllner, Ezio Bartocci, Laura Kovács
2024	—	`conf`	PolySAT: Word-level Bit-vector Reasoning in Z3. VSTTE Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj S. Bjørner, Laura Kovács
2024	J	`jnl`	PolySAT: Word-level Bit-vector Reasoning in Z3. CoRR Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj S. Bjørner, Laura Kovács
2024	J	`jnl`	Program Synthesis in Saturation. CoRR Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov
2024	—	`ed.`	Reachability Problems - 18th International Conference, RP 2024, Vienna, Austria, September 25-27, 2024, Proceedings RP Laura Kovács, Ana Sokolova
2024	—	`conf`	Reducibility Constraints in Superposition. IJCAR (1) Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov
2024	B	`conf`	Rewriting and Inductive Reasoning. LPAR Márton Hajdú, Laura Kovács, Michael Rawson
2024	J	`jnl`	Rewriting and Inductive Reasoning. CoRR Márton Hajdú, Laura Kovács, Michael Rawson
2024	J	`jnl`	SAT Solving for Variants of First-Order Subsumption. CoRR Robin Coutelier, Jakob Rath, Michael Rawson, Armin Biere, Laura Kovács
2024	J	`jnl`	SAT and Interactions (Dagstuhl Seminar 24421). Dagstuhl Reports Olaf Beyersdorff, Laura Kovács, Meena Mahajan, Martina Seidl, Kaspar Kasche
2024	J	`jnl`	SAT-Based Subsumption Resolution. CoRR Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath
2024	B	`conf`	Saturating Sorting without Sorts. LPAR Pamina Georgiou, Márton Hajdú, Laura Kovács
2024	J	`jnl`	Saturating Sorting without Sorts. CoRR Pamina Georgiou, Márton Hajdú, Laura Kovács
2024	B	`conf`	Scaling CheckMate for Game-Theoretic Security. LPAR Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovács, Michael Rawson
2024	J	`jnl`	Scaling Game-Theoretic Security Reasoning. CoRR Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovács, Michael Rawson
2024	J	`jnl`	Spanning Matrices via Satisfiability Solving. CoRR Clemens Eisenhofer, Michael Rawson, Laura Kovács
2024	J	`jnl`	Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. Proc. ACM Program. Lang. Julian Müllner, Marcel Moosbrugger, Laura Kovács
2024	—	`conf`	Synthesis of Recursive Programs in Saturation. IJCAR (1) Petra Hozzová, Daneshvar Amrollahi, Márton Hajdú, Laura Kovács, Andrei Voronkov, Eva Maria Wagner
2024	—	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I TACAS (1) Bernd Finkbeiner, Laura Kovács
2024	—	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II TACAS (2) Bernd Finkbeiner, Laura Kovács
2024	—	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III TACAS (3) Bernd Finkbeiner, Laura Kovács
2024	B	`conf`	VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. LPAR Johannes Schoisswohl, Laura Kovács, Konstantin Korovin
2023	J	`jnl`	(Un)Solvable Loop Analysis. CoRR Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovic
2023	—	`conf`	ALASCA: Reasoning in Quantified Linear Arithmetic. TACAS (1) Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl, Andrei Voronkov
2023	B	`conf`	Algebra-Based Loop Analysis. ISSAC Laura Kovács
2023	B	`conf`	Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). MFCS Laura Kovács
2023	B	`conf`	Automated Sensitivity Analysis for Probabilistic Loops. iFM Marcel Moosbrugger, Julian Müllner, Laura Kovács
2023	J	`jnl`	Automated Sensitivity Analysis for Probabilistic Loops. CoRR Marcel Moosbrugger, Julian Müllner, Laura Kovács
2023	A*	`conf`	CheckMate: Automated Game-Theoretic Security Reasoning. CCS Lea Salome Brugger, Laura Kovács, Anja Petkovic Komel, Sophie Rain, Michael Rawson
2023	J	`jnl`	CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. CoRR Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson
2023	—	`conf`	Embedding the Connection Calculus in Satisfiability Modulo Theories. AReCCa@TABLEAUX Clemens Eisenhofer, Laura Kovács, Michael Rawson
2023	B	`conf`	From Polynomial Invariants to Linear Loops. ISSAC George Kenison, Laura Kovács, Anton Varonka
2023	J	`jnl`	From Polynomial Invariants to Linear Loops. CoRR George Kenison, Laura Kovács, Anton Varonka
2023	J	`jnl`	Linear Loop Synthesis for Quadratic Invariants. CoRR S. Hitarth, George Kenison, Laura Kovács, Anton Varonka
2023	J	`jnl`	Lonely Points in Simplices. Discret. Comput. Geom. Maximilian Jaroschek, Manuel Kauers, Laura Kovács
2023	B	`conf`	Non-Classical Logics in Satisfiability Modulo Theories. TABLEAUX Clemens Eisenhofer, Ruba Alassaf, Michael Rawson, Laura Kovács
2023	A	`conf`	Program Synthesis in Saturation. CADE Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov
2023	B	`conf`	Refining Unification with Abstraction. LPAR Ahmed Bhayat, Konstantin Korovin, Laura Kovács, Johannes Schoisswohl
2023	—	`conf`	Reshaping Unplugged Computer Science Workshops for Primary School Education. ISSEP Martina Landman, Sophie Rain, Laura Kovács, Gerald Futschek
2023	A	`conf`	SAT-Based Subsumption Resolution. CADE Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath
2023	B	`conf`	SMT Solving over Finite Field Arithmetic. LPAR Thomas Hader, Daniela Kaufmann, Laura Kovács
2023	J	`jnl`	SMT Solving over Finite Field Arithmetic. CoRR Thomas Hader, Daniela Kaufmann, Laura Kovács
2023	B	`conf`	Satisfiability Modulo Custom Theories in Z3. VMCAI Nikolaj S. Bjørner, Clemens Eisenhofer, Laura Kovács
2023	J	`jnl`	Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. CoRR Julian Müllner, Marcel Moosbrugger, Laura Kovács
2023	B	`conf`	Symbolic Computation in Automated Program Reasoning. FM Laura Kovács
2023	A	`conf`	Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. CSF Sophie Rain, Georgia Avarikioti, Laura Kovács, Matteo Maffei
2023	C	`conf`	What Else is Undecidable About Loops? RAMiCS Laura Kovács, Anton Varonka
2022	J	`jnl`	Algebra-Based Reasoning for Loop Synthesis. CoRR Andreas Humenberger, Daneshvar Amrollahi, Nikolaj S. Bjørner, Laura Kovács
2022	J	`jnl`	Algebra-Based Reasoning for Loop Synthesis. Formal Aspects Comput. Andreas Humenberger, Daneshvar Amrollahi, Nikolaj S. Bjørner, Laura Kovács
2022	—	`conf`	An SMT Approach for Solving Polynomials over Finite Fields. SMT Thomas Hader, Laura Kovács
2022	A	`ed.`	Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings IJCAR Jasmin Blanchette, Laura Kovács, Dirk Pattinson
2022	—	`conf`	Distribution Estimation for Probabilistic Loops. QEST Ahmad Karimi, Marcel Moosbrugger, Miroslav Stankovic, Laura Kovács, Ezio Bartocci, Efstathia Bura
2022	B	`conf`	First-Order Subsumption via SAT Solving. FMCAD Jakob Rath, Armin Biere, Laura Kovács
2022	—	`conf`	Getting Saturated with Induction. Principles of Systems Design Márton Hajdú, Petra Hozzová, Laura Kovács, Giles Reger, Andrei Voronkov
2022	C	`conf`	Lemmaless Induction in Trace Logic. CICM Ahmed Bhayat, Pamina Georgiou, Clemens Eisenhofer, Laura Kovács, Giles Reger
2022	J	`jnl`	Moment-based analysis of Bayesian network properties. Theor. Comput. Sci. Miroslav Stankovic, Ezio Bartocci, Laura Kovács
2022	B	`conf`	Solving Invariant Generation for Unsolvable Loops. SAS Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovic
2022	J	`jnl`	Solving Invariant Generation for Unsolvable Loops. CoRR Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovic
2022	—	`ed.`	Tests and Proofs - 16th International Conference, TAP 2022, Held as Part of STAF 2022, Nantes, France, July 5, 2022, Proceedings TAP@STAF Laura Kovács, Karl Meinke
2022	B	`conf`	The Rapid Software Verification Framework. FMCAD Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovács, Giles Reger
2022	—	`conf`	The Vampire Approach to Induction (short paper). PAAR@IJCAR Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov
2022	J	`jnl`	The probabilistic termination tool amber. Formal Methods Syst. Des. Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács
2022	J	`jnl`	This is the Moment for Probabilistic Loops. CoRR Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács
2022	J	`jnl`	This is the moment for probabilistic loops. Proc. ACM Program. Lang. Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács
2022	—	`conf`	User-Propagators for Custom Theories in SMT Solving. SMT Nikolaj S. Bjørner, Clemens Eisenhofer, Laura Kovács
2021	B	`conf`	Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). VMCAI Andreas Humenberger, Laura Kovács
2021	J	`jnl`	Algebra-based Synthesis of Loops and their Invariants (Invited Paper). CoRR Andreas Humenberger, Laura Kovács
2021	C	`conf`	Automated Generation of Exam Sheets for Automated Deduction. CICM Petra Hozzová, Laura Kovács, Jakob Rath
2021	A	`conf`	Automated Termination Analysis of Polynomial Probabilistic Programs. ESOP Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács
2021	J	`jnl`	Automating Induction by Reflection. CoRR Johannes Schoisswohl, Laura Kovács
2021	—	`conf`	Automating Induction by Reflection. LFMTP Johannes Schoisswohl, Laura Kovács
2021	J	`jnl`	Formalizing Graph Trail Properties in Isabelle/HOL. CoRR Laura Kovács, Hanna Lachnitt, Stefan Szeider
2021	B	`conf`	Induction with Recursive Definitions in Superposition. FMCAD Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov
2021	C	`conf`	Inductive Benchmarks for Automated Reasoning. CICM Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov
2021	A	`conf`	Integer Induction in Saturation. CADE Petra Hozzová, Laura Kovács, Andrei Voronkov
2021	J	`jnl`	MORA - Automatic Generation of Moment-Based Invariants. CoRR Ezio Bartocci, Laura Kovács, Miroslav Stankovic
2021	J	`jnl`	Summing Up Smart Transitions. CoRR Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv
2021	—	`conf`	Summing up Smart Transitions. CAV (1) Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv
2021	B	`conf`	The Probabilistic Termination Tool Amber. FM Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács
2021	J	`jnl`	The Probabilistic Termination Tool Amber. CoRR Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács
2021	J	`jnl`	Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. CoRR Sophie Rain, Zeta Avarikioti, Laura Kovács, Matteo Maffei
2020	B	`ed.`	31st International Conference on Concurrency Theory, CONCUR 2020, Vienna, Austria (Virtual Conference), September 1-4, 2020 CONCUR Igor Konnov, Laura Kovács
2020	B	`conf`	Algebra-Based Loop Synthesis. IFM Andreas Humenberger, Nikolaj S. Bjørner, Laura Kovács
2020	J	`jnl`	Algebra-based Loop Synthesis. CoRR Andreas Humenberger, Laura Kovács
2020	C	`conf`	Analysis of Bayesian Networks via Prob-Solvable Loops. ICTAC Ezio Bartocci, Laura Kovács, Miroslav Stankovic
2020	J	`jnl`	Analysis of Bayesian Networks via Prob-Solvable Loops. CoRR Ezio Bartocci, Laura Kovács, Miroslav Stankovic
2020	J	`jnl`	Automated Termination Analysis of Polynomial Probabilistic Programs. CoRR Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács
2020	C	`conf`	Formalizing Graph Trail Properties in Isabelle/HOL. CICM Laura Kovács, Hanna Lachnitt, Stefan Szeider
2020	C	`conf`	Induction with Generalization in Superposition Reasoning. CICM Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov
2020	J	`jnl`	Interactive Visualization of Saturation Attempts in Vampire. CoRR Bernhard Gleiss, Laura Kovács, Lena Schnedlitz
2020	B	`ed.`	LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020. LPAR Elvira Albert, Laura Kovács
2020	—	`conf`	Mora - Automatic Generation of Moment-Based Invariants. TACAS (1) Ezio Bartocci, Laura Kovács, Miroslav Stankovic
2020	—	`conf`	Subsumption Demodulation in First-Order Theorem Proving. IJCAR (1) Bernhard Gleiss, Laura Kovács, Jakob Rath
2020	J	`jnl`	Subsumption Demodulation in First-Order Theorem Proving. CoRR Bernhard Gleiss, Laura Kovács, Jakob Rath
2020	B	`conf`	Trace Logic for Inductive Loop Reasoning. FMCAD Pamina Georgiou, Bernhard Gleiss, Laura Kovács
2020	J	`jnl`	Trace Logic for Inductive Loop Reasoning. CoRR Pamina Georgiou, Bernhard Gleiss, Laura Kovács
2019	B	`conf`	Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. ATVA Ezio Bartocci, Laura Kovács, Miroslav Stankovic
2019	J	`jnl`	Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. CoRR Ezio Bartocci, Laura Kovács, Miroslav Stankovic
2019	J	`jnl`	Foreword - Formalization of geometry, automated and interactive geometric reasoning. Ann. Math. Artif. Intell. Pascal Schreck, Tetsuo Ida, Laura Kovács
2019	J	`jnl`	Foreword. Math. Comput. Sci. James H. Davenport, Laura Kovács, Daniela Zaharie
2019	B	`conf`	Interactive Visualization of Saturation Attempts in Vampire. IFM Bernhard Gleiss, Laura Kovács, Lena Schnedlitz
2019	J	`jnl`	Lonely Points in Simplices. CoRR Maximilian Jaroschek, Manuel Kauers, Laura Kovács
2019	Misc	`conf`	Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. SYNASC Gergely Kovásznai, Krisztián Gajdár, Laura Kovács
2019	Misc	`conf`	Superposition Reasoning about Quantified Bitvector Formulas. SYNASC David Damestani, Laura Kovács, Martin Suda
2019	—	`ed.`	Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops Vampire Laura Kovács, Andrei Voronkov
2019	B	`conf`	Verifying Relational Properties using Trace Logic. FMCAD Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei
2019	J	`jnl`	Verifying Relational Properties using Trace Logic. CoRR Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei
2018	A	`conf`	A FOOLish Encoding of the Next State Relations of Imperative Programs. IJCAR Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
2018	C	`conf`	Aligator.jl - A Julia Package for Loop Invariant Generation. CICM Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
2018	J	`jnl`	Aligator.jl - A Julia Package for Loop Invariant Generation. CoRR Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
2018	B	`conf`	Invariant Generation for Multi-Path Loops with Polynomial Assignments. VMCAI Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
2018	J	`jnl`	Invariant Generation for Multi-Path Loops with Polynomial Assignments. CoRR Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
2018	B	`conf`	Loop Analysis by Quantification over Iterations. LPAR Bernhard Gleiss, Laura Kovács, Simon Robillard
2017	—	`conf`	A Supervisory Control Algorithm Based on Property-Directed Reachability. Haifa Verification Conference Koen Claessen, Jonatan Kilhamn, Laura Kovács, Bengt Lennartson
2017	J	`jnl`	A Supervisory Control Algorithm Based on Property-Directed Reachability. CoRR Koen Claessen, Jonatan Kilhamn, Laura Kovács, Bengt Lennartson
2017	B	`conf`	Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. ISSAC Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
2017	J	`jnl`	Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. CoRR Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
2017	A*	`conf`	Coming to terms with quantified reasoning. POPL Laura Kovács, Simon Robillard, Andrei Voronkov
2017	B	`conf`	First-Order Interpolation and Grey Areas of Proofs (Invited Talk). CSL Laura Kovács
2017	B	`conf`	First-Order Interpolation and Interpolating Proof Systems. LPAR Laura Kovács, Andrei Voronkov
2017	J	`jnl`	Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution. J. Symb. Comput. Jens Knoop, Laura Kovács, Jakob Zwirchmayr
2017	A	`conf`	Splitting Proofs for Interpolation. CADE Bernhard Gleiss, Laura Kovács, Martin Suda
2017	J	`jnl`	Splitting Proofs for Interpolation. CoRR Bernhard Gleiss, Laura Kovács, Martin Suda
2017	J	`jnl`	Symbolic Computation and Automated Reasoning for Program Analysis. CoRR Laura Kovács
2017	—	`ed.`	Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, July 2, 2016. Vampire@IJCAR Laura Kovács, Andrei Voronkov
2016	—	`conf`	A Clausal Normal Form Translation for FOOL. GCAI Evgenii Kotelnikov, Laura Kovács, Martin Suda, Andrei Voronkov
2016	J	`jnl`	Coming to Terms with Quantified Reasoning. CoRR Laura Kovács, Simon Robillard, Andrei Voronkov
2016	—	`ed.`	Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany, August 2, 2015 Vampire Laura Kovács, Andrei Voronkov
2016	B	`conf`	Symbolic Computation and Automated Reasoning for Program Analysis. IFM Laura Kovács
2016	B	`conf`	The vampire and the FOOL. CPP Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov
2016	—	`conf`	Theory-Specific Reasoning about Loops with Arrays using Vampire. Vampire@IJCAR Yuting Chen, Laura Kovács, Simon Robillard
2015	Misc	`ed.`	17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2015, Timisoara, Romania, September 21-24, 2015 SYNASC Laura Kovács, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen M. Watt, Daniela Zaharie
2015	C	`conf`	A First Class Boolean Sort in First-Order Theorem Proving and TPTP. CICM Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
2015	J	`jnl`	A First Class Boolean Sort in First-Order Theorem Proving and TPTP. CoRR Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
2015	B	`conf`	Reasoning About Loops Using Vampire in KeY. LPAR Wolfgang Ahrendt, Laura Kovács, Simon Robillard
2015	—	`conf`	Reasoning About Loops Using Vampire. Vampire Workshop Laura Kovács, Simon Robillard
2015	A	`conf`	Segment Abstraction for Worst-Case Execution Time Analysis. ESOP Pavol Cerný, Thomas A. Henzinger, Laura Kovács, Arjun Radhakrishna, Jakob Zwirchmayr
2015	J	`jnl`	Special issue on symbolic computation in software science. J. Symb. Comput. Adel Bouhoula, Bruno Buchberger, Laura Kovács, Temur Kutsia
2015	J	`jnl`	The Vampire and the FOOL. CoRR Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov
2014	—	`conf`	Experimenting with SAT Solvers in Vampire. MICAI (1) Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov
2014	B	`conf`	Extensional Crisis and Proving Identity. ATVA Ashutosh Gupta, Laura Kovács, Bernhard Kragl, Andrei Voronkov
2014	—	`conf`	Lingva: Generating and Proving Program Properties Using Symbol Elimination. Ershov Memorial Conference Ioan Dragan, Laura Kovács
2014	—	`conf`	SAT solving experiments in Vampire. Vampire Workshop Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov
2014	—	`conf`	Supervisory Control of Discrete-Event Systems via IC3. Haifa Verification Conference Mohammad Reza Shoaei, Laura Kovács, Bengt Lennartson
2014	J	`jnl`	Symbol Elimination for Automated Generation of Program Properties. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Laura Kovács
2013	—	`ed.`	5th International Symposium on Symbolic Computation in Software Science, SCSS 2013, Castle of Hagenberg, Austria SCSS Laura Kovács, Temur Kutsia
2013	—	`ed.`	6th International Workshop on Automated Specification and Verification of Web Systems, WWV 2010, Vienna, Austria, July 30-31, 2010 WWV Laura Kovács, Temur Kutsia
2013	—	`conf`	A Parametric Interpolation Framework for First-Order Theories. MICAI (1) Laura Kovács, Simone Fulvio Rollini, Natasha Sharygina
2013	Misc	`conf`	Bound Propagation for Arithmetic Reasoning in Vampire. SYNASC Ioan Dragan, Konstantin Korovin, Laura Kovács, Andrei Voronkov
2013	A*	`conf`	First-Order Theorem Proving and Vampire. CAV Laura Kovács, Andrei Voronkov
2013	B	`conf`	SmacC: A Retargetable Symbolic Execution Engine. ATVA Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr
2013	J	`jnl`	Special issue on Automated Specification and Verification of Web Systems. J. Log. Algebraic Methods Program. Laura Kovács, Rosario Pugliese, Josep Silva, Francesco Tiezzi
2013	—	`conf`	The Auspicious Couple: Symbolic Execution and WCET Analysis. WCET Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr
2013	—	`conf`	The Inverse Method for Many-Valued Logics. MICAI (1) Laura Kovács, Andrei Mantsivoda, Andrei Voronkov
2013	B	`conf`	Tree Interpolation in Vampire. LPAR Régis Blanc, Ashutosh Gupta, Laura Kovács, Bernhard Kragl
2013	Misc	`conf`	WCET squeezing: on-demand feasibility refinement for proven precise WCET-bounds. RTNS Jens Knoop, Laura Kovács, Jakob Zwirchmayr
2012	Misc	`conf`	FFX: a portable WCET annotation language. RTNS Armelle Bonenfant, Hugues Cassé, Marianne De Michiel, Jens Knoop, Laura Kovács, Jakob Zwirchmayr
2012	J	`jnl`	Foreword. J. Symb. Comput. Nikolaj S. Bjørner, Laura Kovács
2012	J	`jnl`	Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). Dagstuhl Reports Nikolaj S. Bjørner, Krishnendu Chatterjee, Laura Kovács, Rupak Majumdar
2012	A*	`conf`	Playing in the grey area of proofs. POPL Krystof Hoder, Laura Kovács, Andrei Voronkov
2012	—	`ed.`	Second International Workshop on Invariant Generation, WING 2009, York, UK, March 29, 2009 and Third International Workshop on Invariant Generation, WING 2010, Edinburgh, UK, July 21, 2010 WING@ETAPS/IJCAR Andrei Voronkov, Laura Kovács, Nikolaj S. Bjørner
2012	Misc	`conf`	Solving Robust Glucose-Insulin Control by Dixon Resultant Computations. SYNASC Laura Kovács, Béla Paláncz, Levente Kovács
2012	J	`jnl`	Special issue on Automated Specification and Verification of Web Systems. J. Appl. Log. Laura Kovács, Temur Kutsia
2012	B	`conf`	Vinter: A Vampire-Based Tool for Interpolation. APLAS Krystof Hoder, Andreas Holzer, Laura Kovács, Andrei Voronkov
2012	B	`conf`	r-TuBound: Loop Bounds for WCET Analysis (Tool Paper). LPAR Jens Knoop, Laura Kovács, Jakob Zwirchmayr
2011	—	`conf`	Case Studies on Invariant Generation Using a Saturation Theorem Prover. MICAI (1) Krystof Hoder, Laura Kovács, Andrei Voronkov
2011	A	`conf`	Invariant Generation in Vampire. TACAS Krystof Hoder, Laura Kovács, Andrei Voronkov
2011	A	`conf`	On Transfinite Knuth-Bendix Orders. CADE Laura Kovács, Georg Moser, Andrei Voronkov
2011	—	`ed.`	Proceedings 7th International Workshop on Automated Specification and Verification of Web Systems, WWV 2011, Reykjavik, Iceland, 9th June 2011. WWV Laura Kovács, Rosario Pugliese, Francesco Tiezzi
2011	Misc	`conf`	Symbol Elimination in Program Analysis. SYNASC Laura Kovács
2011	—	`conf`	Symbolic Loop Bound Computation for WCET Analysis. Ershov Memorial Conference Jens Knoop, Laura Kovács, Jakob Zwirchmayr
2010	—	`conf`	ABC: Algebraic Bound Computation for Loops. LPAR (Dakar) Régis Blanc, Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács
2010	—	`conf`	Aligators for Arrays (Tool Paper). LPAR (Yogyakarta) Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrey Rybalchenko
2010	A	`conf`	Interpolation and Symbol Elimination in Vampire. IJCAR Krystof Hoder, Laura Kovács, Andrei Voronkov
2010	J	`jnl`	Introduction. J. Symb. Comput. Martin Giese, Andrew Ireland, Laura Kovács
2010	B	`conf`	Invariant and Type Inference for Matrices. VMCAI Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrei Voronkov
2009	—	`conf`	A Complete Invariant Generation Approach for P-solvable Loops. Ershov Memorial Conference Laura Kovács
2009	B	`conf`	Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. FASE Laura Kovács, Andrei Voronkov
2009	Misc	`conf`	Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. SYNASC Laura Kovács, Andrei Voronkov
2009	A	`conf`	Interpolation and Symbol Elimination. CADE Laura Kovács, Andrei Voronkov
2008	A	`conf`	Aligator: A Mathematica Package for Invariant Generation (System Description). IJCAR Laura Kovács
2008	Misc	`conf`	Invariant Generation for P-Solvable Loops with Assignments. CSR Laura Kovács
2008	A	`conf`	Reasoning Algebraically About P-Solvable Loops. TACAS Laura Kovács
2008	B	`conf`	Valigator: A Verification Tool with Bound and Invariant Generation. LPAR Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács
2006	C	`conf`	Combining Logic and Algebraic Techniques for Program Verification in Theorema. ISoLA Laura Kovács, Nikolaj Popov, Tudor Jebelean
2006	J	`jnl`	Theorema: Towards computer-aided mathematical theory exploration. J. Appl. Log. Bruno Buchberger, Adrian Craciun, Tudor Jebelean, Laura Kovács, Temur Kutsia, Koji Nakagawa, Florina Piroi, Nikolaj Popov, Judit Robu, Markus Rosenkranz, Wolfgang Windsteiger
2004	—	`conf`	Experimental Program Verification in the Theorema System. ISoLA (Preliminary proceedings) Tudor Jebelean, Laura Kovács, Nikolaj Popov