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)

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

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

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., 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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

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

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)

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)

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)

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)

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)

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)

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

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

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)

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)

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

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

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)

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

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)

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)

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.), Verification, Model Checking, and Abstract Interpretation (pp. 17–28). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_2 ( reposiTUm)

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

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

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

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

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)

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

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

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

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

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

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

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

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)

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)

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)

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

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

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)

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

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

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

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

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)

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

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

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)

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

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)

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)

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)

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)

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)

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)

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, 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, 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)

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)

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

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)

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

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)

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)

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)

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)

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)

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)

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

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)

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

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

Kovacs, L. (2022, May 30). Automated Program Reasoning [Keynote Presentation]. Informatics Europe Webinar Series, Switzerland. ( 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, 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)

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

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, 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)

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, 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, 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, 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)

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)

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). 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 ( 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. 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. 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, United States of America (the). http://hdl.handle.net/20.500.12708/86988 ( reposiTUm)

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

Kovacs, L. (2019). First Order Interpolation. SAT/SMT/AR Summer School 2019, Lisbon, Portugal. http://hdl.handle.net/20.500.12708/86994 ( 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). 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 ( reposiTUm)

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 ( 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. http://hdl.handle.net/20.500.12708/86998 ( 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). Automated Reasoning for Rigorous Systems Engineering. RiSE/SHINE Media Seminar 2018, Vienna, Austria. http://hdl.handle.net/20.500.12708/86714 ( 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). Symbol Elimination for Program Analysis. Highlights of Logic, Games and Automata, Paris, France. 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, United Kingdom of Great Britain and Northern Ireland (the). http://hdl.handle.net/20.500.12708/86842 ( 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. http://hdl.handle.net/20.500.12708/86840 ( reposiTUm)

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

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

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

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)

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

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. (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. (2013). Formal Methods in Software Design and Verification. SAAB Technical Seminar, Linköping, Schweden, EU. http://hdl.handle.net/20.500.12708/85755 ( 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. (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)

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

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

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., & 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)

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., & 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. (2010). Interpolation and Symbol Elimination. RiSE Workshop, Technical University of Graz, Austria. http://hdl.handle.net/20.500.12708/85043 ( 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). 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). Aligators and Arrays. IST/TU Rigorous System Engineering, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85047 ( 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)

Georgiou, P., Hajdu, M., & Kovács, 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)