TU Wien Informatics

Overview Professors Scientific Staff Administrative Staff Student Staff External Lecturers By Responsibilities By Committee By Name
Related
Guest Professors Honoraries Alumni (LinkedIn) #5qw

Laura Kovacs

Univ.Prof.in Dr.in techn. / MSc

Research Focus

  • Logic and Computation: 100%

Research Areas

  • software verification, Computational Logic, theorem proving, Automated Reasoning, computer algebra, Cybersecurity
Laura Kovacs

Roles

Contact

2024W

2025S

 

2025

  • Polar: An Algebraic Analyzer for (Probabilistic) Loops / Moosbrugger, M., Müllner, J., Bartocci, E., & Kovacs, L. (2025). Polar: An Algebraic Analyzer for (Probabilistic) Loops. In Principles of Verification: Cycling the Probabilistic Landscape (Vol. 15260, pp. 179–200). https://doi.org/10.1007/978-3-031-75783-9_8
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025) / QuAT (2024–2025)

2024

  • SAT solving for variants of first-order subsumption / Coutelier, R., Rath, J., Rawson, M., Biere, A., & Kovacs, L. (2024). SAT solving for variants of first-order subsumption. Formal Methods in System Design. https://doi.org/10.1007/s10703-024-00454-1
    Download: SAT solving for variants of first-order subsumption (3.26 MB)
    Projects: DK - Logic (2014–2023) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)
  • PolySAT: Word-level Bit-vector Reasoning in Z3 / Rath, J., Eisenhofer, C., Kaufmann, D., Bjørner, N., & Kovacs, L. (2024, October 14). PolySAT: Word-level Bit-vector Reasoning in Z3 [Conference Presentation]. VSTTE 2024, Prague, Czechia. http://hdl.handle.net/20.500.12708/211021
    Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
  • Lazy Reimplication in Chronological Backtracking / Coutelier, R., Fleury, M., & Kovacs, L. (2024). Lazy Reimplication in Chronological Backtracking. In S. Chakraborty & J.-H. R. Jiang (Eds.), 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) (pp. 9:1-9:19). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.SAT.2024.9
    Download: Lazy Reimplication in Chronological Backtracking (946 KB)
    Projects: ForSmart (2023–2027) / SFB SPyCoDe (2023–2026) / Testing Dafny (2024–2027)
  • MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper) / Hader, T., Kaufmann, D., Irfan, A., Graham-Lengrand, S., & Kovács, L. (2024). MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 386–395). Springer International Publishing. https://doi.org/10.1007/978-3-031-63498-7_23
    Projects: ARTIST (2021–2026) / CalgSAT (2024–2027) / SFB SPyCoDe (2023–2026)
  • (Un)Solvable loop analysis / Amrollahi, D., Bartocci, E., Kenison, G. J., Kovacs, L., Moosbrugger, M., & Stankovic, M. (2024). (Un)Solvable loop analysis. Formal Methods in System Design. https://doi.org/10.1007/s10703-024-00455-0
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Rewriting and Inductive Reasoning / Hajdu, M., Kovács, L., & Rawson, M. (2024). Rewriting and Inductive Reasoning. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 278–294). https://doi.org/10.29007/vbfp
    Download: PDF (589 KB)
    Projects: ARTIST (2021–2026) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)
  • Saturating Sorting without Sorts / Georgiou, P., Hajdu, M., & Kovacs, L. (2024). Saturating Sorting without Sorts. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 88–105). https://doi.org/10.29007/rg9z
    Download: PDF (712 KB)
    Projects: ARTIST (2021–2026) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)
  • VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic / Schoisswohl, J., Kovács, L., & Korovin, K. (2024). VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 147–164). https://doi.org/10.29007/kg4v
    Download: PDF (597 KB)
    Projects: ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)
  • Linear Loop Synthesis for Quadratic Invariants / Hitarth, S., Kenison, G. J., Kovacs, L., & Varonka, A. (2024). Linear Loop Synthesis for Quadratic Invariants. In O. Beyersdorff, M. M. Kanté, O. Kupferman, & D. Lokshtanov (Eds.), 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.STACS.2024.41
    Download: PDF (780 KB)
    Projects: ARTIST (2021–2026) / LCS (2017–2025) / ProbInG (2020–2025)
  • Saturating Sorting without Sorts / Georgiou, P., Hajdu, M., & Kovács, L. (2024). Saturating Sorting without Sorts. arXiv. https://doi.org/10.34726/5861
    Download: Preprint (322 KB)
    Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
  • Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs / Müllner, J., Moosbrugger, M., & Kovács, L. (2024). Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. Proceedings of the ACM on Programming Languages, 8(POPL), 882–910. https://doi.org/10.1145/3632872
  • Synthesis of Recursive Programs in Saturation / Hozzová, P., Amrollahi, D., Hajdu, M., Kovács, L., Voronkov, A., & Wagner, E. M. (2024). Synthesis of Recursive Programs in Saturation. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 154–171). Springer International Publishing. https://doi.org/10.1007/978-3-031-63498-7_10
  • Reducibility Constraints in Superposition / Hajdu, M., Kovács, L., Rawson, M., & Voronkov, A. (2024). Reducibility Constraints in Superposition. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 115–132). https://doi.org/10.1007/978-3-031-63498-7_8
    Download: PDF (541 KB)
  • Induction in Saturation / Kovács, L., Hozzová, P., Hajdu, M., & Voronkov, A. (2024). Induction in Saturation. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 21–29). Springer. https://doi.org/10.1007/978-3-031-63498-7_2
    Download: Verlags-PDF (345 KB)
    Projects: ARTIST (2021–2026) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)
  • Scaling CheckMate for Game-Theoretic Security / Rain, S., Brugger, L. S., Petković Komel, A., Kovács, L., & Rawson, M. (2024). Scaling CheckMate for Game-Theoretic Security. In N. Bjorner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Pro gramming, Artificial Intelligence and Reasoning (pp. 222–231). https://doi.org/10.29007/llnq
  • CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model / Jeanteur, S., Kovács, L., Maffei, M., & Rawson, M. (2024). CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. In 2024 IEEE Symposium on Security and Privacy (SP) (pp. 3165–3183). IEEE. https://doi.org/10.1109/SP54263.2024.00246
    Projects: Browsec (2018–2024) / CDL-BOT (2020–2025) / DLDaI (2022–2024) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026) / SPFBT (2020–2026)
  • Quantifying Uncertainty in Probabilistic Loops Without Sampling: A Fully Automated Approach / Bartocci, E. (2024). Quantifying Uncertainty in Probabilistic Loops Without Sampling: A Fully Automated Approach. In L. Kovacs & A. Sokolova (Eds.), Reachability Problems (pp. 3–8). Springer. https://doi.org/10.1007/978-3-031-72621-7_1
    Project: ProbInG (2020–2025)
  • Embedding the Connection Calculus in Satisfiability Modulo Theories / Eisenhofer, C., Kovács, L., & Rawson, M. (2024). Embedding the Connection Calculus in Satisfiability Modulo Theories. In Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) (pp. 54–63). CEUR-WS.org. https://doi.org/10.34726/5394
    Download: PDF (248 KB)
    Projects: ARTIST (2021–2026) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)

2023

  • CheckMate: Automated Game-Theoretic Security Reasoning / Brugger, L. S., Kovács, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2023). CheckMate: Automated Game-Theoretic Security Reasoning. In CCS ’23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 1407–1421). Association for Computing Machinery. https://doi.org/10.1145/3576915.3623183
    Download: PDF (1.15 MB)
    Project: SFB SPyCoDe (2023–2026)
  • Automated Sensitivity Analysis for Probabilistic Loops / Moosbrugger, M., Müllner, J., & Kovács, L. (2023). Automated Sensitivity Analysis for Probabilistic Loops. In P. Herber & A. Wijs (Eds.), iFM 2023 : 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings (pp. 21–39). Springer. https://doi.org/10.1007/978-3-031-47705-8_2
  • Reshaping Unplugged Computer Science Workshops for Primary School Education / Landman, M., Rain, S., Kovács, L., & Gerald Futschek. (2023). Reshaping Unplugged Computer Science Workshops for Primary School Education. In J.-P. Pellet & G. Parriaux (Eds.), Informatics in Schools. Beyond Bits and Bytes: Nurturing Informatics Intelligence in Education : 16th International Conference on Informatics in Schools: Situation, Evolution, and Perspectives, ISSEP 2023, Lausanne, Switzerland, October 23–25, 2023, Proceedings (pp. 139–151). Springer. https://doi.org/10.1007/978-3-031-44900-0_11
    Download: PDF (1020 KB)
    Projects: AbInfVS (2023–2025) / SFB SPyCoDe (2023–2026)
  • Non-Classical Logics in Satisfiability Modulo Theories / Eisenhofer, C., Alassaf, R., Rawson, M., & Kovács, L. (2023). Non-Classical Logics in Satisfiability Modulo Theories. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 24–36). Springer. https://doi.org/10.1007/978-3-031-43513-3_2
    Download: PDF (423 KB)
    Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
  • Program Synthesis in Saturation / Hozzová, P., Kovács, L., Norman, C., & Voronkov, A. (2023). Program Synthesis in Saturation. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 307–324). Springer. https://doi.org/10.1007/978-3-031-38499-8_18
    Download: PDF (528 KB)
    Projects: ARTIST (2021–2026) / DK - Logic (2014–2023)
  • SAT-Based Subsumption Resolution / Coutelier, R., Kovács, L., Rawson, M., & Rath, J. (2023). SAT-Based Subsumption Resolution. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 190–206). Springer. https://doi.org/10.1007/978-3-031-38499-8_11
  • From Polynomial Invariants to Linear Loops / Kenison, G. J., Kovacs, L., & Varonka, A. (2023). From Polynomial Invariants to Linear Loops. In A. Dickenstein, E. Tsigaridas, & G. Jeronimo (Eds.), ISSAC ’23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation (pp. 398–406). Association for Computing Machinery. https://doi.org/10.1145/3597066.3597109
    Projects: ARTIST (2021–2026) / LCS (2017–2025) / ProbInG (2020–2025)
  • Refining Unification with Abstraction / Bhayat, A., Korovin, K., Kovács, L., & Schoisswohl, J. (2023). Refining Unification with Abstraction. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 36–47). EasyChair EPiC. https://doi.org/10.29007/h65j
    Download: PDF (394 KB)
    Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
  • SMT Solving over Finite Field Arithmetic / Hader, T., Kaufmann, D., & Kovacs, L. (2023). SMT Solving over Finite Field Arithmetic. In R. Piscac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 238–256). https://doi.org/10.29007/4n6w
    Project: ARTIST (2021–2026)
  • Symbolic Computation in Automated Program Reasoning / Kovács, L. (2023). Symbolic Computation in Automated Program Reasoning. In M. Chechik, J.-P. Katoen, & M. Leucker (Eds.), Formal Methods : 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings (pp. 3–9). Springer. https://doi.org/10.1007/978-3-031-27481-7_1
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Algebraic Reasoning for (Un)Solvable Loops (Invited Talk) / Kovacs, L. (2023). Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In J. Leroux, S. Lombardy, & D. Peleg (Eds.), 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) (pp. 4:1-4:2). Schloss-Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPICS.MFCS.2023.4
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • ALASCA: Reasoning in Quantified Linear Arithmetic / Korovin, K., Kovács, L., Reger, G., Schoisswohl, J., & Voronkov, A. (2023). ALASCA: Reasoning in Quantified Linear Arithmetic. In S. Sankaranarayanan & N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 647–665). Springer. https://doi.org/10.1007/978-3-031-30823-9_33
    Download: PDF (479 KB)
    Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
  • What Else is Undecidable About Loops? / Kovács, L., & Varonka, A. (2023). What Else is Undecidable About Loops? In R. Glück, L. Santocanale, & M. Winter (Eds.), Relational and Algebraic Methods in Computer Science. RAMiCS 2023 (pp. 176–193). Springer. https://doi.org/10.1007/978-3-031-28083-2_11
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Algebra-Based Loop Analysis / Kovács, L. (2023). Algebra-Based Loop Analysis. In A. Dickenstein, E. Tsigaridas, & G. Jeronimo (Eds.), ISSAC ’23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation (pp. 41–42). Association for Computing Machinery. https://doi.org/10.1145/3597066.3597150
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Satisfiability Modulo Custom Theories in Z3 / Bjørner, N., Eisenhofer, C., & Kovács, L. (2023). Satisfiability Modulo Custom Theories in Z3. In C. Dragoi, M. Emmi, & J. Wang (Eds.), Verification, Model Checking, and Abstract Interpretation. VMCAI 2023 (pp. 91–105). Springer. https://doi.org/10.1007/978-3-031-24950-1_5
    Project: ARTIST (2021–2026)
  • Towards a Game-Theoretic Security Analysis of Off-Chain Protocols / Rain, S., Avarikioti, G., Kovacs, L., & Maffei, M. (2023). Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. In 2023 IEEE 36th Computer Security Foundations Symposium (CSF) (pp. 107–122). IEEE. https://doi.org/10.1109/CSF57540.2023.00003
    Projects: Browsec (2018–2024) / CDL-BOT (2020–2025) / LCS (2017–2025) / PROFET (2019–2023) / ViSP (2019–2023)

2022

  • Getting Saturated with Induction / Hajdu, M., Hozzová, P., Kovács, L., Reger, G., & Voronkov, A. (2022). Getting Saturated with Induction. In J.-F. Raskin, K. Chatterjee, L. Doyen, & R. Majumdar (Eds.), Principles of Systems Design (Vol. 13660, pp. 306–322). Springer Cham. https://doi.org/10.1007/978-3-031-22337-2_15
    Download: PDF (446 KB)
    Projects: ARTIST (2021–2026) / DK - Logic (2014–2023)
  • First-Order Theorem Proving and Vampire / Kovacs, L. (2022, December 6). First-Order Theorem Proving and Vampire [Keynote Presentation]. 7th School of Theoretical Computer Science and Formal Methods (ETMF), online, Brazil.
    Project: ARTIST (2021–2026)
  • This Is the Moment for Probabilistic Loops / Moosbrugger, M., Stankovic, M., Bartocci, E., & Kovacs, L. (2022). This Is the Moment for Probabilistic Loops. Proceedings of the ACM on Programming Languages, 6(OOPSLA2), 1497–1525. https://doi.org/10.1145/3563341
  • Symbolic Computation for Software Analysis / Kovacs, L. (2022, October 25). Symbolic Computation for Software Analysis [Conference Presentation]. Symposium on the Occasion of the 80th Birthday of RISC-founder Bruno Buchberger, Linz, Austria.
    Project: ARTIST (2021–2026)
  • On the Undecidability of Loop Analysis / Varonka, A., & Kovacs, L. (2022, October 12). On the Undecidability of Loop Analysis [Conference Presentation]. Reachability Problems, Kaiserslautern, Germany. https://doi.org/10.1007/978-3-031-19135-0
  • First-Order Theorem Proving - Theory and Practice / Kovacs, L. (2022, October 10). First-Order Theorem Proving - Theory and Practice [Conference Presentation]. Dagstuhl Seminar 22411 on Theory and Practice of SAT and Combinatorial Solving, Dagstuhl, Germany. http://hdl.handle.net/20.500.12708/153840
    Project: ARTIST (2021–2026)
  • The RAPID Software Verification Framework / Georgiou, P., Gleiss, B., Bhayat, A., Rawson, M., Kovács, L., & Reger, G. (2022). The RAPID Software Verification Framework. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 255–260). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_32
    Download: PDF (308 KB)
  • First-Order Subsumption via SAT Solving / Rath, J., Biere, A., & Kovács, L. (2022). First-Order Subsumption via SAT Solving. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 160–169). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_22
    Download: PDF (551 KB)
  • Lonely Points in Simplices / Jaroschek, M., Kauers, M., & Kovács, L. (2022). Lonely Points in Simplices. Discrete and Computational Geometry, 69, 4–25. https://doi.org/10.1007/s00454-022-00428-2
    Project: ARTIST (2021–2026)
  • Getting Saturated with Induction / Kovacs, L. (2022, September 29). Getting Saturated with Induction [Keynote Presentation]. Automated Reasoning Symposium of Amazon Web Services, United States of America (the). http://hdl.handle.net/20.500.12708/153839
    Project: ARTIST (2021–2026)
  • Algebra-Based Analysis of Polynomial Probabilistic Programs / Kovacs, L. (2022, September 22). Algebra-Based Analysis of Polynomial Probabilistic Programs [Keynote Presentation]. Distinguished Lecture Series of the Max Planck Institute for Software Systems (MPI-SWS), Germany. http://hdl.handle.net/20.500.12708/153258
    Project: ARTIST (2021–2026)
  • Distribution Estimation for Probabilistic Loops / Karimi, A., Moosbrugger, M., Stankovič, M., Kovács, L., Bartocci, E., & Bura, E. (2022). Distribution Estimation for Probabilistic Loops. In E. Ábrahám & M. Paolieri (Eds.), Quantitative Evaluation of Systems (pp. 26–42). Springer-Verlag. https://doi.org/10.1007/978-3-031-16336-4_2
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • PolySAT - a word-level solver for large bitvectors / Rath, J., Bjørner, N., Kovacs, L., Nutz, A., & Sagiv, M. (2022, September 1). PolySAT - a word-level solver for large bitvectors [Presentation]. Formal Reasoning about Financial Systems, Stanford, United States of America (the). http://hdl.handle.net/20.500.12708/154065
  • The Vampire Approach to Induction (short paper) / Hajdu, M., Kovács, L., Rawson, M., & Voronkov, A. (2022). The Vampire Approach to Induction (short paper). In B. Konev, C. Schon, & A. Steen (Eds.), PAAR 2022. Practical Aspects of Automated Reasoning 2022.  Proceedings of the Workshop on Practical Aspects of Automated Reasoning. https://doi.org/10.34726/4103
    Download: PDF (836 KB)
  • User-Propagation for Custom Theories in SMT Solving / Bjorner, N., Eisenhofer, C., & Kovács, L. (2022). User-Propagation for Custom Theories in SMT Solving. In D. Deharbe & A. Hyvärinen (Eds.), Satisfiability Modulo Theories. 20th International Workshop. SMT 2022. Proceedings (pp. 71–79). CEUR-WS.org. https://doi.org/10.34726/4104
    Download: PDF (1.15 MB)
    Project: ARTIST (2021–2026)
  • Automating Security Analysis of Off-Chain Protocols / Brugger, L. S., Kovacs, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2022, August 11). Automating Security Analysis of Off-Chain Protocols [Conference Presentation]. 4th International Workshop on Formal Methods for Blockchains, Haifa, Israel. https://doi.org/10.34726/3523
    Download: PDF (265 KB)
    Project: ARTIST (2021–2026)
  • Automated Reasoning: 11th International Joint Conference (IJCAR 2022) / Blanchette, J. C., Kovacs, L., & Pattinson, D. (Eds.). (2022). Automated Reasoning: 11th International Joint Conference (IJCAR 2022) (Vol. 13385). Springer-Verlag. https://doi.org/10.1007/978-3-031-10769-6
    Project: ARTIST (2021–2026)
  • The probabilistic termination tool amber / Moosbrugger, M., Bartocci, E., Katoen, J.-P., & Kovacs, L. (2022). The probabilistic termination tool amber. Formal Methods in System Design, 61(1), 90–109. https://doi.org/10.1007/s10703-023-00424-z
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • An SMT Approach for Solving Polynomials over Finite Fields / Hader, T., & Kovacs, L. (2022). An SMT Approach for Solving Polynomials over Finite Fields. In Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories (SMT) (pp. 90–98).
    Project: ARTIST (2021–2026)
  • Automated Reasoning for Trustworthy Software / Kovacs, L. (2022, June 21). Automated Reasoning for Trustworthy Software [Keynote Presentation]. Austrian Computer Science Day 2022, IST Austria, Austria. http://hdl.handle.net/20.500.12708/153819
    Project: ARTIST (2021–2026)
  • First-Order Theorem Proving and Vampire / Kovacs, L. (2022, June 17). First-Order Theorem Proving and Vampire [Keynote Presentation]. 15TH SUMMER SCHOOL ON MODELLING AND VERIFICATION OF PARALLEL PROCESSES (MOVEP2022), Aalborg, Denmark. http://hdl.handle.net/20.500.12708/153941
    Project: ARTIST (2021–2026)
  • Algebraic Synthesis of Loops and their Invariants / Kovacs, L. (2022, June 6). Algebraic Synthesis of Loops and their Invariants [Conference Presentation]. Workshop on Differential Algebra, Leipzig, Germany. http://hdl.handle.net/20.500.12708/153259
    Project: ARTIST (2021–2026)
  • Tests and Proofs / Meinke, K., & Kovacs, L. (Eds.). (2022). Tests and Proofs (Vol. 13361). Springer-Verlag. https://doi.org/10.1007/978-3-031-09827-7
    Project: ARTIST (2021–2026)
  • Automated Program Reasoning / Kovacs, L. (2022, May 30). Automated Program Reasoning [Keynote Presentation]. Informatics Europe Webinar Series, Switzerland.
    Project: ARTIST (2021–2026)
  • Enjoying Research at the Intersection of Math and Computer Science / Kovacs, L. (2022, April 3). Enjoying Research at the Intersection of Math and Computer Science [Keynote Presentation]. ETAPS 2022 Mentoring Workshop, Munich, Germany.
    Project: ARTIST (2021–2026)
  • Algebra-Based Reasoning for Loop Synthesis / Humenberger, A., Amrollahi, D., Bjørner, N., & Kovács, L. (2022). Algebra-Based Reasoning for Loop Synthesis. Formal Aspects of Computing, 34(1), 4:31. https://doi.org/10.1145/3527458
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Getting Saturated with Induction / Kovacs, L. (2022, January 27). Getting Saturated with Induction [Conference Presentation]. Automated Reasoning Seminar at TU Kaiserslautern, Kaiserslautern, Germany. http://hdl.handle.net/20.500.12708/153837
    Project: ARTIST (2021–2026)
  • Can Computers Think as Humans? / Kovacs, L. (2022, January 26). Can Computers Think as Humans? [Keynote Presentation]. WiSE Talk at the SCIENCE Lecture Series Talks of Wiener Volksshochsculen and City of Vienna, Austria.
    Project: ARTIST (2021–2026)
  • Solving Invariant Generation for Unsolvable Loops / Amrollahi, D., Bartocci, E., Kenison, G., Kovács, L., Moosbrugger, M., & Stankovič, M. (2022). Solving Invariant Generation for Unsolvable Loops. In Static Analysis: 29th International Symposium, SAS 2022 (pp. 19–43). https://doi.org/10.1007/978-3-031-22308-2_3
  • Actions over Core-Closed Knowledge Bases / Cauli, C., Ortiz, M., & Piterman, N. (2022). Actions over Core-Closed Knowledge Bases. In J. Blanchette, L. Kovacs, & D. Pattinson (Eds.), Automated Reasoning.  IJCAR 2022 (pp. 281–299). Springer. https://doi.org/10.1007/978-3-031-10769-6_17
  • Lemmaless Induction in Trace Logic / Bhayat, A., Georgiou, P., Eisenhofer, C., Kovács, L., & Reger, G. (2022). Lemmaless Induction in Trace Logic. In K. Buzzard & T. Kutsia (Eds.), Intelligent Computer Mathematics : 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022, Proceedings (pp. 191–208). https://doi.org/10.34726/5860
    Download: PDF (320 KB)
    Project: DK - Logic (2014–2023)
  • Moment-based analysis of Bayesian network properties / Stankovič, M., Bartocci, E., & Kovács, L. (2022). Moment-based analysis of Bayesian network properties. Theoretical Computer Science, 903, 113–133. https://doi.org/10.1016/j.tcs.2021.12.021

2021

  • Induction with Recursive Definitions in Superposition / Hajdu, M., Hozzová, P., Kovács, L., & Voronkov, A. (2021). Induction with Recursive Definitions in Superposition. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (Vol. 2, pp. 246–255). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34
    Download: PDF (350 KB)
  • Inductive Benchmarks for Automated Reasoning / Hajdu, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2021). Inductive Benchmarks for Automated Reasoning. In Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings (pp. 124–129). Springer. https://doi.org/10.34726/1563
    Download: PDF (216 KB)
    Projects: ARTIST (2021–2026) / Symcar (2016–2021)
  • Automated Generation of Exam Sheets for Automated Deduction / Hozzová, P., Kovács, L., & Rath, J. (2021). Automated Generation of Exam Sheets for Automated Deduction. In Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings (pp. 185–196). Springer. https://doi.org/10.34726/1562
    Download: PDF (458 KB)
    Projects: ARTIST (2021–2026) / Symcar (2016–2021)
  • Integer Induction in Saturation / Hozzová, P., Kovács, L., & Voronkov, A. (2021). Integer Induction in Saturation. In Proceedings of CADE 2021 (pp. 361–377). Springer, Cham. https://doi.org/10.34726/1561
    Download: Preprint submitted for publication as it is (345 KB)
    Projects: ARTIST (2021–2026) / Symcar (2016–2021)
  • Induction in Saturation-Based Reasoning / Kovacs, L. (2021, July 26). Induction in Saturation-Based Reasoning [Keynote Presentation]. 14th Conference on Intelligent Computer Mathematics (CICM 2021), Timisoara, Romania. http://hdl.handle.net/20.500.12708/154161
    Project: ARTIST (2021–2026)
  • The Probabilistic Termination Tool Amber / Marcel Moosbrugger, Ezio Bartocci, Katoen, J.-P., & Laura Kovács. (2021). The Probabilistic Termination Tool Amber. In Formal Methods. FM 2021 (pp. 667–675). https://doi.org/10.1007/978-3-030-90870-6_36
  • Automated Termination Analysis of Polynomial Probabilistic Programs / Moosbrugger, M., Bartocci, E., Katoen, J.-P., & Kovács, L. (2021). Automated Termination Analysis of Polynomial Probabilistic Programs. In Programming Languages and Systems (pp. 491–518). Springer. https://doi.org/10.1007/978-3-030-72019-3_18
  • Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper) / Humenberger, A., & Kovács, L. (2021). Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). In F. Henglein, S. Shoham, & Y. Vizel (Eds.), Verification, Model Checking, and Abstract Interpretation (pp. 17–28). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_2
  • Automating Induction by Reflection / Schoisswohl, J., & Kovács, L. (2021). Automating Induction by Reflection. In E. Pimentel & E. Tassi (Eds.), Electronic Proceedings in Theoretical Computer Science (pp. 39–54). EPTCS. https://doi.org/10.4204/eptcs.337.4
  • Summing up Smart Transitions / Elad, N., Rain, S., Immerman, N., Sagiv, M., & Kovacs, L. (2021). Summing up Smart Transitions. In A. Silva & R. Leino (Eds.), Computer Aided Verification (pp. 317–340). Springer LNCS. https://doi.org/10.1007/978-3-030-81685-8_15

2020

  • Induction with Generalization in Superposition Reasoning / Hajdú, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2020). Induction with Generalization in Superposition Reasoning. In Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM) (pp. 123–137). Springer. https://doi.org/10.34726/961
    Download: Postprint was published at CICM 2020. (300 KB)
    Projects: DoS-IoT (2019–2020) / Symcar (2016–2021) / SYMELS (2019–2020)
  • Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization / Kovasznai, G., Gajdár, K., & Kovács, L. (2020). Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (pp. 85–91). IEEE. https://doi.org/10.34726/341
    Download: accepted version (499 KB)
    Projects: Symcar (2016–2021) / SYMELS (2019–2020)
  • Superposition Reasoning about Quantified Bitvector Formulas / Damestani, D., Kovács, L., & Suda, M. (2020). Superposition Reasoning about Quantified Bitvector Formulas. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (pp. 95–99). IEEE. https://doi.org/10.34726/342
    Download: accepted version (226 KB)
    Projects: Symcar (2016–2021) / SYMELS (2019–2020)
  • Trace Logic for Inductive Loop Reasoning / Georgiou, P., Gleiss, B., & Kovacs, L. (2020). Trace Logic for Inductive Loop Reasoning. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design - FMCAD 2020 (pp. 255–263). IEEE. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_33
  • Analysis of Bayesian Networks via Prob-Solvable Loops / Bartocci, E., Kovács, L., & Stankovič, M. (2020). Analysis of Bayesian Networks via Prob-Solvable Loops. In Theoretical Aspects of Computing – ICTAC 2020 (pp. 221–241). Springer. https://doi.org/10.1007/978-3-030-64276-1_12
  • Mora - Automatic Generation of Moment-Based Invariants / Bartocci, E., Kovács, L., & Stankovič, M. (2020). Mora - Automatic Generation of Moment-Based Invariants. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 492–498). Springer. https://doi.org/10.1007/978-3-030-45190-5_28
  • Trace Logic for Inductive Loop Reasoning / Georgiou, P., Gleiss, B., & Kovács, L. (2020). Trace Logic for Inductive Loop Reasoning. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 255–263). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_33
    Download: Published version (490 KB)
  • Subsumption Demodulation in First-Order Theorem Proving / Gleiss, B., Kovacs, L., & Rath, J. (2020). Subsumption Demodulation in First-Order Theorem Proving. In N. Peltier & V. Sofronie-Stokkermans (Eds.), Automated Reasoning (pp. 297–315). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-51074-9_17
  • Algebra-Based Loop Synthesis / Humenberger, A., Bjørner, N., & Kovacs, L. (2020). Algebra-Based Loop Synthesis. In B. Dongol & E. Troubitsyna (Eds.), Integrated Formal Methods. Proceedings of the 16th International Conference, IFM 2020 (pp. 440–459). Springer. https://doi.org/10.1007/978-3-030-63461-2_24
  • Formalizing Graph Trail Properties in Isabelle/HOL / Kovács, L., Lachnitt, H., & Szeider, S. (2020). Formalizing Graph Trail Properties in Isabelle/HOL. In Intelligent Computer Mathematics 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings (pp. 190–205). LNCS. https://doi.org/10.1007/978-3-030-53518-6_12
  • RAT Elimination / Rebola Pardo, A., & Weissenbacher, G. (2020). RAT Elimination. In L. Kovacs & E. Albert (Eds.), EPiC Series in Computing. EasyChair. https://doi.org/10.29007/fccb
  • A typed parallel lambda-calculus via 1-depth intermediate proofs / Aschieri, F., Ciabattoni, A., & Genco, F. A. (2020). A typed parallel lambda-calculus via 1-depth intermediate proofs. In L. Kovacs (Ed.), EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/g15z
  • ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs / Bartocci, E., Kovacs, L., & Bura, E. (2020). ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs. Vienna Science, Research and Technology Fund - ProbInG, online, Austria. http://hdl.handle.net/20.500.12708/123229
  • Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23) / Albert, E., & Kovacs, L. (Eds.). (2020). Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/24792
  • Proceedings of the 31st International Conference on Concurrency Theory (CONCUR) / Konnov, I., & Kovacs, L. (Eds.). (2020). Proceedings of the 31st International Conference on Concurrency Theory (CONCUR). Dagstuhl Publishing LIPICS. http://hdl.handle.net/20.500.12708/24793

2019

  • 60 Shades of Grey in Vampire / Kovacs, L. (2019). 60 Shades of Grey in Vampire. ANDREI-60: Automating New-Era Deductive Reasoning Event in Iberia, Tbilisi, Georgia. http://hdl.handle.net/20.500.12708/86990
  • Trace Reasoning for Formal Verification using the First-Order Superposition Calculus / Georgiou, P., Gleiss, B., Kovacs, L., & Maffei, M. (2019). Trace Reasoning for Formal Verification using the First-Order Superposition Calculus. FMCAD 2019 Student Forum, San Jose, United States of America (the). http://hdl.handle.net/20.500.12708/86988
  • Interactive Visualization of Saturation Attempts in Vampire / Gleiss, B., Kovács, L., & Schnedlitz, L. (2019). Interactive Visualization of Saturation Attempts in Vampire. In W. Ahrendt & S. Lizeth (Eds.), Integrated Formal Methods : 15th International Conference, IFM 2019, Bergen, Norway, December 2–6, 2019, Proceedings (pp. 504–513). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-34968-4_28
  • Verifying Relational Properties using Trace Logic / Barthe, G., Eilers, R., Georgiou, P., Gleiss, B., Kovacs, L., & Maffei, M. (2019). Verifying Relational Properties using Trace Logic. In B. Clark & J. Yang (Eds.), 2019 Formal Methods in Computer Aided Design (FMCAD). IEEE. https://doi.org/10.23919/fmcad.2019.8894277
  • Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops / Bartocci, E., Kovacs, L., & Stankovic, M. (2019). Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. In Y.-F. Chen, C.-H. Cheng, & J. Esparza (Eds.), Automated Technology for Verification and Analysis (pp. 255–276). Springer. https://doi.org/10.1007/978-3-030-31784-3_15
  • Formal Methods in the Digital World (in Hungarian) / Kovacs, L. (2019). Formal Methods in the Digital World (in Hungarian). JegKepzes Series of Presentations- Hungarian Scientists from the Bartok Bela Highschool, Timisoara, Romania. http://hdl.handle.net/20.500.12708/86998
  • First-Order Interpolation / Kovacs, L. (2019). First-Order Interpolation. PhD Research Seminar in Logic and Computation, Faculty of Informatics, West University of Timisoara, Timisoara, Romania. http://hdl.handle.net/20.500.12708/86997
  • Symbolic Computation and Automated Reasoning for Program Analysis / Kovacs, L. (2019). Symbolic Computation and Automated Reasoning for Program Analysis. 23rd IEEE International Conference on Intelligent Engineering Systems (INES) 2019, Gödöllõ, Hungary. http://hdl.handle.net/20.500.12708/86996
  • First Order Interpolation / Kovacs, L. (2019). First Order Interpolation. SAT/SMT/AR Summer School 2019, Lisbon, Portugal. http://hdl.handle.net/20.500.12708/86994
  • Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire / Gleiss, B., Kovacs, L., & Rath, J. (2019). Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire. Vampire 2019 - The Sixth Vampire Workshop, Lisbon, Portugal. http://hdl.handle.net/20.500.12708/86993
  • Verifying Relational Properties using Trace Logic / Kovacs, L. (2019). Verifying Relational Properties using Trace Logic. First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal. http://hdl.handle.net/20.500.12708/86991
  • Symbol Elimination and Vampire / Kovacs, L. (2019). Symbol Elimination and Vampire. Dagstuhl Seminar 19062 - Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving, Schloss Dagstuhl, Germany. http://hdl.handle.net/20.500.12708/86989
  • Foreword - Formalization of geometry, automated and interactive geometric reasoning / Schreck, P., Ida, T., & Kovacs, L. (2019). Foreword - Formalization of geometry, automated and interactive geometric reasoning. Annals of Mathematics and Artificial Intelligence, 85(2–4), 71–72. https://doi.org/10.1007/s10472-019-9617-2
  • Foreword / Davenport, J. H., Kovacs, L., & Zaharie, D. (2019). Foreword. Mathematics in Computer Science, 13(4), 459–460. https://doi.org/10.1007/s11786-019-00411-w
  • APRe, Vampire, Welcome in Vienna! / Kovacs, L. (2019). APRe, Vampire, Welcome in Vienna! APRe 2019 Workshop, TU Wien, TU Wien, Vienna, Austria. http://hdl.handle.net/20.500.12708/86999
  • Interpolation in the Grey Area of Proofs / Kovacs, L. (2019). Interpolation in the Grey Area of Proofs. Helmut Veith Memorial Workshop 2019, Turracher Höhe, Austria. http://hdl.handle.net/20.500.12708/86995

2018

  • Loop Analysis by Quantification over Iterations / Gleiss, B., Kovács, L., & Robillard, S. (2018). Loop Analysis by Quantification over Iterations. In G. Barthe, G. Sutcliffe, & M. Veanes (Eds.), EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/269p
  • Automated Reasoning for Systems Engineering / Kovacs, L. (2018). Automated Reasoning for Systems Engineering. In Foundations of Information and Knowledge Systems (FOIKS) 2018 (p. 1). LNCS. http://hdl.handle.net/20.500.12708/57375
  • A FOOLish Encoding of the Next State Relations of Imperative Programs / Kotelnikov, E., Kovács, L., & Voronkov, A. (2018). A FOOLish Encoding of the Next State Relations of Imperative Programs. In Automated Reasoning (pp. 405–421). LNCS. https://doi.org/10.1007/978-3-319-94205-6_27
  • First-Order Interpolation / Kovacs, L. (2018). First-Order Interpolation. SAT/SMT/AR Summer School 2018, Manchester, United Kingdom of Great Britain and Northern Ireland (the). http://hdl.handle.net/20.500.12708/86712
  • Automated Reasoning for Systems Engineering / Kovacs, L. (2018). Automated Reasoning for Systems Engineering. 2018 IEEE International Conference on Future IoT Technologies (Future IoT 2018), Eger, Hungary. http://hdl.handle.net/20.500.12708/86713
  • First-Order Interpolation in the Grey Area of Proofs / Kovacs, L. (2018). First-Order Interpolation in the Grey Area of Proofs. Summer School on Syntax meets Semantics - Methods, Interactions, and Connections in Substructural Logics (SYSMICS), Les Diablerets, Switzerland. http://hdl.handle.net/20.500.12708/86840
  • Symbol Elimination for Program Analysis / Kovacs, L. (2018). Symbol Elimination for Program Analysis. Highlights of Logic, Games and Automata, Paris, France. http://hdl.handle.net/20.500.12708/86841
  • Symbol Elimination in Program Analysis / Kovacs, L. (2018). Symbol Elimination in Program Analysis. 2nd Facebook Testing and Veri cation Symposium (FaceTAV), London, United Kingdom of Great Britain and Northern Ireland (the). http://hdl.handle.net/20.500.12708/86842
  • Local proofs and AVATAR / Reger, G., & Suda, M. (2018). Local proofs and AVATAR. In L. Kovacs & A. Voronkov (Eds.), EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/qgdk
  • First-Order Theorem Proving in Rigorous Systems Engineering / Kovacs, L., & Voronkov, A. (2018). First-Order Theorem Proving in Rigorous Systems Engineering. RiSE/SHiNE Winter School 2018, Wien, Austria. http://hdl.handle.net/20.500.12708/86711
  • Vampire 2017. Proceedings of the 4th Vampire Workshop / Kovacs, L., & Voronkov, A. (Eds.). (2018). Vampire 2017. Proceedings of the 4th Vampire Workshop. EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/24544
  • Invariant Generation for Multi-Path Loops with Polynomial Assignments / Humenberger, A., Jaroschek, M., & Kovacs, L. (2018). Invariant Generation for Multi-Path Loops with Polynomial Assignments. In I. Dillig & J. Palsberg (Eds.), Verification, Model Checking, and Abstract Interpretation (pp. 226–246). Springer. https://doi.org/10.1007/978-3-319-73721-8_11
  • Aligator.jl – A Julia Package for Loop Invariant Generation / Humenberger, A., Jaroschek, M., & Kovács, L. (2018). Aligator.jl – A Julia Package for Loop Invariant Generation. In F. Rabe (Ed.), Intelligent Computer Mathematics : 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings (pp. 111–117). LNCS. https://doi.org/10.1007/978-3-319-96812-4_10
  • Automated Reasoning for Rigorous Systems Engineering / Kovacs, L. (2018). Automated Reasoning for Rigorous Systems Engineering. RiSE/SHINE Media Seminar 2018, Vienna, Austria. http://hdl.handle.net/20.500.12708/86714

2017

  • Symbol Elimination for Program Analysis / Kovacs, L. (2017). Symbol Elimination for Program Analysis. ETH Workshop on Software Correctness and Reliability, Zürich, Switzerland. http://hdl.handle.net/20.500.12708/86690
  • Coming to Terms with Quantified Reasoning / Kovacs, L., Robillard, S., & Voronkov, A. (2017). Coming to Terms with Quantified Reasoning. In G. Castagna & A. D. Gordon (Eds.), Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM. https://doi.org/10.1145/3009837
  • Splitting Proofs for Interpolation / Gleiss, B., Kovács, L., & Suda, M. (2017). Splitting Proofs for Interpolation. In Automated Deduction – CADE 26 (pp. 291–309). Springer. https://doi.org/10.1007/978-3-319-63046-5_18
  • Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences / Humenberger, A., Jaroschek, M., & Kovács, L. (2017). Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. In Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation. International Symposium on Symbolic and Algebraic Computation (ISSAC), Kaiserslautern, Germany. ACM. https://doi.org/10.1145/3087604.3087623
  • A Supervisory Control Algorithm Based on Property-Directed Reachability / Claessen, K., Kilhamn, J., Kovács, L., & Lennartson, B. (2017). A Supervisory Control Algorithm Based on Property-Directed Reachability. In O. Strichman & R. Tzoref-Brill (Eds.), Hardware and Software: Verification and Testing (pp. 115–130). Lecture Notes in Computer Science / Springer. https://doi.org/10.1007/978-3-319-70389-3_8
  • Algebraic Reasoning for Program Analysis / Kovacs, L. (2017). Algebraic Reasoning for Program Analysis. 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS), Laibach, Slovenia. http://hdl.handle.net/20.500.12708/86689
  • Polynomial Invariant Generation for Multi-Path Loops / Humenberger, A., Jaroschek, M., & Kovacs, L. (2017). Polynomial Invariant Generation for Multi-Path Loops. Second International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Kaiserslautern, Germany. http://hdl.handle.net/20.500.12708/86847
  • Global Subsumption Revisited (Briefly) / Reger, G., & Suda, M. (2017). Global Subsumption Revisited (Briefly). In L. Kovacs & A. Voronkov (Eds.), Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop (pp. 61–73). http://hdl.handle.net/20.500.12708/57133
  • First-Order Interpolation and Interpolating Proof Systems / Kovacs, L., & Voronkov, A. (2017). First-Order Interpolation and Interpolating Proof Systems. In LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 49–64). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/57308
  • Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds Using Symbolic Execution / Knoop, J., Kovács, L., & Zwirchmayr, J. (2017). Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds Using Symbolic Execution. Journal of Symbolic Computation, 80, 101–124. https://doi.org/10.1016/j.jsc.2016.07.023
    Download: PDF (875 KB)
  • First-Order Interpolation and Grey Areas of Proofs (Invited Talk) / Kovacs, L. (2017). First-Order Interpolation and Grey Areas of Proofs (Invited Talk). In V. Goranko & M. Dam (Eds.), 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). DROPS. https://doi.org/10.4230/LIPIcs.CSL.2017.3
    Download: PDF (206 KB)

2016

  • A Clausal Normal Form Translation for FOOL / Kotelnikov, E., Kovacs, L., Suda, M., & Voronkov, A. (2016). A Clausal Normal Form Translation for FOOL. In GCAI 2016. 2nd Global Conference on Artificial Intelligence (pp. 53–71). EasyChair. http://hdl.handle.net/20.500.12708/56716
  • The vampire and the FOOL / Kotelnikov, E., Kovács, L., Reger, G., & Voronkov, A. (2016). The vampire and the FOOL. In J. Avigad & A. Chlipala (Eds.), Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. ACM. https://doi.org/10.1145/2854065.2854071
  • Symbolic Computation and Automated Reasoning for Program Analysis / Kovács, L. (2016). Symbolic Computation and Automated Reasoning for Program Analysis. In E. Abraham & M. Huisman (Eds.), Integrated Formal Methods : 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings (pp. 20–27). Springer / LNCS. https://doi.org/10.1007/978-3-319-33693-0_2
  • Automated Reasoning for Systems Engineering / Kovacs, L. (2016). Automated Reasoning for Systems Engineering. Austrian Computer Science Day 2018, Salzburg, Austria. http://hdl.handle.net/20.500.12708/86695
  • With a Timisoara Background in the Scientific World of Computer Science and / Kovacs, L. (2016). With a Timisoara Background in the Scientific World of Computer Science and. Timisoara Hungarian Science Festival, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/86440
  • Enjoying Research at the Intersection of Math and Computer Science / Kovacs, L. (2016). Enjoying Research at the Intersection of Math and Computer Science. Women in Science Workshop Series (WISE), Gothenburg, Schweden, EU. http://hdl.handle.net/20.500.12708/86439
  • First-Order Theorem Proving and Vampire / Kovacs, L. (2016). First-Order Theorem Proving and Vampire. Spring School on Logic and Verification - LoVE, Vienna, Austria, Austria. http://hdl.handle.net/20.500.12708/86438

2015

  • Reasoning About Loops Using Vampire in KeY / Ahrendt, W., Kovacs, L., & Robillard, S. (2015). Reasoning About Loops Using Vampire in KeY. In M. Davis, A. Fehnker, A. McIver, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings. LNCS. https://doi.org/10.1007/978-3-662-48899-7_30
  • A First Class Boolean Sort in First-Order Theorem Proving and TPTP / Kotelnikov, E., Kovacs, L., & Voronkov, A. (2015). A First Class Boolean Sort in First-Order Theorem Proving and TPTP. In M. Kerber (Ed.), Intelligent Computer Mathematics International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. LNCS. https://doi.org/10.1007/978-3-319-20615-8_5
  • Segment Abstraction for Worst-Case Execution Time Analysis / Cerny, P., Henzinger, T. A., Kovacs, L., Radhakrishna, A., & Zwirchmayr, J. (2015). Segment Abstraction for Worst-Case Execution Time Analysis. In J. Vitek (Ed.), Programming Languages and Systems 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. LNCS. https://doi.org/10.1007/978-3-662-46669-8_5
  • Foreword to the Special Issue on Symbolic Computation in Software Science / Bouhoula, A., Buchberger, B., Kovács, L., & Kutsia, T. (2015). Foreword to the Special Issue on Symbolic Computation in Software Science. Journal of Symbolic Computation, 69, 1–2. https://doi.org/10.1016/j.jsc.2014.09.027
  • Symbol Elimination for Program Analysis / Kovacs, L. (2015). Symbol Elimination for Program Analysis. Dagstuhl Seminar 15471 on “Symbolic Computation and Satisfiability Checking,” Dagstuhl, Germany, EU. http://hdl.handle.net/20.500.12708/86263
  • Symbol Elimination for Program Analysis / Kovacs, L. (2015). Symbol Elimination for Program Analysis. Theoretical Computer Science Seminar Series of the KTH Royal Institute of Technology, Stockholm, Sweden, EU. http://hdl.handle.net/20.500.12708/86262
  • vanHelsing: A Fast Proof Checker for Debuggable Compiler Verification / Lezuo, R., Dragan, I., Barany, G., & Krall, A. (2015). vanHelsing: A Fast Proof Checker for Debuggable Compiler Verification. In L. Kovacs & D. Zaharie (Eds.), 2015 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). https://doi.org/10.1109/synasc.2015.34
  • First-Order Theorem Proving and Program Analysis / Kovacs, L. (2015). First-Order Theorem Proving and Program Analysis. In J. Baras (Ed.), Proc. of the LCCC-ACCESS workshop on Model-Based Engineering (pp. 192–217). http://hdl.handle.net/20.500.12708/56444
  • Special issue on symbolic computation in software science / Special issue on symbolic computation in software science. (2015). In A. Bouhoula, B. Buchberger, L. Kovacs, & T. Kutsia (Eds.), Journal of Symbolic Computation (p. 2). Elsevier. https://doi.org/10.1016/j.jsc.2014.09.027

2014

  • Extensional Crisis and Proving Identity / Gupta, A., Kovács, L., Kragl, B., & Voronkov, A. (2014). Extensional Crisis and Proving Identity. In F. Cassez & J.-F. Raskin (Eds.), Automated Technology for Verification and Analysis (pp. 185–200). Lecture Notes in Computer Science, Springer Verlag. https://doi.org/10.1007/978-3-319-11936-6_14
  • Experimenting with SAT Solvers in Vampire / Biere, A., Dragan, I., Kovács, L., & Voronkov, A. (2014). Experimenting with SAT Solvers in Vampire. In Human-Inspired Computing and its Applications 13th Mexican International Conference on Artificial Intelligence, MICAI2014, Tuxtla Gutiérrez, Mexico, November 16-22, 2014. Proceedings, Part I (pp. 431–442). https://doi.org/10.1007/978-3-319-13647-9_39
  • Symbol Elimination for Automated Generation of Program Properties / Kovacs, L. (2014). Symbol Elimination for Automated Generation of Program Properties. ECEASST, ECEASST(70), 1–2. http://hdl.handle.net/20.500.12708/157934
  • Von Vertrauen zum Beweis - Über funktionale Programmkorrektheit hinaus / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2014). Von Vertrauen zum Beweis - Über funktionale Programmkorrektheit hinaus. Festkolloquium zum 80. Geburtstag von Prof. Dr. Dr.h.c. Hans Langmaack, Christian-Albrechts-Universität zu Kiel, Deutschland, EU. http://hdl.handle.net/20.500.12708/85806
  • Replacing Conjectures by Positive Knowledge: Inferring and Proving Precision of Worst-Case Execution Time Bounds using Symbolic Execution / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2014). Replacing Conjectures by Positive Knowledge: Inferring and Proving Precision of Worst-Case Execution Time Bounds using Symbolic Execution. 3rd Joint Meeting of EU FP7 COST Action IC1202 Timing Analysis on Code-Level (TACLe), Vienna, Austria. http://hdl.handle.net/20.500.12708/85811
  • The Five P's of Inferring Proven Precise Worst-Case Execution Time Bounds / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2014). The Five P’s of Inferring Proven Precise Worst-Case Execution Time Bounds. 55th Meeting of the IFIP Working Group 2.4 Software Implementation Technology, Stellenbosch, Non-EU. http://hdl.handle.net/20.500.12708/86020
  • Lingva: Generating and Proving Program Properties using Symbol Elimination / Dragan, I., & Kovacs, L. (2014). Lingva: Generating and Proving Program Properties using Symbol Elimination. In 9th International Andrei Ershov Memorial Conference - Perspectives of System Informatics (PSI 2014). Springer LNCS. http://hdl.handle.net/20.500.12708/55992
  • Supervisory Control of Discrete-Event Systems via IC3 / Shoaei, M. R., Kovács, L., & Lennartson, B. (2014). Supervisory Control of Discrete-Event Systems via IC3. In E. Yahav (Ed.), Hardware and Software: Verification and Testing (pp. 252–266). Springer Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-319-13338-6_19

2013

  • Bound Propagation for Arithmetic Reasoning in Vampire / Dragan, I., Korovin, K., Kovacs, L., & Voronkov, A. (2013). Bound Propagation for Arithmetic Reasoning in Vampire. In Proceedings of the 15th International Conference on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/55050
  • First-Order Theorem Proving and Vampire / Kovács, L., & Voronkov, A. (2013). First-Order Theorem Proving and Vampire. In N. Sharygina & H. Veith (Eds.), Computer Aided Verification (pp. 1–35). Springer LNCS 8044. https://doi.org/10.1007/978-3-642-39799-8_1
  • The Inverse Method for Many-Valued Logics / Kovács, L., Mantsivoda, A., & Voronkov, A. (2013). The Inverse Method for Many-Valued Logics. In F. Castro, A. Gelbukh, & M. Gonzalez (Eds.), Advances in Artificial Intelligence and Its Applications (pp. 12–23). Springer LNCS 8265. https://doi.org/10.1007/978-3-642-45114-0_2
  • Tree Interpolation in Vampire / Blanc, R., Gupta, A., Kovács, L., & Kragl, B. (2013). Tree Interpolation in Vampire. In M. Kenneth, A. Middeldorp, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 173–181). Springer LNCS 8312. https://doi.org/10.1007/978-3-642-45221-5_13
  • Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds using Symbolic Execution / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2013). Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds using Symbolic Execution. 2nd International Seminar on Program Verification, Automated Debugging and Symbolic Computation (PAS 2013), Peking, Non-EU. http://hdl.handle.net/20.500.12708/85808
  • The Auspicious Couple: Symbolic Execution and WCET Analysis / Biere, A., Knoop, J., Kovacs, L., & Zwirchmayr, J. (2013). The Auspicious Couple: Symbolic Execution and WCET Analysis. In C. Maiza (Ed.), Pre-Proceedings of the 13th International Workshop on Worst-Case Execution Time Analysis (WCET 2013) (pp. 51–60). http://hdl.handle.net/20.500.12708/54652
  • SmacC: A Retargetable Symbolic Execution Engine / Biere, A., Knoop, J., Kovacs, L., & Zwirchmayr, J. (2013). SmacC: A Retargetable Symbolic Execution Engine. In AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS 11th International Symposium, ATVA 2013. Dang Van Hung and Mizuhito Ogawa, Austria. Springer LNCS 8172. http://hdl.handle.net/20.500.12708/54744
  • Editorial to the Special issue on Automated Specification and Verification of Web Systems / Kovács, L., Pugliese, R., Silva, J., & Tiezzi, F. (2013). Editorial to the Special issue on Automated Specification and Verification of Web Systems. The Journal of Logic and Algebraic Programming, 82(8), 241–242. https://doi.org/10.1016/j.jlap.2013.05.007
  • Formal Methods for Program Verification / Kovacs, L. (2013). Formal Methods for Program Verification. SAAB/Chalmers joint research seminar, SAAB Kallebäck, Schweden, EU. http://hdl.handle.net/20.500.12708/85756
  • Formal Methods in Software Design and Verification / Kovacs, L. (2013). Formal Methods in Software Design and Verification. SAAB Technical Seminar, Linköping, Schweden, EU. http://hdl.handle.net/20.500.12708/85755
  • WCET Squeezing by On-demand Feasibility Refinement / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2013). WCET Squeezing by On-demand Feasibility Refinement. 53rd Meeting of the IFIP Working Group 2.4 “Software Implementation Technology,” Mysore, Non-EU. http://hdl.handle.net/20.500.12708/85551
  • WCET Squeezing: On-demand Feasibility Refinement for Proven Precise WCET-bounds / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2013). WCET Squeezing: On-demand Feasibility Refinement for Proven Precise WCET-bounds. In 21st International Conference on Real-Time Networks and Systems. Acm Dl. http://hdl.handle.net/20.500.12708/54743
  • A Parametric Interpolation Framework for First-Order Theories / Kovacs, L., Sharygina, N., & Rollini, S. F. (2013). A Parametric Interpolation Framework for First-Order Theories. In F. Castro, A. Gelbukh, & M. Gonzalez (Eds.), Advances in Artificial Intelligence and Its Applications (pp. 24–40). Springer LNCS 8265. https://doi.org/10.1007/978-3-642-45114-0_3
  • 5th International Symposium on Symbolic Computation in Software Science / Kovacs, L., & Kutsia, T. (Eds.). (2013). 5th International Symposium on Symbolic Computation in Software Science. EasyChair. http://hdl.handle.net/20.500.12708/23783
  • 6th International Workshop on Automated Specification and Verification of Web Systems (WWV) / Kovacs, L., & Kutsia, T. (Eds.). (2013). 6th International Workshop on Automated Specification and Verification of Web Systems (WWV). EasyChair. http://hdl.handle.net/20.500.12708/23784
  • Special issue on Automated Specification and Verification of Web Systems / Special issue on Automated Specification and Verification of Web Systems. (2013). In L. Kovacs, R. Pugliese, J. Silva, & F. Tiezzi (Eds.), The Journal of Logic and Algebraic Programming (p. 242). Elsevier. https://doi.org/10.1016/j.jlap.2013.05.007

2012

  • Foreword / Bjørner, N., & Kovacs, L. (2012). Foreword. Journal of Symbolic Computation, 47(12), 1413–1415. https://doi.org/10.1016/j.jsc.2011.12.047
  • Vinter: A Vampire-Based Tool for Interpolation / Hoder, K., Holzer, A., Kovács, L., & Voronkov, A. (2012). Vinter: A Vampire-Based Tool for Interpolation. In Programming Languages and Systems (pp. 148–156). Springer / LNCS. https://doi.org/10.1007/978-3-642-35182-2_11
  • Playing in the grey area of proofs / Hoder, K., Kovacs, L., & Voronkov, A. (2012). Playing in the grey area of proofs. In J. Field & M. Hicks (Eds.), Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’12. ACM. https://doi.org/10.1145/2103656.2103689
  • r-TuBound: Loop Bounds for WCET Analysis (Tool Paper) / Zwirchmayr, J., Knoop, J., & Kovacs, L. (2012). r-TuBound: Loop Bounds for WCET Analysis (Tool Paper). In N. Bjørner & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 435–444). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-642-28717-6_34
  • Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops / Bjørner, N., & Kovacs, L. (Eds.). (2012). Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops (p. 1415). Springer. https://doi.org/10.1016/j.jsc.2011.12.047
  • Special issue on Automated Specification and Verification of Web Systems / Kovács, L., & Kutsia, T. (2012). Special issue on Automated Specification and Verification of Web Systems. Journal of Applied Logic, 10(1), 1. https://doi.org/10.1016/j.jal.2011.11.001
  • FFX: A Portable WCET Annotation Language / Zwirchmayr, J., Kovacs, L., Knoop, J., Bonenfant, A., Cassé, H., & Rochange, C. (2012). FFX: A Portable WCET Annotation Language. In 20th International Conference on Real-Time and Network Systems (pp. 91–100). ACM. http://hdl.handle.net/20.500.12708/54270
  • Portable Worst-Case Execution Time Analysis / Bonenfant, A., Cassé, H., de Michiel, M., Knoop, J., Kovacs, L., & Zwirchmayr, J. (2012). Portable Worst-Case Execution Time Analysis. 53rd Meeting of the IFIP Working Group 2.4 Software Implementation Technology, Vadstena, Schweden, EU. http://hdl.handle.net/20.500.12708/85538
  • Portable Worst-Case Execution Time Analysis via Flow Facts in XML / Bonenfant, A., Cassé, H., de Michiel, M., Knoop, J., Kovacs, L., & Zwirchmayr, J. (2012). Portable Worst-Case Execution Time Analysis via Flow Facts in XML. 29th Annual Workshop of the GI-Fachgruppe “Programmiersprachen und Rechenkonzepte,” Bad Honnef, Deutschland, EU. http://hdl.handle.net/20.500.12708/85537
  • Playing in the Grey Area of Proofs / Kovacs, L. (2012). Playing in the Grey Area of Proofs. Rigorous System Engineering Seminar IST/TU Wien, Vienna, Austria. http://hdl.handle.net/20.500.12708/85493
  • Playing in the Grey Area of Proofs / Kovacs, L. (2012). Playing in the Grey Area of Proofs. Research Seminar at VERIMAG Grenoble, Grenoble, France, EU. http://hdl.handle.net/20.500.12708/85492
  • Playing in the Grey Area of Proofs / Kovacs, L. (2012). Playing in the Grey Area of Proofs. Research Seminar at Microsoft Research Cambridge, Cambridge, UK, EU. http://hdl.handle.net/20.500.12708/85490
  • Symbol Elimination in Program Analysis / Kovacs, L. (2012). Symbol Elimination in Program Analysis. International Seminar on Program Verification, Automated Debugging and Symbolic Computation (PAS), Beijing, China, Non-EU. http://hdl.handle.net/20.500.12708/85489
  • Automated Theorem Proving - An Introduction / Kovacs, L. (2012). Automated Theorem Proving - An Introduction. ARiSE/VCLA Winter School on Verification, Wien, Austria. http://hdl.handle.net/20.500.12708/85319
  • Automated Theorem Proving - with some Applications to Verification / Kovacs, L. (2012). Automated Theorem Proving - with some Applications to Verification. ARiSE/VCLA Winter School on Verification, Wien, Austria. http://hdl.handle.net/20.500.12708/85316
  • Solving Robust Glucose-Insulin Control by Dixon Resultant Computations / Kovacs, L., Palancz, B., & Kovacs, L. (2012). Solving Robust Glucose-Insulin Control by Dixon Resultant Computations. In Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scienti c Computing (SYNASC 2012). 14th International Symposium on Symbolic and Numeric Algorithms for Scienti c Computing (SYNASC 2012), Timisoara, Romania, EU. IEEE Proceedings. http://hdl.handle.net/20.500.12708/54508
  • The Boundary Element Method in the Study of Non-Stationary Movements Through Network Pro les / Kovacs, A., Kovacs, L., & Kovacs, L. (2012). The Boundary Element Method in the Study of Non-Stationary Movements Through Network Pro les. In Proceedings of 13th International Conference on Mathematics and its Applications. (pp. 241–248). Scientific Bulletin of Politehnica University Timisoara, Romania. http://hdl.handle.net/20.500.12708/54506
  • Examples of Symbol Elimination in Program Verification / Kovacs, L., & Kovacs, A. (2012). Examples of Symbol Elimination in Program Verification. In Proceedings of 13th International Conference on Mathematics and its Applications (pp. 145–150). Scientific Bulletin of Politehnica University Timisoara, Romania. http://hdl.handle.net/20.500.12708/54507
  • A Hodographic Approximation Method for Analyzing the Fluid Motion Through Network Pro files / Kovacs, A., & Kovacs, L. (2012). A Hodographic Approximation Method for Analyzing the Fluid Motion Through Network Pro files. In Annals of DAAAM for 2012 & Proceedings of the 23rd International DAAAM Symposium (p. 4). DAAAM International, Vienna, Austria. http://hdl.handle.net/20.500.12708/54505
  • Symbol Elimination in Program Analysis / Kovacs, L. (2012). Symbol Elimination in Program Analysis. In D. Wang, V. Negru, T. Ida, T. Jebelean, D. Petcu, S. M. Watt, & D. Zaharie (Eds.), Proc. of 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) (pp. 12–13). IEEE Computer Society. http://hdl.handle.net/20.500.12708/54061
  • Symbolic Loop Bound Computation for WCET Analysis / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2012). Symbolic Loop Bound Computation for WCET Analysis. In Ershov Informatic Conference, PSI Series, 8th Edition (pp. 224–239). Springer-Verlag, Lecture Notes in Computer Science. http://hdl.handle.net/20.500.12708/53669
  • Special Issue on Automated Speci cation and Veri cation of Web Systems / Kovacs, L., & Kutsia, T. (Eds.). (2012). Special Issue on Automated Speci cation and Veri cation of Web Systems. Elsevier B.V. http://hdl.handle.net/20.500.12708/23614

2011

  • Case Studies on Invariant Generation Using a Saturation Theorem Prover / Hoder, K., Kovacs, L., & Voronkov, A. (2011). Case Studies on Invariant Generation Using a Saturation Theorem Prover. In I. Z. Batyrshin & G. Sidorov (Eds.), Advances in Artificial Intelligence - 10th Mexican International Conference on Artificial Intelligence (MICAI) (pp. 1–15). Springer. http://hdl.handle.net/20.500.12708/54058
  • Invariant Generation in Vampire / Hoder, K., Kovacs, L., & Voronkov, A. (2011). Invariant Generation in Vampire. In Proc. of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (pp. 60–64). Springer. http://hdl.handle.net/20.500.12708/54052
  • First-order theorem proving and Vampire / Kovacs, L., & Voronkov, A. (2011). First-order theorem proving and Vampire. 10th Mexican International Conference on Artificial Intelligence (MICAI), Puebla, Mexico, Non-EU. http://hdl.handle.net/20.500.12708/85275
  • Invariant Generation using Theorem Proving / Kovacs, L., & Voronkov, A. (2011). Invariant Generation using Theorem Proving. 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/85273
  • First-order theorem proving and Vampire / Hoder, K., Kovacs, L., & Voronkov, A. (2011). First-order theorem proving and Vampire. 23rd International Conference on Automated Deduction (CADE-23), Wroclaw, Poland, EU. http://hdl.handle.net/20.500.12708/85270
  • On Transfinite Knuth-Bendix Orders / Kovacs, L., Moser, G., & Voronkov, A. (2011). On Transfinite Knuth-Bendix Orders. In N. Bjørner & V. Sofronie-Stokkermans (Eds.), Proc. of the 23rd International Conference on Automated Deduction (CADE-23) (pp. 384–399). Springer. http://hdl.handle.net/20.500.12708/54018
  • First-order theorem proving and Vampire / Kovacs, L. (2011). First-order theorem proving and Vampire. RiSE-PUMA Workshop, Traunkirchen, Austria, EU. http://hdl.handle.net/20.500.12708/85274
  • Program Assertion Synthesis using Symbolic Computation / Kovacs, L. (2011). Program Assertion Synthesis using Symbolic Computation. 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/85272
  • Symbol Elimination in Program Analysis / Kovacs, L. (2011). Symbol Elimination in Program Analysis. Helsinki Institute for Information Technology (HIIT), Helsinki, Finnland, EU. http://hdl.handle.net/20.500.12708/85271
  • Interpolation and Symbol Elimination / Kovacs, L. (2011). Interpolation and Symbol Elimination. TU Graz, Austria. http://hdl.handle.net/20.500.12708/85269
  • RiSE: Rigorous Systems Engineering / Kovacs, L. (2011). RiSE: Rigorous Systems Engineering. Research Seminar for Master Students, West University of Timisoara, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/85268
  • Experiments with Invariant Generation Using a Saturation Theorem Prover / Kovacs, L. (2011). Experiments with Invariant Generation Using a Saturation Theorem Prover. AdaCore Paris, Paris, France, EU. http://hdl.handle.net/20.500.12708/85267
  • Experiments with Invariant Generation Using a Saturation Theorem Prover / Kovacs, L. (2011). Experiments with Invariant Generation Using a Saturation Theorem Prover. “Deduction at Scale” Seminar, Ringberg Castle, Germany, EU. http://hdl.handle.net/20.500.12708/85266
  • Proceedings of the 7th International Workshop on Automated Specification and Verification of Web Systems / Kovacs, L., Pugliese, R., & Tiezzi, F. (Eds.). (2011). Proceedings of the 7th International Workshop on Automated Specification and Verification of Web Systems. EPTCS Vol. 61. https://doi.org/10.48550/arXiv.1108.2085
  • Aligator: Experiments and Limitations / Kovacs, L., & Kovacs, A. (2011). Aligator: Experiments and Limitations. In Proc. of the 22nd International DAAAM Symposium: “Intelligent Manufactoring and Automation: Power of Knowledge and Creativity” (pp. 1145–1146). DAAAM International. http://hdl.handle.net/20.500.12708/54065
  • Analyzing the Fluid Motion Through Network Profiles Using the Boundary Element Method / Kovacs, A., & Kovacs, L. (2011). Analyzing the Fluid Motion Through Network Profiles Using the Boundary Element Method. In Proc. of the 22nd International DAAAM Symposium: “Intelligent Manufactoring and Automation: Power of Knowledge and Creativity” (pp. 1147–1148). DAAAM International, Volume 22, Nr. 1. http://hdl.handle.net/20.500.12708/54062
  • An Evaluation of WCET Analysis using Symbolic Loop Bounds (abstract/presentation) / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2011). An Evaluation of WCET Analysis using Symbolic Loop Bounds (abstract/presentation). In Tagungsband 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS’11) (p. 200). Westfälische Wilhelms-Universität Münster. http://hdl.handle.net/20.500.12708/54044
  • An Evaluation of WCET Analysis using Symbolic Loop Bounds (extended Abstract) / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2011). An Evaluation of WCET Analysis using Symbolic Loop Bounds (extended Abstract). In MEMICS Proceedings (p. 119). http://hdl.handle.net/20.500.12708/54021
  • Practical Experiments with Symbolic Loop Bound Computation for WCET Analysis / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2011). Practical Experiments with Symbolic Loop Bound Computation for WCET Analysis. In 28. Workshop der GI-Fachgruppe Programmiersprachen & Rechenkonzepte. 28. Workshop der GI-Fachgruppe “Programmiersprachen und Rechenkonzepte,” Bad Honnef, EU. Technischer Bericht des Instituts für Informatik der Christian-Albrechts Universität zu Kiel. http://hdl.handle.net/20.500.12708/53670
  • An Evaluation of WCET Analysis using Symbolic Loop Bounds / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2011). An Evaluation of WCET Analysis using Symbolic Loop Bounds. In C. Healy (Ed.), Proc. 11’th International Workshop on Worst-Case Execution Time Analysis (pp. 93–103). Österreichische Computer Gesellschaft - OCG. http://hdl.handle.net/20.500.12708/53668

2010

 

2025

2024

2023

  • Moment-based loop analysis / Stankovic, M. (2023). Moment-based loop analysis [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.113863
    Download: PDF (1.26 MB)
  • Exact inference for probabilistic loops / Müllner, J. (2023). Exact inference for probabilistic loops [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.107471
    Download: PDF (1020 KB)
  • Constraint superposition for higher-order logic / Hetzenberger, M. (2023). Constraint superposition for higher-order logic [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.108280
    Download: PDF (1.3 MB)

2022

2021

2020

2019

2016

  • Interpolation and local proofs / Gleiss, B. (2016). Interpolation and local proofs [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.36061
    Download: PDF (761 KB)

2015

2014

2013