Laura Kovacs
Univ.Prof.in Dr.in techn. / MSc
Research Areas
- verification, invariants, theorem proving, symbolic computation
Roles
-
Head of Research Unit
Formal Methods in Systems Engineering, E192-04 -
Full Professor
Formal Methods in Systems Engineering, E192-04 -
Women in Informatics
Coordinator
Courses
2023W
- Bachelor Thesis / 184.695 / PR
- Doctoral & Master Students Seminar / 181.224 / SE
- Formal Methods in Computer Science / 185.A93 / UE
- Formal Methods in Computer Science / 185.291 / VU
- Introduction to Logical Methods in Computer Science / 184.766 / VO
- Orientation Bachelor with Honors of Informatics and Business Informatics / 180.767 / SE
- Project in Computer Science 1 / 192.021 / PR
- Project in Computer Science 2 / 192.022 / PR
- Research Seminar LogiCS / 184.767 / SE
- Seminar for Master Students in Logic and Computation / 180.773 / SE
2024S
- Bachelor Thesis / 184.695 / PR
- Doctoral & Master Students Seminar / 181.224 / SE
- Introduction to Logical Methods in Computer Science / 184.766 / VO
- Research Seminar LogiCS / 184.767 / SE
- Seminar Formal Methods / 181.221 / SE
Projects
-
Effective Formal Methods for Smart-Contract Certification
2023 – 2027 / Vienna Science and Technology Fund (WWTF) -
Semantic and Cryptographic Foundations of Security and Privacy by Compositional Design
2023 – 2026 / Austrian Science Fund (FWF) -
Abenteuer Informatik für Volksschulen
2023 – 2024 / BUNDESMINISTERIN FÜR FRAUEN, FAMILIE, INTEGRATION UND MEDIEN -
Game-theoretic modelling of the fAsset protocol
2023 / Flare Networks Limited -
Automated Reasoning with Theories and Induction for Software Technologies
2021 – 2026 / European Commission
Publications: 177097 / 154343 / 139734 / 152387 / 144346 / 150329 / 153774 / 150352 / 142174 / 153940 / 153941 / 154268 / 153819 / 153259 / 154161 / 153840 / 153839 / 153838 / 153837 / 153258 / 153836 / 153834 / 146113 / 175984 / 177657 / 18556 / 18557 / 18558 / 19886 / 101800 -
FOREST: First-Order Reasoning for Ensuring System Security
2021 – 2022 / Amazon Research Awards -
Distribution Recovery for Invariant Generation of Probabilistic Programs
2020 – 2025 / Vienna Science and Technology Fund (WWTF)
Publications: 139734 / 146113 / 19886 / 101800 -
Algorithms think differently
2019 – 2022 / Federal Ministry of Transport, Innovation and Technology (bm:vit) -
Symbol Elimination in Reliable System Engineering
2019 – 2020 / European Commission
Publications: 16308 / 16309 / 16998 -
Domain-Specific Reasoning in IoT Applications
2019 – 2020 / DoS-IoT
Publication: 16998 -
Symbolic Computation and Automated Reasoning for Program Analysis
2016 – 2021 / European Commission
Publications: 16308 / 16309 / 16998 / 18556 / 18557 / 18558 -
Interpolation and Symbol Elimination
2011 – 2015 / Austrian Science Fund (FWF) -
Computer Algebra abd Theorem Proving for Verified Software
2010 – 2013 / Austrian Science Fund (FWF) -
Program Verification with Frama-C, Vampire and Aligator
2010 – 2011 / Dassault Aviation, France
Publications
2023
-
From Polynomial Invariants to Linear Loops
/
Kenison, G. J., Kovacs, L., & Varonka, A. (2023). From Polynomial Invariants to Linear Loops. In A. Dickenstein, E. Tsigaridas, & G. Jeronimo (Eds.), ISSAC ’23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation (pp. 398–406). Association for Computing Machinery. https://doi.org/10.1145/3597066.3597109
Projects: ARTIST (2021–2026) / LCS (2017–2025) / ProbInG (2020–2025) -
Satisfiability Modulo Custom Theories in Z3
/
Bjørner, N., Eisenhofer, C., & Kovács, L. (2023). Satisfiability Modulo Custom Theories in Z3. In C. Dragoi, M. Emmi, & J. Wang (Eds.), Verification, Model Checking, and Abstract Interpretation. VMCAI 2023 (pp. 91–105). Springer. https://doi.org/10.1007/978-3-031-24950-1_5
Project: ARTIST (2021–2026)
2022
- Getting Saturated with Induction / Hajdu, M., Hozzová, P., Kovács, L., Reger, G., & Voronkov, A. (2022). Getting Saturated with Induction. In J.-F. Raskin, K. Chatterjee, L. Doyen, & R. Majumdar (Eds.), Principles of Systems Design (Vol. 13660, pp. 306–322). Springer Cham. https://doi.org/10.1007/978-3-031-22337-2_15
-
First-Order Theorem Proving and Vampire
/
Kovacs, L. (2022, December 6). First-Order Theorem Proving and Vampire [Keynote Presentation]. 7th School of Theoretical Computer Science and Formal Methods (ETMF), online, Brazil.
Project: ARTIST (2021–2026) - This Is the Moment for Probabilistic Loops / Moosbrugger, M., Stankovic, M., Bartocci, E., & Kovacs, L. (2022). This Is the Moment for Probabilistic Loops. Proceedings of the ACM on Programming Languages, 6(OOPSLA2), 1497–1525. https://doi.org/10.1145/3563341
-
Symbolic Computation for Software Analysis
/
Kovacs, L. (2022, October 25). Symbolic Computation for Software Analysis [Conference Presentation]. Symposium on the Occasion of the 80th Birthday of RISC-founder Bruno Buchberger, Linz, Austria.
Project: ARTIST (2021–2026) - On the Undecidability of Loop Analysis / Varonka, A., & Kovacs, L. (2022, October 12). On the Undecidability of Loop Analysis [Conference Presentation]. Reachability Problems, Kaiserslautern, Germany. https://doi.org/10.1007/978-3-031-19135-0
-
First-Order Theorem Proving - Theory and Practice
/
Kovacs, L. (2022, October 10). First-Order Theorem Proving - Theory and Practice [Conference Presentation]. Dagstuhl Seminar 22411 on Theory and Practice of SAT and Combinatorial Solving, Dagstuhl, Germany. http://hdl.handle.net/20.500.12708/153840
Project: ARTIST (2021–2026) -
First-Order Subsumption via SAT Solving
/
Rath, J., Biere, A., & Kovacs, L. (2022). First-Order Subsumption via SAT Solving. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 160–169). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_22
Download: PDF (551 KB) -
The RAPID Software Verification Framework
/
Georgiou, P., Gleiss, B., Bhayat, A., Rawson, M., Kovacs, L., & Reger, G. (2022). The RAPID Software Verification Framework. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 255–260). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_32
Download: PDF (308 KB) -
Getting Saturated with Induction
/
Kovacs, L. (2022, September 29). Getting Saturated with Induction [Keynote Presentation]. Automated Reasoning Symposium of Amazon Web Services, United States of America (the). http://hdl.handle.net/20.500.12708/153839
Project: ARTIST (2021–2026) -
Lonely Points in Simplices
/
Jaroschek, M., Kauers, M., & Kovács, L. (2022). Lonely Points in Simplices. Discrete and Computational Geometry, 69, 4–25. https://doi.org/10.1007/s00454-022-00428-2
Project: ARTIST (2021–2026) -
Algebra-Based Analysis of Polynomial Probabilistic Programs
/
Kovacs, L. (2022, September 22). Algebra-Based Analysis of Polynomial Probabilistic Programs [Keynote Presentation]. Distinguished Lecture Series of the Max Planck Institute for Software Systems (MPI-SWS), Germany. http://hdl.handle.net/20.500.12708/153258
Project: ARTIST (2021–2026) - PolySAT - a word-level solver for large bitvectors / Rath, J., Bjørner, N., Kovacs, L., Nutz, A., & Sagiv, M. (2022, September 1). PolySAT - a word-level solver for large bitvectors [Presentation]. Formal Reasoning about Financial Systems, Stanford, United States of America (the). http://hdl.handle.net/20.500.12708/154065
-
The Vampire Approach to Induction (short paper)
/
Hajdu, M., 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
Download: PDF (836 KB) -
User-Propagation for Custom Theories in SMT Solving
/
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
Download: PDF (1.15 MB)
Project: ARTIST (2021–2026) -
Automating Security Analysis of Off-Chain Protocols
/
Brugger, L. S., Kovacs, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2022, August 11). Automating Security Analysis of Off-Chain Protocols [Conference Presentation]. 4th International Workshop on Formal Methods for Blockchains, Haifa, Israel. https://doi.org/10.34726/3523
Download: PDF (265 KB)
Project: ARTIST (2021–2026) -
Automated Reasoning: 11th International Joint Conference (IJCAR 2022)
/
Blanchette, J. C., Kovacs, L., & Pattinson, D. (Eds.). (2022). Automated Reasoning: 11th International Joint Conference (IJCAR 2022) (Vol. 13385). Springer-Verlag. https://doi.org/10.1007/978-3-031-10769-6
Project: ARTIST (2021–2026) -
An SMT Approach for Solving Polynomials over Finite Fields
/
Hader, T., & Kovacs, L. (2022). An SMT Approach for Solving Polynomials over Finite Fields. In Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories (SMT) (pp. 90–98).
Project: ARTIST (2021–2026) -
Automated Reasoning for Trustworthy Software
/
Kovacs, L. (2022, June 21). Automated Reasoning for Trustworthy Software [Keynote Presentation]. Austrian Computer Science Day 2022, IST Austria, Austria. http://hdl.handle.net/20.500.12708/153819
Project: ARTIST (2021–2026) -
First-Order Theorem Proving and Vampire
/
Kovacs, L. (2022, June 17). First-Order Theorem Proving and Vampire [Keynote Presentation]. 15TH SUMMER SCHOOL ON MODELLING AND VERIFICATION OF PARALLEL PROCESSES (MOVEP2022), Aalborg, Denmark. http://hdl.handle.net/20.500.12708/153941
Project: ARTIST (2021–2026) -
Algebraic Synthesis of Loops and their Invariants
/
Kovacs, L. (2022, June 6). Algebraic Synthesis of Loops and their Invariants [Conference Presentation]. Workshop on Differential Algebra, Leipzig, Germany. http://hdl.handle.net/20.500.12708/153259
Project: ARTIST (2021–2026) -
Tests and Proofs
/
Meinke, K., & Kovacs, L. (Eds.). (2022). Tests and Proofs (Vol. 13361). Springer-Verlag. https://doi.org/10.1007/978-3-031-09827-7
Project: ARTIST (2021–2026) -
Automated Program Reasoning
/
Kovacs, L. (2022, May 30). Automated Program Reasoning [Keynote Presentation]. Informatics Europe Webinar Series, Switzerland.
Project: ARTIST (2021–2026) -
Enjoying Research at the Intersection of Math and Computer Science
/
Kovacs, L. (2022, April 3). Enjoying Research at the Intersection of Math and Computer Science [Keynote Presentation]. ETAPS 2022 Mentoring Workshop, Munich, Germany.
Project: ARTIST (2021–2026) -
Algebra-Based Reasoning for Loop Synthesis
/
Humenberger, A., Amrollahi, D., Bjørner, N., & Kovács, L. (2022). Algebra-Based Reasoning for Loop Synthesis. Formal Aspects of Computing, 34(1), 4:31. https://doi.org/10.1145/3527458
Projects: ARTIST (2021–2026) / ProbInG (2020–2025) -
Getting Saturated with Induction
/
Kovacs, L. (2022, January 27). Getting Saturated with Induction [Conference Presentation]. Automated Reasoning Seminar at TU Kaiserslautern, Kaiserslautern, Germany. http://hdl.handle.net/20.500.12708/153837
Project: ARTIST (2021–2026) -
Can Computers Think as Humans?
/
Kovacs, L. (2022, January 26). Can Computers Think as Humans? [Keynote Presentation]. WiSE Talk at the SCIENCE Lecture Series Talks of Wiener Volksshochsculen and City of Vienna, Austria.
Project: ARTIST (2021–2026) - Actions over Core-Closed Knowledge Bases / Cauli, C., Ortiz, M., & Piterman, N. (2022). Actions over Core-Closed Knowledge Bases. In J. Blanchette, L. Kovacs, & D. Pattinson (Eds.), Automated Reasoning. IJCAR 2022 (pp. 281–299). Springer. https://doi.org/10.1007/978-3-031-10769-6_17
- Solving Invariant Generation for Unsolvable Loops / Amrollahi, D., Bartocci, E., Kenison, G., Kovács, L., Moosbrugger, M., & Stankovič, M. (2022). Solving Invariant Generation for Unsolvable Loops. In Static Analysis: 29th International Symposium, SAS 2022 (pp. 19–43). https://doi.org/10.1007/978-3-031-22308-2_3
- Moment-based analysis of Bayesian network properties / Stankovič, M., Bartocci, E., & Kovács, L. (2022). Moment-based analysis of Bayesian network properties. Theoretical Computer Science, 903, 113–133. https://doi.org/10.1016/j.tcs.2021.12.021
2021
-
Induction with Recursive Definitions in Superposition
/
Hajdu, M., 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 (pp. 246–255). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34
Download: PDF (350 KB) -
Automated Generation of Exam Sheets for Automated Deduction
/
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
Download: PDF (458 KB)
Projects: ARTIST (2021–2026) / Symcar (2016–2021) -
Inductive Benchmarks for Automated Reasoning
/
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
Download: PDF (216 KB)
Projects: ARTIST (2021–2026) / Symcar (2016–2021) -
Integer Induction in Saturation
/
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
Download: Preprint submitted for publication as it is (345 KB)
Projects: ARTIST (2021–2026) / Symcar (2016–2021) -
Induction in Saturation-Based Reasoning
/
Kovacs, L. (2021, July 26). Induction in Saturation-Based Reasoning [Keynote Presentation]. 14th Conference on Intelligent Computer Mathematics (CICM 2021), Timisoara, Romania. http://hdl.handle.net/20.500.12708/154161
Project: ARTIST (2021–2026) - The Probabilistic Termination Tool Amber / Marcel Moosbrugger, Ezio Bartocci, Katoen, J.-P., & Laura Kovács. (2021). The Probabilistic Termination Tool Amber. In Formal Methods. FM 2021 (pp. 667–675). https://doi.org/10.1007/978-3-030-90870-6_36
- Automated Termination Analysis of Polynomial Probabilistic Programs / Moosbrugger, M., Bartocci, E., Katoen, J.-P., & Kovács, L. (2021). Automated Termination Analysis of Polynomial Probabilistic Programs. In Programming Languages and Systems (pp. 491–518). Springer. https://doi.org/10.1007/978-3-030-72019-3_18
- Summing up Smart Transitions / Elad, N., Rain, S., Immerman, N., Sagiv, M., & Kovacs, L. (2021). Summing up Smart Transitions. In A. Silva & R. Leino (Eds.), Computer Aided Verification (pp. 317–340). Springer LNCS. https://doi.org/10.1007/978-3-030-81685-8_15
- Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper) / Humenberger, A., & Kovács, L. (2021). Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). In F. Henglein, S. Shoham, & Y. Vizel (Eds.), Lecture Notes in Computer Science (pp. 17–28). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_2
- Automating Induction by Reflection / Schoisswohl, J., & Kovács, L. (2021). Automating Induction by Reflection. In E. Pimentel & E. Tassi (Eds.), Electronic Proceedings in Theoretical Computer Science (pp. 39–54). EPTCS. https://doi.org/10.4204/eptcs.337.4
2020
-
Induction with Generalization in Superposition Reasoning
/
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
Download: Postprint was published at CICM 2020. (300 KB)
Projects: DoS-IoT (2019–2020) / Symcar (2016–2021) / SYMELS (2019–2020) -
Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization
/
Kovasznai, G., Gajdár, K., & 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
Download: accepted version (499 KB)
Projects: Symcar (2016–2021) / SYMELS (2019–2020) -
Superposition Reasoning about Quantified Bitvector Formulas
/
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
Download: accepted version (226 KB)
Projects: Symcar (2016–2021) / SYMELS (2019–2020) - A typed parallel lambda-calculus via 1-depth intermediate proofs / Aschieri, F., Ciabattoni, A., & Genco, F. A. (2020). A typed parallel lambda-calculus via 1-depth intermediate proofs. In L. Kovacs (Ed.), EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/g15z
- RAT Elimination / Rebola Pardo, A., & Weissenbacher, G. (2020). RAT Elimination. In L. Kovacs & E. Albert (Eds.), EPiC Series in Computing. EasyChair. https://doi.org/10.29007/fccb
- Subsumption Demodulation in First-Order Theorem Proving / Gleiss, B., Kovacs, L., & Rath, J. (2020). Subsumption Demodulation in First-Order Theorem Proving. In N. Peltier & V. Sofronie-Stokkermans (Eds.), Automated Reasoning (pp. 297–315). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-51074-9_17
- Algebra-Based Loop Synthesis / Humenberger, A., Bjørner, N., & Kovacs, L. (2020). Algebra-Based Loop Synthesis. In B. Dongol & E. Troubitsyna (Eds.), 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
- ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs / Bartocci, E., Kovacs, L., & Bura, E. (2020). ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs. Vienna Science, Research and Technology Fund - ProbInG, online, Austria. http://hdl.handle.net/20.500.12708/123229
- Formalizing Graph Trail Properties in Isabelle/HOL / 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
- Analysis of Bayesian Networks via Prob-Solvable Loops / Bartocci, E., Kovács, L., & Stankovič, M. (2020). Analysis of Bayesian Networks via Prob-Solvable Loops. In Theoretical Aspects of Computing – ICTAC 2020 (pp. 221–241). Springer. https://doi.org/10.1007/978-3-030-64276-1_12
- Mora - Automatic Generation of Moment-Based Invariants / Bartocci, E., Kovács, L., & Stankovič, M. (2020). Mora - Automatic Generation of Moment-Based Invariants. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 492–498). Springer. https://doi.org/10.1007/978-3-030-45190-5_28
- Trace Logic for Inductive Loop Reasoning / Georgiou, P., Gleiss, B., & 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
- Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23) / Albert, E., & Kovacs, L. (Eds.). (2020). Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/24792
- Proceedings of the 31st International Conference on Concurrency Theory (CONCUR) / Konnov, I., & Kovacs, L. (Eds.). (2020). Proceedings of the 31st International Conference on Concurrency Theory (CONCUR). Dagstuhl Publishing LIPICS. http://hdl.handle.net/20.500.12708/24793
-
Trace Logic for Inductive Loop Reasoning
/
Georgiou, P., Gleiss, B., & Kovacs, L. (2020). Trace Logic for Inductive Loop Reasoning. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 255–263). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_33
Download: Published version (490 KB)
2019
- Foreword - Formalization of geometry, automated and interactive geometric reasoning / Schreck, P., Ida, T., & Kovacs, L. (2019). Foreword - Formalization of geometry, automated and interactive geometric reasoning. Annals of Mathematics and Artificial Intelligence, 85(2–4), 71–72. https://doi.org/10.1007/s10472-019-9617-2
- Foreword / Davenport, J. H., Kovacs, L., & Zaharie, D. (2019). Foreword. Mathematics in Computer Science, 13(4), 459–460. https://doi.org/10.1007/s11786-019-00411-w
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops / Bartocci, E., Kovacs, L., & Stankovic, M. (2019). Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. In Y.-F. Chen, C.-H. Cheng, & J. Esparza (Eds.), Automated Technology for Verification and Analysis (pp. 255–276). Springer. https://doi.org/10.1007/978-3-030-31784-3_15
- Trace Reasoning for Formal Verification using the First-Order Superposition Calculus / Georgiou, P., Gleiss, B., Kovacs, L., & Maffei, M. (2019). Trace Reasoning for Formal Verification using the First-Order Superposition Calculus. FMCAD 2019 Student Forum, San Jose, US, Non-EU. http://hdl.handle.net/20.500.12708/86988
- APRe, Vampire, Welcome in Vienna! / Kovacs, L. (2019). APRe, Vampire, Welcome in Vienna! APRe 2019 Workshop, TU Wien, TU Wien, Vienna, Austria. http://hdl.handle.net/20.500.12708/86999
- Formal Methods in the Digital World (in Hungarian) / Kovacs, L. (2019). Formal Methods in the Digital World (in Hungarian). JegKepzes Series of Presentations- Hungarian Scientists from the Bartok Bela Highschool, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/86998
- First-Order Interpolation / Kovacs, L. (2019). First-Order Interpolation. PhD Research Seminar in Logic and Computation, Faculty of Informatics, West University of Timisoara, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/86997
- Symbolic Computation and Automated Reasoning for Program Analysis / Kovacs, L. (2019). Symbolic Computation and Automated Reasoning for Program Analysis. 23rd IEEE International Conference on Intelligent Engineering Systems (INES) 2019, Gödöllõ, Hungary, EU. http://hdl.handle.net/20.500.12708/86996
- Interpolation in the Grey Area of Proofs / Kovacs, L. (2019). Interpolation in the Grey Area of Proofs. Helmut Veith Memorial Workshop 2019, Turracher Höhe, Austria. http://hdl.handle.net/20.500.12708/86995
- First Order Interpolation / Kovacs, L. (2019). First Order Interpolation. SAT/SMT/AR Summer School 2019, Lisbon, Portugal, EU. http://hdl.handle.net/20.500.12708/86994
- Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire / Gleiss, B., Kovacs, L., & Rath, J. (2019). Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire. Vampire 2019 - The Sixth Vampire Workshop, Lisbon, Portugal, EU. http://hdl.handle.net/20.500.12708/86993
- Verifying Relational Properties using Trace Logic / Kovacs, L. (2019). Verifying Relational Properties using Trace Logic. First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal, EU. http://hdl.handle.net/20.500.12708/86991
- 60 Shades of Grey in Vampire / Kovacs, L. (2019). 60 Shades of Grey in Vampire. ANDREI-60: Automating New-Era Deductive Reasoning Event in Iberia, Tbilisi, Georgia, Non-EU. http://hdl.handle.net/20.500.12708/86990
- Symbol Elimination and Vampire / Kovacs, L. (2019). Symbol Elimination and Vampire. Dagstuhl Seminar 19062 - Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving, Schloss Dagstuhl, Germany, EU. http://hdl.handle.net/20.500.12708/86989
- Interactive Visualization of Saturation Attempts in Vampire / Gleiss, B., Kovács, L., & Schnedlitz, L. (2019). Interactive Visualization of Saturation Attempts in Vampire. In W. Ahrendt & S. Lizeth (Eds.), 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
- Verifying Relational Properties using Trace Logic / Barthe, G., Eilers, R., Georgiou, P., Gleiss, B., Kovacs, L., & Maffei, M. (2019). Verifying Relational Properties using Trace Logic. In B. Clark & J. Yang (Eds.), 2019 Formal Methods in Computer Aided Design (FMCAD). IEEE. https://doi.org/10.23919/fmcad.2019.8894277
2018
- Invariant Generation for Multi-Path Loops with Polynomial Assignments / Humenberger, A., Jaroschek, M., & Kovacs, L. (2018). Invariant Generation for Multi-Path Loops with Polynomial Assignments. In I. Dillig & J. Palsberg (Eds.), Verification, Model Checking, and Abstract Interpretation (pp. 226–246). Springer. https://doi.org/10.1007/978-3-319-73721-8_11
- Symbol Elimination in Program Analysis / 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
- Symbol Elimination for Program Analysis / 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
- First-Order Interpolation in the Grey Area of Proofs / Kovacs, L. (2018). First-Order Interpolation in the Grey Area of Proofs. Summer School on Syntax meets Semantics - Methods, Interactions, and Connections in Substructural Logics (SYSMICS), Les Diablerets, Switzerland, EU. http://hdl.handle.net/20.500.12708/86840
- Automated Reasoning for Rigorous Systems Engineering / Kovacs, L. (2018). Automated Reasoning for Rigorous Systems Engineering. RiSE/SHINE Media Seminar 2018, Vienna, Austria. http://hdl.handle.net/20.500.12708/86714
- Automated Reasoning for Systems Engineering / Kovacs, L. (2018). Automated Reasoning for Systems Engineering. 2018 IEEE International Conference on Future IoT Technologies (Future IoT 2018), Eger, Hungary, EU. http://hdl.handle.net/20.500.12708/86713
- First-Order Interpolation / Kovacs, L. (2018). First-Order Interpolation. SAT/SMT/AR Summer School 2018, Manchester, EU. http://hdl.handle.net/20.500.12708/86712
- First-Order Theorem Proving in Rigorous Systems Engineering / Kovacs, L., & Voronkov, A. (2018). First-Order Theorem Proving in Rigorous Systems Engineering. RiSE/SHiNE Winter School 2018, Wien, Austria. http://hdl.handle.net/20.500.12708/86711
- Aligator.jl – A Julia Package for Loop Invariant Generation / Humenberger, A., Jaroschek, M., & Kovács, L. (2018). Aligator.jl – A Julia Package for Loop Invariant Generation. In F. Rabe (Ed.), Lecture Notes in Computer Science (pp. 111–117). LNCS. https://doi.org/10.1007/978-3-319-96812-4_10
- A FOOLish Encoding of the Next State Relations of Imperative Programs / Kotelnikov, E., Kovács, L., & Voronkov, A. (2018). A FOOLish Encoding of the Next State Relations of Imperative Programs. In Automated Reasoning (pp. 405–421). LNCS. https://doi.org/10.1007/978-3-319-94205-6_27
- Automated Reasoning for Systems Engineering / Kovacs, L. (2018). Automated Reasoning for Systems Engineering. In Foundations of Information and Knowledge Systems (FOIKS) 2018 (p. 1). LNCS. http://hdl.handle.net/20.500.12708/57375
- Loop Analysis by Quantification over Iterations / Gleiss, B., Kovács, L., & Robillard, S. (2018). Loop Analysis by Quantification over Iterations. In G. Barthe, G. Sutcliffe, & M. Veanes (Eds.), EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/269p
- Local proofs and AVATAR / Reger, G., & Suda, M. (2018). Local proofs and AVATAR. In L. Kovacs & A. Voronkov (Eds.), EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/qgdk
- Vampire 2017. Proceedings of the 4th Vampire Workshop / Kovacs, L., & Voronkov, A. (Eds.). (2018). Vampire 2017. Proceedings of the 4th Vampire Workshop. EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/24544
2017
-
Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds Using Symbolic Execution
/
Knoop, J., Kovács, L., & Zwirchmayr, J. (2017). Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds Using Symbolic Execution. Journal of Symbolic Computation, 80, 101–124. https://doi.org/10.1016/j.jsc.2016.07.023
Download: PDF (875 KB) - Global Subsumption Revisited (Briefly) / Reger, G., & Suda, M. (2017). Global Subsumption Revisited (Briefly). In L. Kovacs & A. Voronkov (Eds.), Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop (pp. 61–73). http://hdl.handle.net/20.500.12708/57133
-
First-Order Interpolation and Grey Areas of Proofs (Invited Talk)
/
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
Download: PDF (206 KB) - Polynomial Invariant Generation for Multi-Path Loops / Humenberger, A., Jaroschek, M., & Kovacs, L. (2017). Polynomial Invariant Generation for Multi-Path Loops. Second International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Kaiserslautern, Germany, EU. http://hdl.handle.net/20.500.12708/86847
- Symbol Elimination for Program Analysis / 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
- Algebraic Reasoning for Program Analysis / 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
- Coming to Terms with Quantified Reasoning / Kovacs, L., Robillard, S., & Voronkov, A. (2017). Coming to Terms with Quantified Reasoning. In G. Castagna & A. D. Gordon (Eds.), Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM. https://doi.org/10.1145/3009837
- A Supervisory Control Algorithm Based on Property-Directed Reachability / Claessen, K., Kilhamn, J., Kovács, L., & Lennartson, B. (2017). A Supervisory Control Algorithm Based on Property-Directed Reachability. In O. Strichman & R. Tzoref-Brill (Eds.), Hardware and Software: Verification and Testing (pp. 115–130). Lecture Notes in Computer Science / Springer. https://doi.org/10.1007/978-3-319-70389-3_8
- First-Order Interpolation and Interpolating Proof Systems / Kovacs, L., & Voronkov, A. (2017). First-Order Interpolation and Interpolating Proof Systems. In LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 49–64). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/57308
- Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences / Humenberger, A., Jaroschek, M., & Kovács, L. (2017). Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. In Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation. International Symposium on Symbolic and Algebraic Computation (ISSAC), Kaiserslautern, EU. ACM. https://doi.org/10.1145/3087604.3087623
- Splitting Proofs for Interpolation / Gleiss, B., Kovács, L., & Suda, M. (2017). Splitting Proofs for Interpolation. In Automated Deduction – CADE 26 (pp. 291–309). Springer. https://doi.org/10.1007/978-3-319-63046-5_18
2016
- Automated Reasoning for Systems Engineering / Kovacs, L. (2016). Automated Reasoning for Systems Engineering. Austrian Computer Science Day 2018, Salzburg, Austria. http://hdl.handle.net/20.500.12708/86695
- With a Timisoara Background in the Scientific World of Computer Science and / Kovacs, L. (2016). With a Timisoara Background in the Scientific World of Computer Science and. Timisoara Hungarian Science Festival, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/86440
- Enjoying Research at the Intersection of Math and Computer Science / Kovacs, L. (2016). Enjoying Research at the Intersection of Math and Computer Science. Women in Science Workshop Series (WISE), Gothenburg, Schweden, EU. http://hdl.handle.net/20.500.12708/86439
- First-Order Theorem Proving and Vampire / Kovacs, L. (2016). First-Order Theorem Proving and Vampire. Spring School on Logic and Verification - LoVE, Vienna, Austria, Austria. http://hdl.handle.net/20.500.12708/86438
- The vampire and the FOOL / Kotelnikov, E., Kovács, L., Reger, G., & Voronkov, A. (2016). The vampire and the FOOL. In J. Avigad & A. Chlipala (Eds.), Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. ACM. https://doi.org/10.1145/2854065.2854071
- Symbolic Computation and Automated Reasoning for Program Analysis / Kovács, L. (2016). Symbolic Computation and Automated Reasoning for Program Analysis. In E. Abraham & M. Huisman (Eds.), Lecture Notes in Computer Science (pp. 20–27). Springer / LNCS. https://doi.org/10.1007/978-3-319-33693-0_2
- A Clausal Normal Form Translation for FOOL / Kotelnikov, E., Kovacs, L., Suda, M., & Voronkov, A. (2016). A Clausal Normal Form Translation for FOOL. In GCAI 2016. 2nd Global Conference on Artificial Intelligence (pp. 53–71). EasyChair. http://hdl.handle.net/20.500.12708/56716
2015
- Foreword to the Special Issue on Symbolic Computation in Software Science / Bouhoula, A., Buchberger, B., Kovács, L., & Kutsia, T. (2015). Foreword to the Special Issue on Symbolic Computation in Software Science. Journal of Symbolic Computation, 69, 1–2. https://doi.org/10.1016/j.jsc.2014.09.027
- Symbol Elimination for Program Analysis / Kovacs, L. (2015). Symbol Elimination for Program Analysis. Dagstuhl Seminar 15471 on “Symbolic Computation and Satisfiability Checking,” Dagstuhl, Germany, EU. http://hdl.handle.net/20.500.12708/86263
- Symbol Elimination for Program Analysis / Kovacs, L. (2015). Symbol Elimination for Program Analysis. Theoretical Computer Science Seminar Series of the KTH Royal Institute of Technology, Stockholm, Sweden, EU. http://hdl.handle.net/20.500.12708/86262
- vanHelsing: A Fast Proof Checker for Debuggable Compiler Verification / Lezuo, R., Dragan, I., Barany, G., & Krall, A. (2015). vanHelsing: A Fast Proof Checker for Debuggable Compiler Verification. In L. Kovacs & D. Zaharie (Eds.), 2015 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). https://doi.org/10.1109/synasc.2015.34
- First-Order Theorem Proving and Program Analysis / Kovacs, L. (2015). First-Order Theorem Proving and Program Analysis. In J. Baras (Ed.), Proc. of the LCCC-ACCESS workshop on Model-Based Engineering (pp. 192–217). http://hdl.handle.net/20.500.12708/56444
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP / Kotelnikov, E., Kovacs, L., & Voronkov, A. (2015). A First Class Boolean Sort in First-Order Theorem Proving and TPTP. In M. Kerber (Ed.), Lecture Notes in Computer Science. LNCS. https://doi.org/10.1007/978-3-319-20615-8
- Reasoning About Loops Using Vampire in KeY / Ahrendt, W., Kovacs, L., & Robillard, S. (2015). Reasoning About Loops Using Vampire in KeY. In M. Davis, A. Fehnker, A. McIver, & A. Voronkov (Eds.), Lecture Notes in Computer Science. LNCS. https://doi.org/10.1007/978-3-662-48899-7
- Segment Abstraction for Worst-Case Execution Time Analysis / Cerny, P., Henzinger, T. A., Kovacs, L., Radhakrishna, A., & Zwirchmayr, J. (2015). Segment Abstraction for Worst-Case Execution Time Analysis. In J. Vitek (Ed.), Lecture Notes in Computer Science. LNCS. https://doi.org/10.1007/978-3-662-46669-8
- Special issue on symbolic computation in software science / Special issue on symbolic computation in software science. (2015). In A. Bouhoula, B. Buchberger, L. Kovacs, & T. Kutsia (Eds.), Journal of Symbolic Computation (p. 2). Elsevier. https://doi.org/10.1016/j.jsc.2014.09.027
2014
- Experimenting with SAT Solvers in Vampire / 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
- Symbol Elimination for Automated Generation of Program Properties / Kovacs, L. (2014). Symbol Elimination for Automated Generation of Program Properties. ECEASST, ECEASST(70), 1–2. http://hdl.handle.net/20.500.12708/157934
- The Five P's of Inferring Proven Precise Worst-Case Execution Time Bounds / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2014). The Five P’s of Inferring Proven Precise Worst-Case Execution Time Bounds. 55th Meeting of the IFIP Working Group 2.4 Software Implementation Technology, Stellenbosch, Non-EU. http://hdl.handle.net/20.500.12708/86020
- Replacing Conjectures by Positive Knowledge: Inferring and Proving Precision of Worst-Case Execution Time Bounds using Symbolic Execution / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2014). Replacing Conjectures by Positive Knowledge: Inferring and Proving Precision of Worst-Case Execution Time Bounds using Symbolic Execution. 3rd Joint Meeting of EU FP7 COST Action IC1202 Timing Analysis on Code-Level (TACLe), Vienna, Austria. http://hdl.handle.net/20.500.12708/85811
- Von Vertrauen zum Beweis - Über funktionale Programmkorrektheit hinaus / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2014). Von Vertrauen zum Beweis - Über funktionale Programmkorrektheit hinaus. Festkolloquium zum 80. Geburtstag von Prof. Dr. Dr.h.c. Hans Langmaack, Christian-Albrechts-Universität zu Kiel, Deutschland, EU. http://hdl.handle.net/20.500.12708/85806
- Extensional Crisis and Proving Identity / Gupta, A., Kovács, L., Kragl, B., & Voronkov, A. (2014). Extensional Crisis and Proving Identity. In F. Cassez & J.-F. Raskin (Eds.), Automated Technology for Verification and Analysis (pp. 185–200). Lecture Notes in Computer Science, Springer Verlag. https://doi.org/10.1007/978-3-319-11936-6_14
- Lingva: Generating and Proving Program Properties using Symbol Elimination / Dragan, I., & Kovacs, L. (2014). Lingva: Generating and Proving Program Properties using Symbol Elimination. In 9th International Andrei Ershov Memorial Conference - Perspectives of System Informatics (PSI 2014). Springer LNCS. http://hdl.handle.net/20.500.12708/55992
- Supervisory Control of Discrete-Event Systems via IC3 / Shoaei, M. R., Kovács, L., & Lennartson, B. (2014). Supervisory Control of Discrete-Event Systems via IC3. In E. Yahav (Ed.), Hardware and Software: Verification and Testing (pp. 252–266). Springer Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-319-13338-6_19
2013
- The Auspicious Couple: Symbolic Execution and WCET Analysis / Biere, A., Knoop, J., Kovacs, L., & Zwirchmayr, J. (2013). The Auspicious Couple: Symbolic Execution and WCET Analysis. In C. Maiza (Ed.), Pre-Proceedings of the 13th International Workshop on Worst-Case Execution Time Analysis (WCET 2013) (pp. 51–60). http://hdl.handle.net/20.500.12708/54652
- SmacC: A Retargetable Symbolic Execution Engine / Biere, A., Knoop, J., Kovacs, L., & Zwirchmayr, J. (2013). SmacC: A Retargetable Symbolic Execution Engine. In AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS 11th International Symposium, ATVA 2013. Dang Van Hung and Mizuhito Ogawa, Austria. Springer LNCS 8172. http://hdl.handle.net/20.500.12708/54744
- Editorial to the Special issue on Automated Specification and Verification of Web Systems / Kovács, L., Pugliese, R., Silva, J., & Tiezzi, F. (2013). Editorial to the Special issue on Automated Specification and Verification of Web Systems. The Journal of Logic and Algebraic Programming, 82(8), 241–242. https://doi.org/10.1016/j.jlap.2013.05.007
- Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds using Symbolic Execution / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2013). Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds using Symbolic Execution. 2nd International Seminar on Program Verification, Automated Debugging and Symbolic Computation (PAS 2013), Peking, Non-EU. http://hdl.handle.net/20.500.12708/85808
- Formal Methods for Program Verification / Kovacs, L. (2013). Formal Methods for Program Verification. SAAB/Chalmers joint research seminar, SAAB Kallebäck, Schweden, EU. http://hdl.handle.net/20.500.12708/85756
- Formal Methods in Software Design and Verification / Kovacs, L. (2013). Formal Methods in Software Design and Verification. SAAB Technical Seminar, Linköping, Schweden, EU. http://hdl.handle.net/20.500.12708/85755
- WCET Squeezing by On-demand Feasibility Refinement / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2013). WCET Squeezing by On-demand Feasibility Refinement. 53rd Meeting of the IFIP Working Group 2.4 “Software Implementation Technology,” Mysore, Non-EU. http://hdl.handle.net/20.500.12708/85551
- WCET Squeezing: On-demand Feasibility Refinement for Proven Precise WCET-bounds / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2013). WCET Squeezing: On-demand Feasibility Refinement for Proven Precise WCET-bounds. In 21st International Conference on Real-Time Networks and Systems. Acm Dl. http://hdl.handle.net/20.500.12708/54743
- Bound Propagation for Arithmetic Reasoning in Vampire / Dragan, I., Korovin, K., Kovacs, L., & Voronkov, A. (2013). Bound Propagation for Arithmetic Reasoning in Vampire. In Proceedings of the 15th International Conference on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/55050
- First-Order Theorem Proving and Vampire / Kovács, L., & Voronkov, A. (2013). First-Order Theorem Proving and Vampire. In N. Sharygina & H. Veith (Eds.), Computer Aided Verification (pp. 1–35). Springer LNCS 8044. https://doi.org/10.1007/978-3-642-39799-8_1
- Tree Interpolation in Vampire / Blanc, R., Gupta, A., Kovács, L., & Kragl, B. (2013). Tree Interpolation in Vampire. In M. Kenneth, A. Middeldorp, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 173–181). Springer LNCS 8312. https://doi.org/10.1007/978-3-642-45221-5_13
- The Inverse Method for Many-Valued Logics / Kovács, L., Mantsivoda, A., & Voronkov, A. (2013). The Inverse Method for Many-Valued Logics. In F. Castro, A. Gelbukh, & M. Gonzalez (Eds.), Advances in Artificial Intelligence and Its Applications (pp. 12–23). Springer LNCS 8265. https://doi.org/10.1007/978-3-642-45114-0_2
- A Parametric Interpolation Framework for First-Order Theories / Kovacs, L., Sharygina, N., & Rollini, S. F. (2013). A Parametric Interpolation Framework for First-Order Theories. In F. Castro, A. Gelbukh, & M. Gonzalez (Eds.), Advances in Artificial Intelligence and Its Applications (pp. 24–40). Springer LNCS 8265. https://doi.org/10.1007/978-3-642-45114-0_3
- 5th International Symposium on Symbolic Computation in Software Science / Kovacs, L., & Kutsia, T. (Eds.). (2013). 5th International Symposium on Symbolic Computation in Software Science. EasyChair. http://hdl.handle.net/20.500.12708/23783
- 6th International Workshop on Automated Specification and Verification of Web Systems (WWV) / Kovacs, L., & Kutsia, T. (Eds.). (2013). 6th International Workshop on Automated Specification and Verification of Web Systems (WWV). EasyChair. http://hdl.handle.net/20.500.12708/23784
- Special issue on Automated Specification and Verification of Web Systems / Special issue on Automated Specification and Verification of Web Systems. (2013). In L. Kovacs, R. Pugliese, J. Silva, & F. Tiezzi (Eds.), The Journal of Logic and Algebraic Programming (p. 242). Elsevier. https://doi.org/10.1016/j.jlap.2013.05.007
2012
- Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops / Bjørner, N., & Kovacs, L. (Eds.). (2012). Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops (p. 1415). Springer. https://doi.org/10.1016/j.jsc.2011.12.047
- r-TuBound: Loop Bounds for WCET Analysis (Tool Paper) / Zwirchmayr, J., Knoop, J., & Kovacs, L. (2012). r-TuBound: Loop Bounds for WCET Analysis (Tool Paper). In N. Bjørner & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 435–444). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-642-28717-6_34
- Foreword to the Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops / Bjørner, N., & Kovacs, L. (2012). Foreword to the Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops. Journal of Symbolic Computation, 47(12), 1413–1415. https://doi.org/10.1016/j.jsc.2011.12.047
- Special issue on Automated Specification and Verification of Web Systems / Kovács, L., & Kutsia, T. (2012). Special issue on Automated Specification and Verification of Web Systems. Journal of Applied Logic, 10(1), 1. https://doi.org/10.1016/j.jal.2011.11.001
- FFX: A Portable WCET Annotation Language / Zwirchmayr, J., Kovacs, L., Knoop, J., Bonenfant, A., Cassé, H., & Rochange, C. (2012). FFX: A Portable WCET Annotation Language. In 20th International Conference on Real-Time and Network Systems (pp. 91–100). ACM. http://hdl.handle.net/20.500.12708/54270
- Portable Worst-Case Execution Time Analysis / Bonenfant, A., Cassé, H., de Michiel, M., Knoop, J., Kovacs, L., & Zwirchmayr, J. (2012). Portable Worst-Case Execution Time Analysis. 53rd Meeting of the IFIP Working Group 2.4 Software Implementation Technology, Vadstena, Schweden, EU. http://hdl.handle.net/20.500.12708/85538
- Portable Worst-Case Execution Time Analysis via Flow Facts in XML / Bonenfant, A., Cassé, H., de Michiel, M., Knoop, J., Kovacs, L., & Zwirchmayr, J. (2012). Portable Worst-Case Execution Time Analysis via Flow Facts in XML. 29th Annual Workshop of the GI-Fachgruppe “Programmiersprachen und Rechenkonzepte,” Bad Honnef, Deutschland, EU. http://hdl.handle.net/20.500.12708/85537
- Playing in the Grey Area of Proofs / Kovacs, L. (2012). Playing in the Grey Area of Proofs. Rigorous System Engineering Seminar IST/TU Wien, Vienna, Austria. http://hdl.handle.net/20.500.12708/85493
- Playing in the Grey Area of Proofs / Kovacs, L. (2012). Playing in the Grey Area of Proofs. Research Seminar at VERIMAG Grenoble, Grenoble, France, EU. http://hdl.handle.net/20.500.12708/85492
- Playing in the Grey Area of Proofs / Kovacs, L. (2012). Playing in the Grey Area of Proofs. Research Seminar at Microsoft Research Cambridge, Cambridge, UK, EU. http://hdl.handle.net/20.500.12708/85490
- Symbol Elimination in Program Analysis / Kovacs, L. (2012). Symbol Elimination in Program Analysis. International Seminar on Program Verification, Automated Debugging and Symbolic Computation (PAS), Beijing, China, Non-EU. http://hdl.handle.net/20.500.12708/85489
- Automated Theorem Proving - An Introduction / Kovacs, L. (2012). Automated Theorem Proving - An Introduction. ARiSE/VCLA Winter School on Verification, Wien, Austria. http://hdl.handle.net/20.500.12708/85319
- Automated Theorem Proving - with some Applications to Verification / Kovacs, L. (2012). Automated Theorem Proving - with some Applications to Verification. ARiSE/VCLA Winter School on Verification, Wien, Austria. http://hdl.handle.net/20.500.12708/85316
- Solving Robust Glucose-Insulin Control by Dixon Resultant Computations / Kovacs, L., Palancz, B., & Kovacs, L. (2012). Solving Robust Glucose-Insulin Control by Dixon Resultant Computations. In Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scienti c Computing (SYNASC 2012). 14th International Symposium on Symbolic and Numeric Algorithms for Scienti c Computing (SYNASC 2012), Timisoara, Romania, EU. IEEE Proceedings. http://hdl.handle.net/20.500.12708/54508
- The Boundary Element Method in the Study of Non-Stationary Movements Through Network Pro les / Kovacs, A., Kovacs, L., & Kovacs, L. (2012). The Boundary Element Method in the Study of Non-Stationary Movements Through Network Pro les. In Proceedings of 13th International Conference on Mathematics and its Applications. (pp. 241–248). Scientific Bulletin of Politehnica University Timisoara, Romania. http://hdl.handle.net/20.500.12708/54506
- Examples of Symbol Elimination in Program Verification / Kovacs, L., & Kovacs, A. (2012). Examples of Symbol Elimination in Program Verification. In Proceedings of 13th International Conference on Mathematics and its Applications (pp. 145–150). Scientific Bulletin of Politehnica University Timisoara, Romania. http://hdl.handle.net/20.500.12708/54507
- A Hodographic Approximation Method for Analyzing the Fluid Motion Through Network Pro files / Kovacs, A., & Kovacs, L. (2012). A Hodographic Approximation Method for Analyzing the Fluid Motion Through Network Pro files. In Annals of DAAAM for 2012 & Proceedings of the 23rd International DAAAM Symposium (p. 4). DAAAM International, Vienna, Austria. http://hdl.handle.net/20.500.12708/54505
- Symbol Elimination in Program Analysis / Kovacs, L. (2012). Symbol Elimination in Program Analysis. In D. Wang, V. Negru, T. Ida, T. Jebelean, D. Petcu, S. M. Watt, & D. Zaharie (Eds.), Proc. of 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) (pp. 12–13). IEEE Computer Society. http://hdl.handle.net/20.500.12708/54061
- Playing in the grey area of proofs / Hoder, K., Kovacs, L., & Voronkov, A. (2012). Playing in the grey area of proofs. In J. Field & M. Hicks (Eds.), Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’12. ACM. https://doi.org/10.1145/2103656.2103689
- Symbolic Loop Bound Computation for WCET Analysis / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2012). Symbolic Loop Bound Computation for WCET Analysis. In Ershov Informatic Conference, PSI Series, 8th Edition (pp. 224–239). Springer-Verlag, Lecture Notes in Computer Science. http://hdl.handle.net/20.500.12708/53669
- Vinter: A Vampire-Based Tool for Interpolation / Hoder, K., Holzer, A., Kovács, L., & Voronkov, A. (2012). Vinter: A Vampire-Based Tool for Interpolation. In Programming Languages and Systems (pp. 148–156). Springer / LNCS. https://doi.org/10.1007/978-3-642-35182-2_11
- Special Issue on Automated Speci cation and Veri cation of Web Systems / Kovacs, L., & Kutsia, T. (Eds.). (2012). Special Issue on Automated Speci cation and Veri cation of Web Systems. Elsevier B.V. http://hdl.handle.net/20.500.12708/23614
2011
- On Transfinite Knuth-Bendix Orders / Kovacs, L., Moser, G., & Voronkov, A. (2011). On Transfinite Knuth-Bendix Orders. In N. Bjørner & V. Sofronie-Stokkermans (Eds.), Proc. of the 23rd International Conference on Automated Deduction (CADE-23) (pp. 384–399). Springer. http://hdl.handle.net/20.500.12708/54018
- First-order theorem proving and Vampire / Kovacs, L., & 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
- First-order theorem proving and Vampire / Kovacs, L. (2011). First-order theorem proving and Vampire. RiSE-PUMA Workshop, Traunkirchen, Austria, EU. http://hdl.handle.net/20.500.12708/85274
- Invariant Generation using Theorem Proving / Kovacs, L., & Voronkov, A. (2011). Invariant Generation using Theorem Proving. 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/85273
- Program Assertion Synthesis using Symbolic Computation / Kovacs, L. (2011). Program Assertion Synthesis using Symbolic Computation. 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/85272
- Symbol Elimination in Program Analysis / Kovacs, L. (2011). Symbol Elimination in Program Analysis. Helsinki Institute for Information Technology (HIIT), Helsinki, Finnland, EU. http://hdl.handle.net/20.500.12708/85271
- First-order theorem proving and Vampire / Hoder, K., Kovacs, L., & Voronkov, A. (2011). First-order theorem proving and Vampire. 23rd International Conference on Automated Deduction (CADE-23), Wroclaw, Poland, EU. http://hdl.handle.net/20.500.12708/85270
- Interpolation and Symbol Elimination / Kovacs, L. (2011). Interpolation and Symbol Elimination. TU Graz, Austria. http://hdl.handle.net/20.500.12708/85269
- RiSE: Rigorous Systems Engineering / Kovacs, L. (2011). RiSE: Rigorous Systems Engineering. Research Seminar for Master Students, West University of Timisoara, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/85268
- Experiments with Invariant Generation Using a Saturation Theorem Prover / Kovacs, L. (2011). Experiments with Invariant Generation Using a Saturation Theorem Prover. AdaCore Paris, Paris, France, EU. http://hdl.handle.net/20.500.12708/85267
- Experiments with Invariant Generation Using a Saturation Theorem Prover / Kovacs, L. (2011). Experiments with Invariant Generation Using a Saturation Theorem Prover. “Deduction at Scale” Seminar, Ringberg Castle, Germany, EU. http://hdl.handle.net/20.500.12708/85266
- Proceedings of the 7th International Workshop on Automated Specification and Verification of Web Systems / Kovacs, L., Pugliese, R., & Tiezzi, F. (Eds.). (2011). Proceedings of the 7th International Workshop on Automated Specification and Verification of Web Systems. EPTCS Vol. 61. https://doi.org/10.48550/arXiv.1108.2085
- Aligator: Experiments and Limitations / Kovacs, L., & Kovacs, A. (2011). Aligator: Experiments and Limitations. In Proc. of the 22nd International DAAAM Symposium: “Intelligent Manufactoring and Automation: Power of Knowledge and Creativity” (pp. 1145–1146). DAAAM International. http://hdl.handle.net/20.500.12708/54065
- Analyzing the Fluid Motion Through Network Profiles Using the Boundary Element Method / Kovacs, A., & Kovacs, L. (2011). Analyzing the Fluid Motion Through Network Profiles Using the Boundary Element Method. In Proc. of the 22nd International DAAAM Symposium: “Intelligent Manufactoring and Automation: Power of Knowledge and Creativity” (pp. 1147–1148). DAAAM International, Volume 22, Nr. 1. http://hdl.handle.net/20.500.12708/54062
- Case Studies on Invariant Generation Using a Saturation Theorem Prover / Hoder, K., Kovacs, L., & Voronkov, A. (2011). Case Studies on Invariant Generation Using a Saturation Theorem Prover. In I. Z. Batyrshin & G. Sidorov (Eds.), Advances in Artificial Intelligence - 10th Mexican International Conference on Artificial Intelligence (MICAI) (pp. 1–15). Springer. http://hdl.handle.net/20.500.12708/54058
- Invariant Generation in Vampire / Hoder, K., Kovacs, L., & Voronkov, A. (2011). Invariant Generation in Vampire. In Proc. of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (pp. 60–64). Springer. http://hdl.handle.net/20.500.12708/54052
- An Evaluation of WCET Analysis using Symbolic Loop Bounds (abstract/presentation) / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2011). An Evaluation of WCET Analysis using Symbolic Loop Bounds (abstract/presentation). In Tagungsband 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS’11) (p. 200). Westfälische Wilhelms-Universität Münster. http://hdl.handle.net/20.500.12708/54044
- An Evaluation of WCET Analysis using Symbolic Loop Bounds (extended Abstract) / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2011). An Evaluation of WCET Analysis using Symbolic Loop Bounds (extended Abstract). In MEMICS Proceedings (p. 119). http://hdl.handle.net/20.500.12708/54021
- Practical Experiments with Symbolic Loop Bound Computation for WCET Analysis / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2011). Practical Experiments with Symbolic Loop Bound Computation for WCET Analysis. In 28. Workshop der GI-Fachgruppe Programmiersprachen & Rechenkonzepte. 28. Workshop der GI-Fachgruppe “Programmiersprachen und Rechenkonzepte,” Bad Honnef, EU. Technischer Bericht des Instituts für Informatik der Christian-Albrechts Universität zu Kiel. http://hdl.handle.net/20.500.12708/53670
- An Evaluation of WCET Analysis using Symbolic Loop Bounds / Knoop, J., Kovacs, L., & Zwirchmayr, J. (2011). An Evaluation of WCET Analysis using Symbolic Loop Bounds. In C. Healy (Ed.), Proc. 11’th International Workshop on Worst-Case Execution Time Analysis (pp. 93–103). Österreichische Computer Gesellschaft - OCG. http://hdl.handle.net/20.500.12708/53668
2010
- Introduction to the Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops / 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
- Quantified Invariant Generation using Symbolic Computation and Theorem Proving / 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
- Aligators and Arrays / Kovacs, L. (2010). Aligators and Arrays. IST/TU Rigorous System Engineering, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85047
- Symbol Elimination and Interpolation / Kovacs, L. (2010). Symbol Elimination and Interpolation. University of Verona, University of Verona, Italy, EU. http://hdl.handle.net/20.500.12708/85046
- Symbol Elimination and Interpolation for Software Verification / Kovacs, L. (2010). Symbol Elimination and Interpolation for Software Verification. Intel Haifa, Haifa, Israel, Non-EU. http://hdl.handle.net/20.500.12708/85045
- Interpolation and Symbol Elimination / 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
- Interpolation and Symbol Elimination / Kovacs, L. (2010). Interpolation and Symbol Elimination. RiSE Workshop, Technical University of Graz, Austria. http://hdl.handle.net/20.500.12708/85043
- Interpolation and Symbol Elimination in Vampire / 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
- Aligators for Arrays (Tool Paper) / 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
- ABC: Algebraic Bound Computation for Loops / 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
- Proceedings of the 6th International Workshop on Automated Specification and Verification of Web Systems (WWV'10) / 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
- Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops / 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
Supervisions
-
Constraint Superposition for Higher-order Logic
/
Hetzenberger, M. (2023). Constraint Superposition for Higher-order Logic [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.108280
Download: PDF (1.3 MB) -
Superposition Reasoning About Quantied Bitvector Formulas
/
Damestani, D. (2023). Superposition Reasoning About Quantied Bitvector Formulas [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.77502
Download: PDF (383 KB) -
Moment-Based Loop Analysis
/
Stankovic, M. (2023). Moment-Based Loop Analysis [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.113863
Download: PDF (1.26 MB) -
Exact Inference for Probabilistic Loops
/
Müllner, J. (2023). Exact Inference for Probabilistic Loops [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.107471
Download: PDF (1020 KB) -
Automating proofs of game-theoretic security properties of off-chain protocols
/
Brugger, L. S. (2022). Automating proofs of game-theoretic security properties of off-chain protocols [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.104340
Download: PDF (666 KB) -
User propagators for satisfiability modulo custom theories
/
Eisenhofer, C. (2022). User propagators for satisfiability modulo custom theories [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.100221
Download: PDF (1.13 MB) -
Non-linear SMT-reasoning over finite fields
/
Hader, T. (2022). Non-linear SMT-reasoning over finite fields [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.89445
Download: PDF (512 KB) -
Non-Linear reasoning in the superposition calculus
/
Lackner, A. (2022). Non-Linear reasoning in the superposition calculus [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.90765
Download: PDF (734 KB) -
Algebra-based loop reasoning - invariant generation and synthesis for numeric loops
/
Humenberger, A. (2021). Algebra-based loop reasoning - invariant generation and synthesis for numeric loops [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.89761
Download: PDF (1.15 MB) -
Automating termination analysis of probabilistic programs
/
Moosbrugger, M. (2020). Automating termination analysis of probabilistic programs [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.77501
Download: PDF (710 KB) -
Automated induction by reflection
/
Schoisswohl, J. (2020). Automated induction by reflection [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.75342
Download: PDF (591 KB) -
Automated reasoning over Arrays in the superposition calculus
/
Hochrainer, C. (2020). Automated reasoning over Arrays in the superposition calculus [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.77511
Download: PDF (705 KB) -
Automated software verification using superposition-based theorem proving
/
Gleiss, B. (2020). Automated software verification using superposition-based theorem proving [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.86611
Download: PDF (1.24 MB) -
Formalizing graph trail properties
/
Lachnitt, H. E. (2020). Formalizing graph trail properties [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.77262
Download: PDF (564 KB) -
Automating inductive reasoning with recursive functions
/
Hajdu, M. (2020). Automating inductive reasoning with recursive functions [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.84140
Download: PDF (961 KB) -
First-order reasoning with aggregates
/
Rain, S. (2020). First-order reasoning with aggregates [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.74620
Download: PDF (794 KB) -
Trace Reasoning for formal verification : guiding vampire in induction
/
Georgiou, P. (2019). Trace Reasoning for formal verification : guiding vampire in induction [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.71683
Download: PDF (501 KB) -
Subsumption demodulation in first-order theorem proving
/
Rath, J. (2019). Subsumption demodulation in first-order theorem proving [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.69280
Download: PDF (4.58 MB) -
Interpolation and local proofs
/
Gleiss, B. (2016). Interpolation and local proofs [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.36061
Download: PDF (761 KB) -
First-order theorem proving for program analysis and theory reasoning
/
Dragan, I.-D. (2015). First-order theorem proving for program analysis and theory reasoning [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2015.28456
Download: PDF (975 KB) -
Reasoning in first-order theories with extensionality
/
Kragl, B. (2014). Reasoning in first-order theories with extensionality [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2014.23884
Download: PDF (503 KB) -
Symbolic methods for the timing analysis of programs
/
Zwirchmayr, J. (2013). Symbolic methods for the timing analysis of programs [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2013.22070
Download: PDF (1.22 MB) -
An evaluation of symbol elimination for generating first-order loop invariants
/
Jucu, I. (2013). An evaluation of symbol elimination for generating first-order loop invariants [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2013.22624
Download: PDF (705 KB)