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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L. (2014). Symbol Elimination for Automated Generation of Program Properties. ECEASST, ECEASST(70), 1–2. http://hdl.handle.net/20.500.12708/157934 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Giese, M., Ireland, A., & Kovacs, L. (2010). Introduction to the Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops. Journal of Symbolic Computation, 45(11), 1097–1100. http://hdl.handle.net/20.500.12708/167839 ( reposiTUm)

Eisenhofer, C., Kovacs, 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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Hozzova, 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 ( reposiTUm)

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 ( reposiTUm)

Martina Landman, Sophie Rain, Laura Kovács, & 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 ( reposiTUm)

Bhayat, A., Korovin, K., Kovacs, 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 ( reposiTUm)

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). ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Hajdu, M., Kovacs, 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 ( reposiTUm)

Bjorner, N., Eisenhofer, C., & Kovacs, 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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Humenberger, A., & Kovács, L. (2021). Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). In F. Henglein, S. Shoham, & Y. Vizel (Eds.), Lecture Notes in Computer Science (pp. 17–28). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_2 ( reposiTUm)

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 ( reposiTUm)

Hozzova, P., Kovacs, L., & Voronkov, A. (2021). Integer Induction in Saturation. In Proceedings of CADE 2021 (pp. 361–377). Springer, Cham. https://doi.org/10.34726/1561 ( reposiTUm)

Hozzova, P., Kovacs, 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 ( reposiTUm)

Hajdu, M., Hozzova, P., Kovacs, 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 ( reposiTUm)

Hajdu, M., Hozzova, P., Kovacs, 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 ( reposiTUm)

Kovács, L., Lachnitt, H., & Szeider, S. (2020). Formalizing Graph Trail Properties in Isabelle/HOL. In Lecture Notes in Computer Science (pp. 190–205). LNCS. https://doi.org/10.1007/978-3-030-53518-6_12 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Humenberger, A., Bjørner, N., & Kovacs, L. (2020). Algebra-Based Loop Synthesis. In B. Dongol & E. Troubitsyna (Eds.), Lecture Notes in Computer Science (pp. 440–459). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-63461-2_24 ( reposiTUm)

Hajdú, M., Hozzova, P., Kovacs, 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 ( reposiTUm)

Kovasznai, G., Gajdár, K., & Kovacs, 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 ( reposiTUm)

Damestani, D., Kovacs, 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 ( reposiTUm)

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 ( reposiTUm)

Gleiss, B., Kovács, L., & Schnedlitz, L. (2019). Interactive Visualization of Saturation Attempts in Vampire. In W. Ahrendt & S. Lizeth (Eds.), Lecture Notes in Computer Science (pp. 504–513). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-34968-4_28 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Humenberger, A., Jaroschek, M., & Kovács, L. (2018). Aligator.jl – A Julia Package for Loop Invariant Generation. In F. Rabe (Ed.), Lecture Notes in Computer Science (pp. 111–117). LNCS. https://doi.org/10.1007/978-3-319-96812-4_10 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L. (2017). First-Order Interpolation and Grey Areas of Proofs (Invited Talk). In Proceedings of the 26th EACSL Annual Conference on Computer Science Logic (CSL) ; Goranko, Valentin; Dam, Mats. DROPS. https://doi.org/10.4230/LIPIcs.CSL.2017.3 ( reposiTUm)

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 ( reposiTUm)

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, EU. ACM. https://doi.org/10.1145/3087604.3087623 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Kovács, L. (2016). Symbolic Computation and Automated Reasoning for Program Analysis. In E. Abraham & M. Huisman (Eds.), Lecture Notes in Computer Science (pp. 20–27). Springer / LNCS. https://doi.org/10.1007/978-3-319-33693-0_2 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Cerny, P., Henzinger, T. A., Kovacs, L., Radhakrishna, A., & Zwirchmayr, J. (2015). Segment Abstraction for Worst-Case Execution Time Analysis. In J. Vitek (Ed.), Lecture Notes in Computer Science. LNCS. https://doi.org/10.1007/978-3-662-46669-8 ( reposiTUm)

Ahrendt, W., Kovacs, L., & Robillard, S. (2015). Reasoning About Loops Using Vampire in KeY. In M. Davis, A. Fehnker, A. McIver, & A. Voronkov (Eds.), Lecture Notes in Computer Science. LNCS. https://doi.org/10.1007/978-3-662-48899-7 ( reposiTUm)

Kotelnikov, E., Kovacs, L., & Voronkov, A. (2015). A First Class Boolean Sort in First-Order Theorem Proving and TPTP. In M. Kerber (Ed.), Lecture Notes in Computer Science. LNCS. https://doi.org/10.1007/978-3-319-20615-8 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Biere, A., Dragan, I., Kovács, L., & Voronkov, A. (2014). Experimenting with SAT Solvers in Vampire. In Lecture Notes in Computer Science (pp. 431–442). https://doi.org/10.1007/978-3-319-13647-9_39 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Henzinger, T. A., Hottelier, T., Kovacs, L., & Rybalchenko, A. (2010). Aligators for Arrays (Tool Paper). In Proceedings of the 17th International Conference on Logic for Programming, Arti cial Intelligence and Reasoning (LPAR-17) (pp. 348–356). Springer LNCS 6397. http://hdl.handle.net/20.500.12708/53472 ( reposiTUm)

Blanc, R., Henzinger, T. A., Hottelier, T., & Kovacs, L. (2010). ABC: Algebraic Bound Computation for Loops. In Proceedings of the 16th International Conference on Logic for Programming, Arti cial Intelligence and Reasoning (LPAR-16) (pp. 103–118). Springer LNAI 6355. http://hdl.handle.net/20.500.12708/53469 ( reposiTUm)

Hoder, K., Kovacs, L., & Voronkov, A. (2010). Interpolation and Symbol Elimination in Vampire. In Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010) (pp. 188–195). Springer LNCS 6173. http://hdl.handle.net/20.500.12708/53490 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Giese, M., Ireland, A., & Kovacs, L. (Eds.). (2010). Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops. Elsevier. http://hdl.handle.net/20.500.12708/23225 ( reposiTUm)

Meinke, K., & Kovacs, L. (Eds.). (2022). Tests and Proofs (Vol. 13361). Springer-Verlag. https://doi.org/10.1007/978-3-031-09827-7 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L., & Kutsia, T. (Eds.). (2013). 5th International Symposium on Symbolic Computation in Software Science. EasyChair. http://hdl.handle.net/20.500.12708/23783 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L., & Kutsia, T. (Eds.). (2010). Proceedings of the 6th International Workshop on Automated Specification and Verification of Web Systems (WWV’10). Eigenverlag. http://hdl.handle.net/20.500.12708/23271 ( reposiTUm)

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. ( reposiTUm)

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. ( reposiTUm)

Kovacs, L. (2022, May 30). Automated Program Reasoning [Keynote Presentation]. Informatics Europe Webinar Series, Switzerland. ( reposiTUm)

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. ( reposiTUm)

Kovacs, L. (2022, April 3). Enjoying Research at the Intersection of Math and Computer Science [Keynote Presentation]. ETAPS 2022 Mentoring Workshop, Munich, Germany. ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L. (2019). Symbol Elimination and Vampire. Dagstuhl Seminar 19062 - Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving, Schloss Dagstuhl, Germany, EU. http://hdl.handle.net/20.500.12708/86989 ( reposiTUm)

Kovacs, L. (2019). 60 Shades of Grey in Vampire. ANDREI-60: Automating New-Era Deductive Reasoning Event in Iberia, Tbilisi, Georgia, Non-EU. http://hdl.handle.net/20.500.12708/86990 ( reposiTUm)

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, US, Non-EU. http://hdl.handle.net/20.500.12708/86988 ( reposiTUm)

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, EU. http://hdl.handle.net/20.500.12708/86991 ( reposiTUm)

Gleiss, B., Kovacs, L., & Rath, J. (2019). Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire. Vampire 2019 - The Sixth Vampire Workshop, Lisbon, Portugal, EU. http://hdl.handle.net/20.500.12708/86993 ( reposiTUm)

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, EU. http://hdl.handle.net/20.500.12708/86996 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L. (2019). First Order Interpolation. SAT/SMT/AR Summer School 2019, Lisbon, Portugal, EU. http://hdl.handle.net/20.500.12708/86994 ( reposiTUm)

Kovacs, L. (2019). Formal Methods in the Digital World (in Hungarian). JegKepzes Series of Presentations- Hungarian Scientists from the Bartok Bela Highschool, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/86998 ( reposiTUm)

Kovacs, L. (2019). First-Order Interpolation. PhD Research Seminar in Logic and Computation, Faculty of Informatics, West University of Timisoara, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/86997 ( reposiTUm)

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 ( reposiTUm)

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, EU. http://hdl.handle.net/20.500.12708/86840 ( reposiTUm)

Kovacs, L. (2018). Symbol Elimination for Program Analysis. Highlights of Logic, Games and Automata, Paris, Frankreich, EU. http://hdl.handle.net/20.500.12708/86841 ( reposiTUm)

Kovacs, L. (2018). Symbol Elimination in Program Analysis. 2nd Facebook Testing and Veri cation Symposium (FaceTAV), London, UK, EU. http://hdl.handle.net/20.500.12708/86842 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L. (2018). First-Order Interpolation. SAT/SMT/AR Summer School 2018, Manchester, EU. http://hdl.handle.net/20.500.12708/86712 ( reposiTUm)

Kovacs, L. (2018). Automated Reasoning for Systems Engineering. 2018 IEEE International Conference on Future IoT Technologies (Future IoT 2018), Eger, Hungary, EU. http://hdl.handle.net/20.500.12708/86713 ( reposiTUm)

Kovacs, L. (2018). Automated Reasoning for Rigorous Systems Engineering. RiSE/SHINE Media Seminar 2018, Vienna, Austria. http://hdl.handle.net/20.500.12708/86714 ( reposiTUm)

Kovacs, L. (2017). Algebraic Reasoning for Program Analysis. 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS), Ljubljana, Slovenia, EU. http://hdl.handle.net/20.500.12708/86689 ( reposiTUm)

Kovacs, L. (2017). Symbol Elimination for Program Analysis. ETH Workshop on Software Correctness and Reliability, Zürich, Switzerland, Non-EU. http://hdl.handle.net/20.500.12708/86690 ( reposiTUm)

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, EU. http://hdl.handle.net/20.500.12708/86847 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L. (2016). Automated Reasoning for Systems Engineering. Austrian Computer Science Day 2018, Salzburg, Austria. http://hdl.handle.net/20.500.12708/86695 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L. (2012). Automated Theorem Proving - An Introduction. ARiSE/VCLA Winter School on Verification, Wien, Austria. http://hdl.handle.net/20.500.12708/85319 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L. (2011). First-order theorem proving and Vampire. RiSE-PUMA Workshop, Traunkirchen, Austria, EU. http://hdl.handle.net/20.500.12708/85274 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L. (2011). Interpolation and Symbol Elimination. TU Graz, Austria. http://hdl.handle.net/20.500.12708/85269 ( reposiTUm)

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 ( reposiTUm)

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 ( reposiTUm)

Kovacs, L. (2010). Interpolation and Symbol Elimination. RiSE Workshop, Technical University of Graz, Austria. http://hdl.handle.net/20.500.12708/85043 ( reposiTUm)

Kovacs, L. (2010). Symbol Elimination and Interpolation for Software Verification. Intel Haifa, Haifa, Israel, Non-EU. http://hdl.handle.net/20.500.12708/85045 ( reposiTUm)

Kovacs, L. (2010). Interpolation and Symbol Elimination. Dagstuhl Seminar 10161 on “Decision Procedures in Software, Hardware and Bioware,” Schloss Dagstuhl, Germany, EU. http://hdl.handle.net/20.500.12708/85044 ( reposiTUm)

Kovacs, L. (2010). Quantified Invariant Generation using Symbolic Computation and Theorem Proving. International Workshop on Symbolic Computation and Software Verification (SCSV), Tsukuba University, Japan, Non-EU. http://hdl.handle.net/20.500.12708/85048 ( reposiTUm)

Kovacs, L. (2010). Symbol Elimination and Interpolation. University of Verona, University of Verona, Italy, EU. http://hdl.handle.net/20.500.12708/85046 ( reposiTUm)

Kovacs, L. (2010). Aligators and Arrays. IST/TU Rigorous System Engineering, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85047 ( reposiTUm)

Georgiou, P., Hajdu, M., & Kovacs, L. (2024). Saturating Sorting without Sorts. arXiv. https://doi.org/10.34726/5861 ( reposiTUm)

Kovács, L. (2012). Symbol elimination in program analysis [Professorial Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/159069 ( reposiTUm)