TU Wien Informatics

Laura Kovacs

Univ.Prof. Dr.techn. / MSc

Research Areas

  • verification, invariants, theorem proving, symbolic computation
Laura Kovacs

Roles

2019

  • Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops / E. Bartocci, L. Kovacs, S. Stankovic / Talk: ATVA 2019: the 17th International Symposium on Automated Technology for Verification and Analysis, Taipei, Taiwan; 2019-10-28 - 2019-10-31; in: "Proc. of ATVA 2019: the 17th International Symposium on Automated Technology for Verification and Analysis", 11781 (2019), 255 - 276

2018

  • Symbol Elimination in Program Analysis / L. Kovacs / Keynote Lecture: 2nd Facebook Testing and Veri cation Symposium (FaceTAV), London, UK (invited); 2018-11-28 - 2018-11-29
  • Symbol Elimination for Program Analysis / L. Kovacs / Keynote Lecture: Highlights of Logic, Games and Automata, Berlin, Germany (invited); 2018-09-18 - 2018-09-21
  • First-Order Interpolation in the Grey Area of Proofs / L. Kovacs / Keynote Lecture: Summer School on Syntax meets Semantics - Methods, Interactions, and Connections in Substructural Logics (SYSMICS), Les Diablerets, Switzerland (invited); 2018-08-22 - 2018-08-26
  • First-Order Interpolation / L. Kovacs / Keynote Lecture: SAT/SMT/AR Summer School 2018, Manchester (invited); 2018-07-03 - 2018-07-06
  • Automated Reasoning for Rigorous Systems Engineering / L. Kovacs / Keynote Lecture: RiSE/SHINE Media Seminar 2018, Vienna (invited); 2018-05-07
  • First-Order Theorem Proving in Rigorous Systems Engineering / L. Kovacs, A. Voronkov / Keynote Lecture: RiSE/SHiNE Winter School 2018, Wien (invited); 2018-02-05 - 2018-02-09
  • Automated Reasoning for Systems Engineering / L. Kovacs / Keynote Lecture: 2018 IEEE International Conference on Future IoT Technologies (Future IoT 2018), Eger, Hungary (invited); 2018-01-18 - 2018-01-19
  • Vampire 2017. Proceedings of the 4th Vampire Workshop / L. Kovacs, A. Voronkov / in series "Vampire 2017. Proceedings of the 4th Vampire Workshop", series editor: A. Voronkov; issued by: EasyChair; EasyChair EPiC Series in Computing, EasyChair, 2018
  • Automated Reasoning for Systems Engineering / L. Kovacs / Keynote Lecture: Foundations of Information and Knowledge Systems (FOIKS) 2018, Budapest, Hungary (invited); 2018-05-14 - 2018-05-18; in: "Foundations of Information and Knowledge Systems (FOIKS) 2018", LNCS, 10833 (2018), 1
  • Aligator.jl - A Julia Package for Loop Invariant Generation / A. Humenberger, M. Jaroschek, L. Kovacs / Talk: 11th International Conference on Intelligent Computer Mathematics (CICM), Hagenberg; 2018-08-13 - 2018-08-17; in: "Proceedings of the 11th International Conference on Intelligent Computer Mathematics (CICM)", F. Rabe et al. (ed.); LNCS, 11006 (2018), 111 - 117
  • Loop Analysis by Quantification over Iterations / B. Gleiss, L. Kovacs, S. Robillard / Talk: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia; 2018-11-16 - 2018-11-21; in: "Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)", G. Barthe, G. Sutcliffe, M. Veanes (ed.); EasyChair EPiC Series in Computing, 57 (2018), 381 - 399
  • A FOOLish Encoding of the Next State Relations of Imperative Programs. / E. Kotelnikov, L. Kovacs, A. Voronkov / Talk: 9th International Joint Conference on Automated Reasoning (IJCAR) 2018, Oxford; 2018-08-14 - 2018-08-17; in: "Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR) 2018", LNCS, 10900 (2018), 405 - 421
  • Invariant Generation for Multi-Path Loops with Polynomial Assignments / A. Humenberger, M. Jaroschek, L. Kovacs / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "Verification, Model Checking, and Abstract Interpretation - 19th International Conference", Springer, (2018), ISBN: 978-3-319-73720-1; 226 - 246

2017

  • Symbol Elimination for Program Analysis / L. Kovacs / Keynote Lecture: ETH Workshop on Software Correctness and Reliability, Zürich, Switzerland (invited); 2017-10-13 - 2017-10-14
  • Polynomial Invariant Generation for Multi-Path Loops / A. Humenberger, M. Jaroschek, L. Kovacs / Talk: Second International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Kaiserslautern, Germany; 2017-07-29
  • Algebraic Reasoning for Program Analysis / L. Kovacs / Keynote Lecture: 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS), Ljubljana, Slovenia (invited); 2017-06-12 - 2017-06-16
  • Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution / J. Knoop, L. Kovacs, J. Zwirchmayr / Journal of Symbolic Computation, 80 (2017), 101 - 124
  • First-Order Interpolation and Interpolating Proof Systems / L. Kovacs, A. Voronkov / in: "LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning", EasyChair EPiC Series in Computing, Volume 46, 2017, 49 - 64
  • First-Order Interpolation and Grey Areas of Proofs / L. Kovacs / Keynote Lecture: 26th EACSL Annual Conference on Computer Science Logic (CSL), Stockholm, Sweden (invited); 2017-08-20 - 2017-08-24; in: "Proceedings of the 26th EACSL Annual Conference on Computer Science Logic (CSL)", V. Goranko, M. Dam (ed.); LIPIcs, 82 (2017), ISBN: 978-3-95977-045-3; 3:1
  • A Supervisory Control Algorithm Based on Property-Directed Reachability / K. Claessen, J. Kilhamn, L. Kovacs, B. Lennartson / Talk: 13th International Haifa Verification Conference (HVC 2017), Haifa, Israel; 2017-11-13 - 2017-11-15; in: "13th International Haifa Verification Conference (HVC)", O. Strichman, R. Tzoref-Brill (ed.); Lecture Notes in Computer Science / Springer, 10629 / Cham (2017), ISBN: 978-3-319-70388-6; 115 - 130
  • Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences / A. Humenberger, M. Jaroschek, L. Kovacs / Talk: International Symposium on Symbolic and Algebraic Computation (ISSAC), Kaiserslautern; 2017-07-23 - 2017-07-28; in: "ISSAC '17 Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation", ACM, (2017), ISBN: 978-1-4503-5064-8; 221 - 228
  • Splitting Proofs for Interpolation / B. Gleiss, L. Kovacs, M. Suda / Talk: CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden; 2017-08-06 - 2017-08-11; in: "Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings", Springer, Lecture Notes in Computer Science / 10395 (2017), ISBN: 978-3-319-63046-5; 291 - 309
  • Coming to Terms with Quantified Reasoning / L. Kovacs, S. Robillard, A. Voronkov / Talk: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Paris, France; 2017-01-18 - 2017-01-20; in: "Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)", G. Castagna, A. Gordon (ed.); ACM, (2017), ISBN: 978-1-4503-4660-3; 260 - 270
  • Theory-Specific Reasoning about Loops with Arrays using Vampire / Y. Chen, L. Kovacs, S. Robillard / accepted as talk for: The Third Vampire Workshop, Coimbra, Portugal; 2016-07-02; in: "Proceedings of the Third Vampire Workshop", L. Kovacs, A. Voronkov (ed.); EasyChair EPiC Series in Computing, (2017)

2016

  • With a Timisoara Background in the Scientific World of Computer Science and / L. Kovacs / Keynote Lecture: Timisoara Hungarian Science Festival, Timisoara, Romania (invited); 2016-11-26
  • Automated Reasoning for Systems Engineering / L. Kovacs / Keynote Lecture: Austrian Computer Science Day 2018, Salzburg (invited); 2016-06-15
  • Enjoying Research at the Intersection of Math and Computer Science / L. Kovacs / Keynote Lecture: Women in Science Workshop Series (WISE), Gothenburg, Schweden (invited); 2016-06-08
  • First-Order Theorem Proving and Vampire / L. Kovacs / Keynote Lecture: Spring School on Logic and Verification - LoVE, Vienna, Austria (invited); 2016-04-15 - 2016-04-17
  • Proceedings of the 1st and 2nd Vampire Workshops / L. Kovacs, A. Voronkov / in series "Proceedings of the 1st and 2nd Vampire Workshops", series editor: L. Kovacs, A. Voronkov; issued by: EasyChair; EasyChair EPiC Series in Computing, 2016
  • Symbolic Computation and Automated Reasoning for Program Analysis / L. Kovacs / Keynote Lecture: 12th International Conference on Integrated Formal Methods (iFM), Bertinoro, Italy (invited); 2016-06-01 - 2016-06-05; in: "Proceedings of the 12th International Conference on Integrated Formal Methods (iFM)", E. Abraham, M. Huisman (ed.); Springer / LNCS, 9681 (2016), ISBN: 978-3-319-33692-3; 20 - 27
  • The Vampire and the FOOL / E. Kotelnikov, L. Kovacs, G. Reger, A. Voronkov / Talk: 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), Saint Petersburg, Florida, USA; 2016-01-20 - 2016-01-22; in: "Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP)", J. Avigad, A. Chlipala (ed.); ACM, (2016), ISBN: 978-1-4503-4127-1; 37 - 48
  • A Clausal Normal Form Translation for FOOL / E. Kotelnikov, L. Kovacs, M. Suda, A. Voronkov / Talk: GCAI 2016 / 2nd Global Conference on Artificial Intelligence, Berlin, Germany; 2016-09-29 - 2016-10-02; in: "GCAI 2016. 2nd Global Conference on Artificial Intelligence", EasyChair, EPiC Series in Computing / 41 / Berlin (2016), 53 - 71

2015

  • Symbol Elimination for Program Analysis / L. Kovacs / Talk: Dagstuhl Seminar 15471 on "Symbolic Computation and Satisfiability Checking", Dagstuhl, Germany (invited); 2015-11-16 - 2015-11-20
  • Symbol Elimination for Program Analysis / L. Kovacs / Talk: Theoretical Computer Science Seminar Series of the KTH Royal Institute of Technology,, Stockholm, Sweden (invited); 2015-05-18
  • Special Issue on Symbolic Computation in Software Science / A. Bouhoula, B. Buchberger, L. Kovacs, T. Kutsia / in series "Journal of Symbolic Computation", series editor: H. Hong; Elsevier, 2015, ISSN: 0747-7171, 158 pages
  • Foreword to the Special Issue on Symbolic Computation in Software Science / A. Bouhoula, B. Buchberger, L. Kovacs, T. Kutsia / Journal of Symbolic Computation, 69 (2015), 1 - 2
  • Segment Abstraction for Worst-Case Execution Time Analysis / P. Cerny, T. Henzinger, L. Kovacs, A. Radhakrishna, J. Zwirchmayr / Talk: European Symposium on Programming (ESOP), Londok, UK; 2015-04-11 - 2015-04-18; in: "Proc. of the 24th European Symposium on Programming (ESOP)", J. Vitek (ed.); LNCS, 9032 (2015), ISBN: 978-3-662-46668-1; 105 - 131
  • Reasoning About Loops Using Vampire in KeY / W. Ahrendt, L. Kovacs, S. Robillard / Talk: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Suva, Fiji; 2015-11-24 - 2015-11-28; in: "Proc. of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20)", M. Davis, A. Fehnker, A. McIver, A. Voronkov (ed.); LNCS, 9450 (2015), ISBN: 978-3-662-48898-0; 434 - 443
  • A First Class Boolean Sort in First-Order Theorem Proving and TPTP / E. Kotelnikov, L. Kovacs, A. Voronkov / Talk: International Conference on Intelligent Computer Mathematics (CICM), Washington, DC, USA; 2015-07-13 - 2015-07-17; in: "Proc. of the International Conference on Intelligent Computer Mathematics", M. Kerber et al. (ed.); LNCS, 9150 (2015), ISBN: 978-3-319-20614-1; 71 - 86
  • First-Order Theorem Proving and Program Analysis / L. Kovacs / Talk: LCCC-ACCESS workshop on Model-Based Engineering, Lund, Sweden (invited); 2015-05-04 - 2015-05-06; in: "Proc. of the LCCC-ACCESS workshop on Model-Based Engineering", J. Baras et al. (ed.); (2015), ISSN: 0280-5316; 192 - 217

2014

2013

2012

2011

2010