default search action
Laura Kovács
Person information
- affiliation: TU Wien, Vienna, Austria
- affiliation: Chalmers University, Gothenburg, Sweden
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j16]Julian Müllner, Marcel Moosbrugger, Laura Kovács:
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. Proc. ACM Program. Lang. 8(POPL): 882-910 (2024) - [c114]Laura Kovács, Petra Hozzová, Márton Hajdú, Andrei Voronkov:
Induction in Saturation. IJCAR (1) 2024: 21-29 - [c113]Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov:
Reducibility Constraints in Superposition. IJCAR (1) 2024: 115-132 - [c112]Petra Hozzová, Daneshvar Amrollahi, Márton Hajdú, Laura Kovács, Andrei Voronkov, Eva Maria Wagner:
Synthesis of Recursive Programs in Saturation. IJCAR (1) 2024: 154-171 - [c111]Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács:
MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). IJCAR (1) 2024: 386-395 - [c110]Pamina Georgiou, Márton Hajdú, Laura Kovács:
Saturating Sorting without Sorts. LPAR 2024: 88-105 - [c109]Johannes Schoisswohl, Laura Kovács, Konstantin Korovin:
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. LPAR 2024: 147-164 - [c108]Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovács, Michael Rawson:
Scaling CheckMate for Game-Theoretic Security. LPAR 2024: 222-231 - [c107]Márton Hajdú, Laura Kovács, Michael Rawson:
Rewriting and Inductive Reasoning. LPAR 2024: 278-294 - [c106]Robin Coutelier, Mathias Fleury, Laura Kovács:
Lazy Reimplication in Chronological Backtracking. SAT 2024: 9:1-9:19 - [c105]Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson:
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. SP 2024: 3165-3183 - [c104]S. Hitarth, George Kenison, Laura Kovács, Anton Varonka:
Linear Loop Synthesis for Quadratic Invariants. STACS 2024: 41:1-41:18 - [e17]Andrea Kohlhase, Laura Kovács:
Intelligent Computer Mathematics - 17th International Conference, CICM 2024, Montréal, QC, Canada, August 5-9, 2024, Proceedings. Lecture Notes in Computer Science 14960, Springer 2024, ISBN 978-3-031-66996-5 [contents] - [e16]Laura Kovács, Ana Sokolova:
Reachability Problems - 18th International Conference, RP 2024, Vienna, Austria, September 25-27, 2024, Proceedings. Lecture Notes in Computer Science 15050, Springer 2024, ISBN 978-3-031-72620-0 [contents] - [e15]Bernd Finkbeiner, Laura Kovács:
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. Lecture Notes in Computer Science 14570, Springer 2024, ISBN 978-3-031-57245-6 [contents] - [e14]Bernd Finkbeiner, Laura Kovács:
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. Lecture Notes in Computer Science 14571, Springer 2024, ISBN 978-3-031-57248-7 [contents] - [e13]Bernd Finkbeiner, Laura Kovács:
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. Lecture Notes in Computer Science 14572, Springer 2024, ISBN 978-3-031-57255-5 [contents] - [i46]Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath:
SAT-Based Subsumption Resolution. CoRR abs/2401.17832 (2024) - [i45]Clemens Eisenhofer, Michael Rawson, Laura Kovács:
Spanning Matrices via Satisfiability Solving. CoRR abs/2402.10610 (2024) - [i44]Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács:
MCSat-based Finite Field Reasoning in the Yices2 SMT Solver. CoRR abs/2402.17927 (2024) - [i43]Márton Hajdú, Petra Hozzová, Laura Kovács, Giles Reger, Andrei Voronkov:
Getting Saturated with Induction. CoRR abs/2402.18954 (2024) - [i42]Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov:
Program Synthesis in Saturation. CoRR abs/2402.18962 (2024) - [i41]Márton Hajdú, Laura Kovács, Michael Rawson:
Rewriting and Inductive Reasoning. CoRR abs/2402.19199 (2024) - [i40]Pamina Georgiou, Márton Hajdú, Laura Kovács:
Saturating Sorting without Sorts. CoRR abs/2403.03712 (2024) - [i39]Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovács, Michael Rawson:
Scaling Game-Theoretic Security Reasoning. CoRR abs/2403.10310 (2024) - [i38]Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj S. Bjørner, Laura Kovács:
PolySAT: Word-level Bit-vector Reasoning in Z3. CoRR abs/2406.04696 (2024) - [i37]Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson:
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. IACR Cryptol. ePrint Arch. 2024: 534 (2024) - 2023
- [j15]Maximilian Jaroschek, Manuel Kauers, Laura Kovács:
Lonely Points in Simplices. Discret. Comput. Geom. 69(1): 4-25 (2023) - [c103]Laura Kovács, Anton Varonka:
What Else is Undecidable About Loops? RAMiCS 2023: 176-193 - [c102]Clemens Eisenhofer, Laura Kovács, Michael Rawson:
Embedding the Connection Calculus in Satisfiability Modulo Theories. AReCCa@TABLEAUX 2023: 54-63 - [c101]Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath:
SAT-Based Subsumption Resolution. CADE 2023: 190-206 - [c100]Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov:
Program Synthesis in Saturation. CADE 2023: 307-324 - [c99]Lea Salome Brugger, Laura Kovács, Anja Petkovic Komel, Sophie Rain, Michael Rawson:
CheckMate: Automated Game-Theoretic Security Reasoning. CCS 2023: 1407-1421 - [c98]Sophie Rain, Georgia Avarikioti, Laura Kovács, Matteo Maffei:
Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. CSF 2023: 107-122 - [c97]Laura Kovács:
Symbolic Computation in Automated Program Reasoning. FM 2023: 3-9 - [c96]Marcel Moosbrugger, Julian Müllner, Laura Kovács:
Automated Sensitivity Analysis for Probabilistic Loops. iFM 2023: 21-39 - [c95]Laura Kovács:
Algebra-Based Loop Analysis. ISSAC 2023: 41-42 - [c94]George Kenison, Laura Kovács, Anton Varonka:
From Polynomial Invariants to Linear Loops. ISSAC 2023: 398-406 - [c93]Martina Landman, Sophie Rain, Laura Kovács, Gerald Futschek:
Reshaping Unplugged Computer Science Workshops for Primary School Education. ISSEP 2023: 139-151 - [c92]Ahmed Bhayat, Konstantin Korovin, Laura Kovács, Johannes Schoisswohl:
Refining Unification with Abstraction. LPAR 2023: 36-47 - [c91]Thomas Hader, Daniela Kaufmann, Laura Kovács:
SMT Solving over Finite Field Arithmetic. LPAR 2023: 238-256 - [c90]Laura Kovács:
Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). MFCS 2023: 4:1-4:2 - [c89]Clemens Eisenhofer, Ruba Alassaf, Michael Rawson, Laura Kovács:
Non-Classical Logics in Satisfiability Modulo Theories. TABLEAUX 2023: 24-36 - [c88]Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl, Andrei Voronkov:
ALASCA: Reasoning in Quantified Linear Arithmetic. TACAS (1) 2023: 647-665 - [c87]Nikolaj S. Bjørner, Clemens Eisenhofer, Laura Kovács:
Satisfiability Modulo Custom Theories in Z3. VMCAI 2023: 91-105 - [i36]George Kenison, Laura Kovács, Anton Varonka:
From Polynomial Invariants to Linear Loops. CoRR abs/2302.06323 (2023) - [i35]Thomas Hader, Daniela Kaufmann, Laura Kovács:
SMT Solving over Finite Field Arithmetic. CoRR abs/2305.00028 (2023) - [i34]Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson:
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. CoRR abs/2305.12173 (2023) - [i33]Marcel Moosbrugger, Julian Müllner, Laura Kovács:
Automated Sensitivity Analysis for Probabilistic Loops. CoRR abs/2305.15259 (2023) - [i32]Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovic:
(Un)Solvable Loop Analysis. CoRR abs/2306.01597 (2023) - [i31]Julian Müllner, Marcel Moosbrugger, Laura Kovács:
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. CoRR abs/2307.10902 (2023) - [i30]S. Hitarth, George Kenison, Laura Kovács, Anton Varonka:
Linear Loop Synthesis for Quadratic Invariants. CoRR abs/2310.05120 (2023) - 2022
- [j14]Andreas Humenberger, Daneshvar Amrollahi, Nikolaj S. Bjørner, Laura Kovács:
Algebra-Based Reasoning for Loop Synthesis. Formal Aspects Comput. 34(1): 1-31 (2022) - [j13]Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács:
The probabilistic termination tool amber. Formal Methods Syst. Des. 61(1): 90-109 (2022) - [j12]Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács:
This is the moment for probabilistic loops. Proc. ACM Program. Lang. 6(OOPSLA2): 1497-1525 (2022) - [j11]Miroslav Stankovic, Ezio Bartocci, Laura Kovács:
Moment-based analysis of Bayesian network properties. Theor. Comput. Sci. 903: 113-133 (2022) - [c86]Márton Hajdú, Petra Hozzová, Laura Kovács, Giles Reger, Andrei Voronkov:
Getting Saturated with Induction. Principles of Systems Design 2022: 306-322 - [c85]Jakob Rath, Armin Biere, Laura Kovács:
First-Order Subsumption via SAT Solving. FMCAD 2022: 160-169 - [c84]Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovács, Giles Reger:
The Rapid Software Verification Framework. FMCAD 2022: 255-260 - [c83]Ahmed Bhayat, Pamina Georgiou, Clemens Eisenhofer, Laura Kovács, Giles Reger:
Lemmaless Induction in Trace Logic. CICM 2022: 191-208 - [c82]Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov:
The Vampire Approach to Induction (short paper). PAAR@IJCAR 2022 - [c81]Ahmad Karimi, Marcel Moosbrugger, Miroslav Stankovic, Laura Kovács, Ezio Bartocci, Efstathia Bura:
Distribution Estimation for Probabilistic Loops. QEST 2022: 26-42 - [c80]Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovic:
Solving Invariant Generation for Unsolvable Loops. SAS 2022: 19-43 - [c79]Nikolaj S. Bjørner, Clemens Eisenhofer, Laura Kovács:
User-Propagators for Custom Theories in SMT Solving. SMT 2022: 71-79 - [c78]Thomas Hader, Laura Kovács:
An SMT Approach for Solving Polynomials over Finite Fields. SMT 2022: 90-98 - [e12]Jasmin Blanchette, Laura Kovács, Dirk Pattinson:
Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings. Lecture Notes in Computer Science 13385, Springer 2022, ISBN 978-3-031-10768-9 [contents] - [e11]Laura Kovács, Karl Meinke:
Tests and Proofs - 16th International Conference, TAP 2022, Held as Part of STAF 2022, Nantes, France, July 5, 2022, Proceedings. Lecture Notes in Computer Science 13361, Springer 2022, ISBN 978-3-031-09826-0 [contents] - [d4]Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács:
This is the Moment for Probabilistic Loops - Artifact (Polar). Zenodo, 2022 - [d3]Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács:
This is the Moment for Probabilistic Loops - Artifact (Polar). Zenodo, 2022 - [d2]Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács:
This is the Moment for Probabilistic Loops - Artifact (Polar). Zenodo, 2022 - [d1]Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács:
This is the Moment for Probabilistic Loops - Artifact (Polar). Zenodo, 2022 - [i29]Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács:
This is the Moment for Probabilistic Loops. CoRR abs/2204.07185 (2022) - [i28]Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovic:
Solving Invariant Generation for Unsolvable Loops. CoRR abs/2206.06943 (2022) - [i27]Andreas Humenberger, Daneshvar Amrollahi, Nikolaj S. Bjørner, Laura Kovács:
Algebra-Based Reasoning for Loop Synthesis. CoRR abs/2206.11495 (2022) - 2021
- [c77]Petra Hozzová, Laura Kovács, Andrei Voronkov:
Integer Induction in Saturation. CADE 2021: 361-377 - [c76]Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv:
Summing up Smart Transitions. CAV (1) 2021: 317-340 - [c75]Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács:
Automated Termination Analysis of Polynomial Probabilistic Programs. ESOP 2021: 491-518 - [c74]Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács:
The Probabilistic Termination Tool Amber. FM 2021: 667-675 - [c73]Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov:
Induction with Recursive Definitions in Superposition. FMCAD 2021: 1-10 - [c72]Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov:
Inductive Benchmarks for Automated Reasoning. CICM 2021: 124-129 - [c71]Petra Hozzová, Laura Kovács, Jakob Rath:
Automated Generation of Exam Sheets for Automated Deduction. CICM 2021: 185-196 - [c70]Andreas Humenberger, Laura Kovács:
Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). VMCAI 2021: 17-28 - [c69]Johannes Schoisswohl, Laura Kovács:
Automating Induction by Reflection. LFMTP 2021: 39-54 - [i26]Andreas Humenberger, Laura Kovács:
Algebra-based Synthesis of Loops and their Invariants (Invited Paper). CoRR abs/2103.03599 (2021) - [i25]Laura Kovács, Hanna Lachnitt, Stefan Szeider:
Formalizing Graph Trail Properties in Isabelle/HOL. CoRR abs/2103.03607 (2021) - [i24]Ezio Bartocci, Laura Kovács, Miroslav Stankovic:
MORA - Automatic Generation of Moment-Based Invariants. CoRR abs/2103.03908 (2021) - [i23]Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv:
Summing Up Smart Transitions. CoRR abs/2105.07663 (2021) - [i22]Johannes Schoisswohl, Laura Kovács:
Automating Induction by Reflection. CoRR abs/2106.05066 (2021) - [i21]Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács:
The Probabilistic Termination Tool Amber. CoRR abs/2107.13072 (2021) - [i20]Sophie Rain, Zeta Avarikioti, Laura Kovács, Matteo Maffei:
Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. CoRR abs/2109.07429 (2021) - 2020
- [c68]Bernhard Gleiss, Laura Kovács, Jakob Rath:
Subsumption Demodulation in First-Order Theorem Proving. IJCAR (1) 2020: 297-315 - [c67]Pamina Georgiou, Bernhard Gleiss, Laura Kovács:
Trace Logic for Inductive Loop Reasoning. FMCAD 2020: 255-263 - [c66]Ezio Bartocci, Laura Kovács, Miroslav Stankovic:
Analysis of Bayesian Networks via Prob-Solvable Loops. ICTAC 2020: 221-241 - [c65]Andreas Humenberger, Nikolaj S. Bjørner, Laura Kovács:
Algebra-Based Loop Synthesis. IFM 2020: 440-459 - [c64]Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov:
Induction with Generalization in Superposition Reasoning. CICM 2020: 123-137 - [c63]Laura Kovács, Hanna Lachnitt, Stefan Szeider:
Formalizing Graph Trail Properties in Isabelle/HOL. CICM 2020: 190-205 - [c62]Ezio Bartocci, Laura Kovács, Miroslav Stankovic:
Mora - Automatic Generation of Moment-Based Invariants. TACAS (1) 2020: 492-498 - [e10]Igor Konnov, Laura Kovács:
31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference). LIPIcs 171, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2020, ISBN 978-3-95977-160-3 [contents] - [e9]Elvira Albert, Laura Kovács:
LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020. EPiC Series in Computing 73, EasyChair 2020 [contents] - [i19]Bernhard Gleiss, Laura Kovács, Lena Schnedlitz:
Interactive Visualization of Saturation Attempts in Vampire. CoRR abs/2001.04100 (2020) - [i18]Bernhard Gleiss, Laura Kovács, Jakob Rath:
Subsumption Demodulation in First-Order Theorem Proving. CoRR abs/2001.10213 (2020) - [i17]Andreas Humenberger, Laura Kovács:
Algebra-based Loop Synthesis. CoRR abs/2004.11787 (2020) - [i16]Ezio Bartocci, Laura Kovács, Miroslav Stankovic:
Analysis of Bayesian Networks via Prob-Solvable Loops. CoRR abs/2007.09450 (2020) - [i15]Pamina Georgiou, Bernhard Gleiss, Laura Kovács:
Trace Logic for Inductive Loop Reasoning. CoRR abs/2008.01387 (2020) - [i14]Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács:
Automated Termination Analysis of Polynomial Probabilistic Programs. CoRR abs/2010.03444 (2020)
2010 – 2019
- 2019
- [j10]Pascal Schreck, Tetsuo Ida, Laura Kovács:
Foreword - Formalization of geometry, automated and interactive geometric reasoning. Ann. Math. Artif. Intell. 85(2-4): 71-72 (2019) - [j9]James H. Davenport, Laura Kovács, Daniela Zaharie:
Foreword. Math. Comput. Sci. 13(4): 459-460 (2019) - [c61]Ezio Bartocci, Laura Kovács, Miroslav Stankovic:
Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. ATVA 2019: 255-276 - [c60]Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei:
Verifying Relational Properties using Trace Logic. FMCAD 2019: 170-178 - [c59]Bernhard Gleiss, Laura Kovács, Lena Schnedlitz:
Interactive Visualization of Saturation Attempts in Vampire. IFM 2019: 504-513 - [c58]Gergely Kovásznai, Krisztián Gajdár, Laura Kovács:
Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. SYNASC 2019: 85-91 - [c57]David Damestani, Laura Kovács, Martin Suda:
Superposition Reasoning about Quantified Bitvector Formulas. SYNASC 2019: 95-99 - [e8]Laura Kovács, Andrei Voronkov:
Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops. EPiC Series in Computing 71, EasyChair 2019 [contents] - [i13]Ezio Bartocci, Laura Kovács, Miroslav Stankovic:
Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. CoRR abs/1905.02835 (2019) - [i12]Maximilian Jaroschek, Manuel Kauers, Laura Kovács:
Lonely Points in Simplices. CoRR abs/1905.08747 (2019) - [i11]Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei:
Verifying Relational Properties using Trace Logic. CoRR abs/1906.09899 (2019) - 2018
- [c56]Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov:
A FOOLish Encoding of the Next State Relations of Imperative Programs. IJCAR 2018: 405-421 - [c55]Bernhard Gleiss, Laura Kovács, Simon Robillard:
Loop Analysis by Quantification over Iterations. LPAR 2018: 381-399 - [c54]Andreas Humenberger, Maximilian Jaroschek, Laura Kovács:
Aligator.jl - A Julia Package for Loop Invariant Generation. CICM 2018: 111-117 - [c53]Andreas Humenberger, Maximilian Jaroschek, Laura Kovács:
Invariant Generation for Multi-Path Loops with Polynomial Assignments. VMCAI 2018: 226-246 - [i10]Andreas Humenberger, Maximilian Jaroschek, Laura Kovács:
Invariant Generation for Multi-Path Loops with Polynomial Assignments. CoRR abs/1801.03967 (2018) - [i9]Andreas Humenberger, Maximilian Jaroschek, Laura Kovács:
Aligator.jl - A Julia Package for Loop Invariant Generation. CoRR abs/1808.05394 (2018) - 2017
- [j8]Jens Knoop, Laura Kovács, Jakob Zwirchmayr:
Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution. J. Symb. Comput. 80: 101-124 (2017) - [c52]Bernhard Gleiss, Laura Kovács, Martin Suda:
Splitting Proofs for Interpolation. CADE 2017: 291-309 - [c51]Laura Kovács:
First-Order Interpolation and Grey Areas of Proofs (Invited Talk). CSL 2017: 3:1-3:1 - [c50]Koen Claessen, Jonatan Kilhamn, Laura Kovács, Bengt Lennartson:
A Supervisory Control Algorithm Based on Property-Directed Reachability. Haifa Verification Conference 2017: 115-130 - [c49]Andreas Humenberger, Maximilian Jaroschek, Laura Kovács:
Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. ISSAC 2017: 221-228 - [c48]Laura Kovács, Andrei Voronkov:
First-Order Interpolation and Interpolating Proof Systems. LPAR 2017: 49-64 - [c47]Laura Kovács, Simon Robillard, Andrei Voronkov:
Coming to terms with quantified reasoning. POPL 2017: 260-270 - [e7]Laura Kovács, Andrei Voronkov:
Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, July 2, 2016. EPiC Series in Computing 44, EasyChair 2017 [contents] - [i8]Laura Kovács:
Symbolic Computation and Automated Reasoning for Program Analysis. CoRR abs/1704.03202 (2017) - [i7]Andreas Humenberger, Maximilian Jaroschek, Laura Kovács:
Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. CoRR abs/1705.02863 (2017) - [i6]Bernhard Gleiss, Laura Kovács, Martin Suda:
Splitting Proofs for Interpolation. CoRR abs/1711.02503 (2017) - [i5]Koen Claessen, Jonatan Kilhamn, Laura Kovács, Bengt Lennartson:
A Supervisory Control Algorithm Based on Property-Directed Reachability. CoRR abs/1711.06501 (2017) - 2016
- [c46]Yuting Chen, Laura Kovács, Simon Robillard:
Theory-Specific Reasoning about Loops with Arrays using Vampire. Vampire@IJCAR 2016: 16-32 - [c45]Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov:
The vampire and the FOOL. CPP 2016: 37-48 - [c44]Evgenii Kotelnikov, Laura Kovács, Martin Suda, Andrei Voronkov:
A Clausal Normal Form Translation for FOOL. GCAI 2016: 53-71 - [c43]Laura Kovács:
Symbolic Computation and Automated Reasoning for Program Analysis. IFM 2016: 20-27 - [e6]Laura Kovács, Andrei Voronkov:
Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany, August 2, 2015. EPiC Series in Computing 38, EasyChair 2016 [contents] - [i4]Laura Kovács, Simon Robillard, Andrei Voronkov:
Coming to Terms with Quantified Reasoning. CoRR abs/1611.02908 (2016) - 2015
- [j7]Adel Bouhoula, Bruno Buchberger, Laura Kovács, Temur Kutsia:
Special issue on symbolic computation in software science. J. Symb. Comput. 69: 1-2 (2015) - [c42]Laura Kovács, Simon Robillard:
Reasoning About Loops Using Vampire. Vampire Workshop 2015: 52-62 - [c41]Pavol Cerný, Thomas A. Henzinger, Laura Kovács, Arjun Radhakrishna, Jakob Zwirchmayr:
Segment Abstraction for Worst-Case Execution Time Analysis. ESOP 2015: 105-131 - [c40]Wolfgang Ahrendt, Laura Kovács, Simon Robillard:
Reasoning About Loops Using Vampire in KeY. LPAR 2015: 434-443 - [c39]Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov:
A First Class Boolean Sort in First-Order Theorem Proving and TPTP. CICM 2015: 71-86 - [e5]Laura Kovács, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen M. Watt, Daniela Zaharie:
17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2015, Timisoara, Romania, September 21-24, 2015. IEEE Computer Society 2015, ISBN 978-1-5090-0461-4 [contents] - [i3]Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov:
A First Class Boolean Sort in First-Order Theorem Proving and TPTP. CoRR abs/1505.01682 (2015) - [i2]Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov:
The Vampire and the FOOL. CoRR abs/1510.04821 (2015) - 2014
- [j6]Laura Kovács:
Symbol Elimination for Automated Generation of Program Properties. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 70 (2014) - [c38]Ashutosh Gupta, Laura Kovács, Bernhard Kragl, Andrei Voronkov:
Extensional Crisis and Proving Identity. ATVA 2014: 185-200 - [c37]Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov:
SAT solving experiments in Vampire. Vampire Workshop 2014: 29-32 - [c36]Ioan Dragan, Laura Kovács:
Lingva: Generating and Proving Program Properties Using Symbol Elimination. Ershov Memorial Conference 2014: 67-75 - [c35]Mohammad Reza Shoaei, Laura Kovács, Bengt Lennartson:
Supervisory Control of Discrete-Event Systems via IC3. Haifa Verification Conference 2014: 252-266 - [c34]Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov:
Experimenting with SAT Solvers in Vampire. MICAI (1) 2014: 431-442 - 2013
- [j5]Laura Kovács, Rosario Pugliese, Josep Silva, Francesco Tiezzi:
Special issue on Automated Specification and Verification of Web Systems. J. Log. Algebraic Methods Program. 82(8): 241-242 (2013) - [c33]Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr:
SmacC: A Retargetable Symbolic Execution Engine. ATVA 2013: 482-486 - [c32]Laura Kovács, Andrei Voronkov:
First-Order Theorem Proving and Vampire. CAV 2013: 1-35 - [c31]Régis Blanc, Ashutosh Gupta, Laura Kovács, Bernhard Kragl:
Tree Interpolation in Vampire. LPAR 2013: 173-181 - [c30]Laura Kovács, Andrei Mantsivoda, Andrei Voronkov:
The Inverse Method for Many-Valued Logics. MICAI (1) 2013: 12-23 - [c29]Laura Kovács, Simone Fulvio Rollini, Natasha Sharygina:
A Parametric Interpolation Framework for First-Order Theories. MICAI (1) 2013: 24-40 - [c28]Jens Knoop, Laura Kovács, Jakob Zwirchmayr:
WCET squeezing: on-demand feasibility refinement for proven precise WCET-bounds. RTNS 2013: 161-170 - [c27]Ioan Dragan, Konstantin Korovin, Laura Kovács, Andrei Voronkov:
Bound Propagation for Arithmetic Reasoning in Vampire. SYNASC 2013: 169-176 - [c26]Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr:
The Auspicious Couple: Symbolic Execution and WCET Analysis. WCET 2013: 53-63 - [e4]Laura Kovács, Temur Kutsia:
5th International Symposium on Symbolic Computation in Software Science, SCSS 2013, Castle of Hagenberg, Austria. EPiC Series in Computing 15, EasyChair 2013 [contents] - [e3]Laura Kovács, Temur Kutsia:
6th International Workshop on Automated Specification and Verification of Web Systems, WWV 2010, Vienna, Austria, July 30-31, 2010. EPiC Series in Computing 18, EasyChair 2013 [contents] - 2012
- [j4]Laura Kovács, Temur Kutsia:
Special issue on Automated Specification and Verification of Web Systems. J. Appl. Log. 10(1): 1 (2012) - [j3]Nikolaj S. Bjørner, Laura Kovács:
Foreword. J. Symb. Comput. 47(12): 1413-1415 (2012) - [c25]Krystof Hoder, Andreas Holzer, Laura Kovács, Andrei Voronkov:
Vinter: A Vampire-Based Tool for Interpolation. APLAS 2012: 148-156 - [c24]Jens Knoop, Laura Kovács, Jakob Zwirchmayr:
r-TuBound: Loop Bounds for WCET Analysis (Tool Paper). LPAR 2012: 435-444 - [c23]Krystof Hoder, Laura Kovács, Andrei Voronkov:
Playing in the grey area of proofs. POPL 2012: 259-272 - [c22]Armelle Bonenfant, Hugues Cassé, Marianne De Michiel, Jens Knoop, Laura Kovács, Jakob Zwirchmayr:
FFX: a portable WCET annotation language. RTNS 2012: 91-100 - [c21]Laura Kovács, Béla Paláncz, Levente Kovács:
Solving Robust Glucose-Insulin Control by Dixon Resultant Computations. SYNASC 2012: 53-61 - [e2]Andrei Voronkov, Laura Kovács, Nikolaj S. Bjørner:
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. EPiC Series in Computing 1, EasyChair 2012 [contents] - [i1]Nikolaj S. Bjørner, Krishnendu Chatterjee, Laura Kovács, Rupak Majumdar:
Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). Dagstuhl Reports 2(11): 45-65 (2012) - 2011
- [c20]Laura Kovács, Georg Moser, Andrei Voronkov:
On Transfinite Knuth-Bendix Orders. CADE 2011: 384-399 - [c19]Jens Knoop, Laura Kovács, Jakob Zwirchmayr:
Symbolic Loop Bound Computation for WCET Analysis. Ershov Memorial Conference 2011: 227-242 - [c18]Krystof Hoder, Laura Kovács, Andrei Voronkov:
Case Studies on Invariant Generation Using a Saturation Theorem Prover. MICAI (1) 2011: 1-15 - [c17]Laura Kovács:
Symbol Elimination in Program Analysis. SYNASC 2011: 12 - [c16]Krystof Hoder, Laura Kovács, Andrei Voronkov:
Invariant Generation in Vampire. TACAS 2011: 60-64 - [e1]Laura Kovács, Rosario Pugliese, Francesco Tiezzi:
Proceedings 7th International Workshop on Automated Specification and Verification of Web Systems, WWV 2011, Reykjavik, Iceland, 9th June 2011. EPTCS 61, 2011 [contents] - 2010
- [j2]Martin Giese, Andrew Ireland, Laura Kovács:
Introduction. J. Symb. Comput. 45(11): 1097-1100 (2010) - [c15]Krystof Hoder, Laura Kovács, Andrei Voronkov:
Interpolation and Symbol Elimination in Vampire. IJCAR 2010: 188-195 - [c14]Régis Blanc, Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács:
ABC: Algebraic Bound Computation for Loops. LPAR (Dakar) 2010: 103-118 - [c13]Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrey Rybalchenko:
Aligators for Arrays (Tool Paper). LPAR (Yogyakarta) 2010: 348-356 - [c12]Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrei Voronkov:
Invariant and Type Inference for Matrices. VMCAI 2010: 163-179
2000 – 2009
- 2009
- [c11]Laura Kovács, Andrei Voronkov:
Interpolation and Symbol Elimination. CADE 2009: 199-213 - [c10]Laura Kovács:
A Complete Invariant Generation Approach for P-solvable Loops. Ershov Memorial Conference 2009: 242-256 - [c9]Laura Kovács, Andrei Voronkov:
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. FASE 2009: 470-485 - [c8]Laura Kovács, Andrei Voronkov:
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. SYNASC 2009: 10 - 2008
- [c7]Laura Kovács:
Aligator: A Mathematica Package for Invariant Generation (System Description). IJCAR 2008: 275-282 - [c6]Laura Kovács:
Invariant Generation for P-Solvable Loops with Assignments. CSR 2008: 349-359 - [c5]Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács:
Valigator: A Verification Tool with Bound and Invariant Generation. LPAR 2008: 333-342 - [c4]Laura Kovács:
Reasoning Algebraically About P-Solvable Loops. TACAS 2008: 249-264 - 2006
- [j1]Bruno Buchberger, Adrian Craciun, Tudor Jebelean, Laura Kovács, Temur Kutsia, Koji Nakagawa, Florina Piroi, Nikolaj Popov, Judit Robu, Markus Rosenkranz, Wolfgang Windsteiger:
Theorema: Towards computer-aided mathematical theory exploration. J. Appl. Log. 4(4): 470-504 (2006) - [c3]Laura Kovács, Nikolaj Popov, Tudor Jebelean:
Combining Logic and Algebraic Techniques for Program Verification in Theorema. ISoLA 2006: 67-74 - 2005
- [c2]Laura Ildikó Kovács, Tudor Jebelean:
An Algorithm for Automated Generation of Invariants for Loops with Conditionals. SYNASC 2005: 245-249 - 2004
- [c1]Tudor Jebelean, Laura Kovács, Nikolaj Popov:
Experimental Program Verification in the Theorema System. ISoLA (Preliminary proceedings) 2004: 92-99
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from , , and to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-24 21:33 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint