Journal Articles

Correnson, A., Nießen, T., Finkbeiner, B., & Weissenbacher, G. (2025). Symbolic execution for refuting ∀∃ hyperproperties. Acta Informatica, 62(4), Article 40. https://doi.org/10.1007/s00236-025-00504-z ( reposiTUm)

Bocevska, I., Petković Komel, A., Kovacs, L., Rain, S., & Rawson, M. (2025). Divide and Conquer: A Compositional Approach to Game-Theoretic Security. Proceedings of the ACM on Programming Languages, 9(OOPSLA2), 1949–1973. https://doi.org/10.1145/3763120 ( reposiTUm)

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)

Kofnov, A., Moosbrugger, M., Stankovic, M., Bartocci, E., & Bura, E. (2024). Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial Assignments. ACM Transactions on Modeling and Computer Simulation, 34(3), Article 18. https://doi.org/10.1145/3641545 ( reposiTUm)

Correnson, A., Nießen, T., Finkbeiner, B., & Weissenbacher, G. (2024). Finding ∀∃ Hyperbugs using Symbolic Execution. Proceedings of the ACM on Programming Languages, 8(OOPSLA2), 1420–1445. https://doi.org/10.1145/3689761 ( reposiTUm)

Pani, T., Weissenbacher, G., & Zuleger, F. (2024). Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification. Formal Methods in System Design, 64(1–3), 108–145. https://doi.org/10.1007/s10703-023-00439-6 ( reposiTUm)

Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., & Biere, A. (2024). Satisfiability Modulo User Propagators. Journal of Artificial Intelligence Research, 81, 989–1017. https://doi.org/10.1613/jair.1.16163 ( 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)

Sochor, H., Ferrarotti, F., & Kaufmann, D. (2024). Fuzzing-based grammar learning from a minimal set of seed inputs. JOURNAL OF COMPUTER LANGUAGES, 78, Article 101252. https://doi.org/10.1016/j.cola.2023.101252 ( reposiTUm)

Amrollahi, D., Bartocci, E., Kenison, G., Kovács, L., Moosbrugger, M., & Stankovič, M. (2024). Correction: (Un)Solvable loop analysis. Formal Methods in System Design. https://doi.org/10.1007/s10703-024-00465-y ( reposiTUm)

Matheja, C., Pagel, J., & Zuleger, F. (2023). A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions. ACM Transactions on Computational Logic, 24(1), 1–76. https://doi.org/10.1145/3534927 ( reposiTUm)

Ayala, P., Naghdi, S., Nandan, S. P., Myakala, S. N., Rath, J., Saito, H., Guggenberger, P., Lakhanlal, L., Kleitz, F., Toroker, M. C., Cherevan, A., & Eder, D. (2023). The Emergence of 2D Building Units in Metal‐Organic Frameworks for Photocatalytic Hydrogen Evolution: A Case Study with COK‐47. Advanced Energy Materials, 13(31), Article 2300961. https://doi.org/10.1002/aenm.202300961 ( reposiTUm)

Kaufmann, D., & Biere, A. (2023). Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra. International Journal on Software Tools for Technology Transfer, 25(2), 133–144. https://doi.org/10.1007/s10009-022-00688-6 ( 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)

Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2022). Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. International Journal on Software Tools for Technology Transfer, 24(1), 33–48. https://doi.org/10.1007/s10009-021-00637-9 ( reposiTUm)

Pagel, J., & Zuleger, F. (2022). Strong-separation Logic (Extended Version). ACM Letters on Programming Languages and Systems, 44(3), 1–40. https://doi.org/10.1145/3498847 ( 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)

Fermüller, C., Lang, T. A., & Pavlova, A. (2022). From Truth Degree Comparison Games to Sequents-of-Relations Calculi for Gödel Logic. Logica Universalis, 16(1–2), 221–235. https://doi.org/10.1007/s11787-022-00300-0 ( 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)

Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2022). Verification of agent navigation in partially-known environments. Artificial Intelligence, 308, Article 103724. https://doi.org/10.1016/j.artint.2022.103724 ( 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)

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)

Chockler, H., & Weissenbacher, G. (2021). Preface of the special issue on the conference on computer-aided verification 2018. Formal Methods in System Design. https://doi.org/10.1007/s10703-021-00365-5 ( reposiTUm)

De Coster, A., Musliu, N., Schaerf, A., Schoisswohl, J., & Smith-Miles, K. (2021). Algorithm selection and instance space analysis for curriculum-based course timetabling. Journal of Scheduling, 25(1), 35–58. https://doi.org/10.1007/s10951-021-00701-x ( reposiTUm)

Fellner, A., Tabaei Befrouei, M., & Weissenbacher, G. (2021). Mutation testing with hyperproperties. Software and Systems Modeling, 20(2), 405–427. https://doi.org/10.1007/s10270-020-00850-1 ( reposiTUm)

Pani, T., Weissenbacher, G., & Zuleger, F. (2021). Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. Formal Methods in System Design, 57(2), 270–302. https://doi.org/10.1007/s10703-021-00370-8 ( reposiTUm)

Metzler, P., Suri, N., & Weissenbacher, G. (2020). Extracting safe thread schedules from incomplete model checking results. International Journal on Software Tools for Technology Transfer, 22(5), 565–581. https://doi.org/10.1007/s10009-020-00575-y ( reposiTUm)

Stewart, D., & Weissenbacher, G. (2020). Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017. Formal Methods in System Design, 57(3), 303–304. https://doi.org/10.1007/s10703-020-00357-x ( reposiTUm)

Homola, M., Kľuka, J., Hozzová, P., Svátek, V., & Vacura, M. (2020). Towards Higher-order OWL. Kuenstliche Intelligenz, 34, 417–421. https://doi.org/10.1007/s13218-020-00665-8 ( reposiTUm)

Barkatou, M. A., & Jaroschek, M. (2019). Removing apparent singularities of linear difference systems. Journal of Symbolic Computation, 102, 86–107. https://doi.org/10.1016/j.jsc.2019.10.010 ( reposiTUm)

Fellner, A., Krenn, W., Schlick, R., Tarrach, T., & Weissenbacher, G. (2019). Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search. ACM Transactions on Embedded Computing Systems, 18(1), 1–28. https://doi.org/10.1145/3289256 ( 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)

Ozkan, B. K., Majumdar, R., Niksic, F., Befrouei, M. T., & Weissenbacher, G. (2018). Randomized testing of distributed systems with probabilistic guarantees. Proceedings of the ACM on Programming Languages, 2(OOPSLA), 1–28. https://doi.org/10.1145/3276530 ( reposiTUm)

Aminof, B., Kotek, T., Rubin, S., Spegni, F., & Veith, H. (2018). Parameterized model checking of rendezvous systems. Distributed Computing, 31(3), 187–222. https://doi.org/10.1007/s00446-017-0302-6 ( reposiTUm)

Beyersdorff, O., Blinkhorn, J., Chew, L., Schmidt, R., & Suda, M. (2018). Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. Journal of Automated Reasoning, 63(3), 597–623. https://doi.org/10.1007/s10817-018-9482-4 ( reposiTUm)

Gottlob, G., Henzinger, T. A., & Weissenbacher, G. (2017). Preface of the Special Issue in Memoriam Helmut Veith. Formal Methods in System Design, 51(2), 267–269. https://doi.org/10.1007/s10703-017-0307-6 ( reposiTUm)

Konnov, I., Veith, H., & Widder, J. (2017). On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation, 252, 95–109. https://doi.org/10.1016/j.ic.2016.03.006 ( reposiTUm)

Demyanova, Y., Pani, T., Veith, H., & Zuleger, F. (2017). Empirical software metrics for benchmarking of verification tools. Formal Methods in System Design, 50(2–3), 289–316. https://doi.org/10.1007/s10703-016-0264-5 ( reposiTUm)

Konnov, I., Lazić, M., Veith, H., & Widder, J. (2017). Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms. Formal Methods in System Design, 51(2), 270–307. https://doi.org/10.1007/s10703-017-0297-4 ( reposiTUm)

Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., & Widder, J. (2016). Decidability of Parameterized Verification. ACM SIGACT News, 47(2), 53–64. https://doi.org/10.1145/2951860.2951873 ( reposiTUm)

Schlaipfer, M., & Weissenbacher, G. (2016). Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs. Journal of Automated Reasoning, 57(1), 3–36. https://doi.org/10.1007/s10817-016-9364-6 ( reposiTUm)

BICHLER, M., MORAK, M., & WOLTRAN, S. (2016). The Power of Non-Ground Rules in Answer Set Programming. Theory and Practice of Logic Programming, 16(5–6), 552–569. https://doi.org/10.1017/s1471068416000338 ( reposiTUm)

Ianni, G., Calimeri, F., Germano, S., Humenberger, A., Redl, C., Stepanova, D., Tucci, A., & Wimmer, A. (2016). Angry-HEX: an Artificial Player for Angry Birds Based on Declarative Knowledge Bases. IEEE Transactions on Computational Intelligence and AI in Games, 8(2), 128–139. https://doi.org/10.1109/tciaig.2015.2509600 ( reposiTUm)

Charron-Bost, B., Függer, M., Welch, J. L., & Widder, J. (2015). Time Complexity of Link Reversal Routing. ACM Transactions on Algorithms, 11(3), 1–39. https://doi.org/10.1145/2644815 ( reposiTUm)

Pani, T., Veith, H., & Zuleger, F. (2015). Loop Patterns in C Programs. ECEASST, 72. http://hdl.handle.net/20.500.12708/151928 ( reposiTUm)

Vizel, Y., Weissenbacher, G., & Malik, S. (2015). Boolean Satisfiability Solvers and Their Applications in Model Checking. Proceedings of the IEEE, 103(11), 2021–2035. https://doi.org/10.1109/jproc.2015.2455034 ( reposiTUm)

Holzer, A., Schallhart, C., Tautschnig, M., & Veith, H. (2015). Closure properties and complexity of rational sets of regular languages. Theoretical Computer Science, 605, 62–79. https://doi.org/10.1016/j.tcs.2015.08.035 ( reposiTUm)

Lewis, M., Kroening, D., & Weissenbacher, G. (2015). Under-approximating loops in C programs for fast counterexample detection. Formal Methods in System Design, 47(1), 75–92. https://doi.org/10.1007/s10703-015-0228-1 ( reposiTUm)

Kotek, T., & Makowsky, J. A. (2014). A representation theorem for (q-)holonomic sequences. Journal of Computer and System Sciences, 80(2), 363–374. https://doi.org/10.1016/j.jcss.2013.05.004 ( reposiTUm)

Kotek, T., & Makowsky, J. A. (2014). Recurrence relations for graph polynomials on bi-iterative families of graphs. European Journal of Combinatorics, 41, 47–67. https://doi.org/10.1016/j.ejc.2014.03.012 ( reposiTUm)

Kotek, T., & Makowsky, J. A. (2014). Connection Matrices and the Definability of Graph Parameters. Logical Methods in Computer Science, 10(4), 1–33. http://hdl.handle.net/20.500.12708/157260 ( reposiTUm)

Charron-Bost, B., Gaillard, A., Welch, J. L., & Widder, J. (2013). Link Reversal Routing with Binary Link Labels: Work Complexity. SIAM Journal on Computing, 42(2), 634–661. https://doi.org/10.1137/110843095 ( reposiTUm)

Chaki, S., Schallhart, C., & Veith, H. (2013). Verification across Intellectual Property Boundaries. ACM Transactions on Software Engineering and Methodology, 22(2), 1–12. https://doi.org/10.1145/2430545.2430550 ( reposiTUm)

Widder, J., Biely, M., Gridling, G., Weiss, B., & Blanquart, J.-P. (2012). Consensus in the presence of mortal Byzantine faulty processes. Distributed Computing, 24(6), 299–321. https://doi.org/10.1007/s00446-011-0147-3 ( reposiTUm)

Veith, H. (2012). Special Issue: Games in Verification (foreword). Journal of Computer and System Sciences, 78(2), 393. https://doi.org/10.1016/j.jcss.2011.05.007 ( reposiTUm)

Dawar, A., & Veith, H. (2012). Selected Papers of the Conference “Computer Science Logic CSL 2010”: Preface. Logical Methods in Computer Science. https://doi.org/10.2168/lmcs-csl:2010 ( reposiTUm)

Bjørner, N., Nieuwenhuis, R., Veith, H., & Voronkov, A. (2011). Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports, 1(7), 23–35. https://doi.org/10.4230/DagRep.1.7.23 ( reposiTUm)

Kinder, J., Katzenbeisser, S., Schallhart, C., & Veith, H. (2010). Proactive Detection of Computer Worms Using Model Checking. IEEE Transactions on Dependable and Secure Computing, 7(4), 424–438. https://doi.org/10.1109/tdsc.2008.74 ( reposiTUm)

Jha, S., Katzenbeisser, S., Schallhart, C., Veith, H., & Chenney, S. (2010). Semantic Integrity in Large-Scale Online Simulations. ACM Transactions on Internet Technology, 10(1), 1–24. https://doi.org/10.1145/1667067.1667069 ( reposiTUm)

Bauer, A., Leucker, M., Schallhart, C., & Tautschnig, M. (2010). Don’t care in SMT---Building flexible yet efficient abstraction/refinement solvers. International Journal on Software Tools for Technology Transfer, 12(1), 23–37. https://doi.org/10.1007/s10009-009-0133-2 ( reposiTUm)

Bauer, A., Leucker, M., & Schallhart, C. (2010). Comparing LTL Semantics for Runtime Verification. Journal of Logic and Computation, 20(3), 651–674. https://doi.org/10.1093/logcom/exn075 ( reposiTUm)

Samer, M., & Veith, H. (2010). On the distributivity of LTL specifications. ACM Transactions on Computational Logic, 11(3), 1–26. https://doi.org/10.1145/1740582.1740588 ( reposiTUm)

Conference Proceedings Contributions

El Manssour, R. A., Kenison, G., Shirmohammadi, M., Varonka, A., & Worrell, J. B. (2026). Determination Problems for Orbit Closures and Matrix Groups. In M. Hicks (Ed.), Proceedings of the ACM on Programming Languages (pp. 1615–1640). Association for Computing Machinery. https://doi.org/10.1145/3776698 ( reposiTUm)

Sextl, F., Rogalewicz, A., Vojnar, T., & Zuleger, F. (2025). Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration. In V. Vafeiadis (Ed.), Programming Languages and Systems (pp. 230–257). Springer, Cham. https://doi.org/10.1007/978-3-031-91121-7_10 ( reposiTUm)

Ait El Manssour, R., Kenison, G., Shirmohammadi, M., & Varonka, A. (2025). Simple Linear Loops: Algebraic Invariants and Applications. In M. Hicks (Ed.), Proceedings of the ACM on Programming Languages (pp. 745–771). Association for Computing Machinery. https://doi.org/10.1145/3704862 ( reposiTUm)

Hofstadler, C., & Kaufmann, D. (2025). Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification. In M. Garcia de la Banda (Ed.), 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.CP.2025.14 ( reposiTUm)

Kaufmann, D., & Hofstadler, C. (2025). Recycling Algebraic Proof Certificates. In M. Erașcu & M. Janota (Eds.), Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC-Square 2025) Collocated with The 30th International Conference on Automated Deduction (CADE 2025) (pp. 35–40). Ceur. ( reposiTUm)

Pluska, A., & Malhotra, S. (2025). On Local Limits of Sparse Random Graphs: Color Convergence and the Refined Configuration Model. In 39th Annual Conference on Neural Information Processing Systems (NeurIPS 2025). 39th Annual Conference on Neural Information Processing Systems (NeurIPS 2025), San Diego, United States of America (the). Curran Associates, Inc. ( reposiTUm)

Bozga, M., Iosif, R., & Zuleger, F. (2025). Regular Grammars for Sets of Graphs of Tree-Width 2. In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (pp. 704–717). IEEE. https://doi.org/10.1109/LICS65433.2025.00059 ( reposiTUm)

Hajdu, M., Coutelier, R., Kovacs, L., & Voronkov, A. (2025). Term Ordering Diagrams. In C. Barrett & U. Waldmann (Eds.), Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings (pp. 552–569). Springer-Verlag. https://doi.org/10.1007/978-3-031-99984-0_29 ( reposiTUm)

Bártek, F., Bhayat, A., Coutelier, R., Hajdu, M., Hetzenberger, M., Hozzová, P., Kovács, L., Rath, J., Rawson, M., Reger, G., Suda, M., Schoisswohl, J., & Voronkov, A. (2025). The Vampire Diary. In R. Piskac & Zvonimir Rakamarić (Eds.), Computer Aided Verification (pp. 57–71). Springer. https://doi.org/10.1007/978-3-031-98682-6_4 ( reposiTUm)

Fazekas, K., Pollitt, F., Fleury, M., & Biere, A. (2025). Incremental Inprocessing Rules beyond Resolution. In J. Hoenicke, M. Janota, A. Niemetz, & S. Tourret (Eds.), SMT+PoS 2025 : Satisfiability Modulo Theories & Pragmatics of SAT 2 (pp. 190–200). ( reposiTUm)

Kaufmann, D., & Berthomieu, J. (2025). Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs. In A. Gurfinkel & M. Heule (Eds.), Tools and Algorithms for the Construction and Analysis of Systems : 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3–8, 2025, Proceedings, Part I (pp. 355–374). Springer. https://doi.org/10.1007/978-3-031-90643-5_19 ( reposiTUm)

Bozga, M., Iosif, R., & Zuleger, F. (2025). Iterating Non-Aggregative Structure Compositions. In C. Aiswarya, R. Mehta, & S. Roy (Eds.), 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Schloss Dagstuhl–Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.FSTTCS.2025.18 ( reposiTUm)

Hajdu, M., Kovács, L., & Voronkov, A. (2025). Partial Redundancy in Saturation. In C. Barrett & U. Waldmann (Eds.), Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings (pp. 532–551). https://doi.org/10.1007/978-3-031-99984-0_28 ( reposiTUm)

Varonka, A., & Watanabe, K. (2025). On Piecewise Affine Reachability with Bellman Operators. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) (pp. 92:1-92:18). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2025.92 ( reposiTUm)

Rath, J., Eisenhofer, C., Kaufmann, D., Bjørner, N., & Kovacs, L. (2025). PolySAT: Word-level Bit-vector Reasoning in Z3. In J. Protzenko & A. Raad (Eds.), Verified Software. Theories, Tools and Experiments : 16th International Conference, VSTTE 2024, Prague, Czech Republic, October 14–15, 2024, Revised Selected Papers (pp. 47–69). Springer. https://doi.org/10.1007/978-3-031-86695-1_4 ( reposiTUm)

Hajdu, M., Hozzová, P., Kovacs, L., Voronkov, A., Wagner, E. M., & Žilinčík, R. S. (2025). Synthesis Benchmarks for Automated Reasoning. In V. de Paiva & P. Koepke (Eds.), Intelligent Computer Mathematics (pp. 21–28). Springer Nature Link. https://doi.org/10.1007/978-3-032-07021-0_2 ( reposiTUm)

Winkler, L., & Kovács, L. (2025). Positive Almost-Sure Termination of Polynomial Random Walks. In P. Prabhakar & A. Vandin (Eds.), Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (pp. 275–292). Springer. https://doi.org/10.1007/978-3-032-05792-1_15 ( reposiTUm)

Simader, M., Rebola-Pardo, A., & Seidl, M. (2025). FERAT: A New Expansion-Based Certification Framework for Quantified Boolean Formulas. In SAC ’25: Proceedings of the 40th ACM/SIGAPP Symposium on Applied Computing (pp. 1043–1050). https://doi.org/10.1145/3672608.3707863 ( reposiTUm)

King, D., Koutavas, V., & Kovacs, L. (2025). LLM-based Generation of Weakest Preconditions and Precise Array Invariants. In Proceedings of the 13th International Conference on Formal Methods in Software Engineering (FormaliSE) (pp. 96–100). IEEE. https://doi.org/10.1109/FORMALISE66629.2025.00016 ( reposiTUm)

Rain, S., Petković Komel, A., Rawson, M., & Kovacs, L. (2025). Game Modeling of Blockchain Protocols. In F. Damiani & M. Farrell (Eds.), Integrated Formal Methods : 20th International Conference, iFM 2025, Paris, France, November 19–21, 2025, Proceedings (pp. 359–377). Springer. https://doi.org/10.1007/978-3-032-10794-7_18 ( 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)

Ciabattoni, A., Eisenhofer, C., & Rozplokhas, D. (2024). Strongly Analytic Calculi for KLM Logics with SMT-Based Prover. In Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (pp. 284–294). https://doi.org/10.24963/kr.2024/27 ( reposiTUm)

Pluska, A., Welke, P., Gärtner, T., & Malhotra, S. (2024). Logical Distillation of Graph Neural Networks. In ICML 2024 Workshop on Mechanistic Interpretability. ICML 2024 Workshop on Mechanistic Interpretability, Vienna, Austria. https://doi.org/10.34726/7099 ( reposiTUm)

Pluska, A., Welke, P., Gärtner, T., & Malhotra, S. (2024). Logical Distillation of Graph Neural Networks. In P. Marquis, M. Ortiz, & M. Pagnucco (Eds.), Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (pp. 920–930). IJCAI Organization. https://doi.org/10.24963/kr.2024/86 ( reposiTUm)

Chimes, M. J., Iosif, R., & Zuleger, F. (2024). Tree-Verifiable Graph Grammars. In Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 165–180). https://doi.org/10.29007/8l13 ( reposiTUm)

Dacík, T., Rogalewicz, A., Vojnar, T., & Zuleger, F. (2024). Deciding Boolean Separation Logic via Small Models. In Tools and Algorithms for the Construction and Analysis of Systems : 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I (pp. 188–206). springer. https://doi.org/10.1007/978-3-031-57246-3_11 ( 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)

Aminof, B., Cooper, L., Rubin, S., Vardi, M. Y., & Zuleger, F. (2024). Probabilistic Synthesis and Verification for LTL on Finite Traces. In P. Marquis, M. Ortiz, & M. Pagnucco (Eds.), Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (pp. 27–37). IJCAI Organization. https://doi.org/10.24963/kr.2024/3 ( reposiTUm)

Aminof, B., De Giacomo, G., Rubin, S., & Zuleger, F. (2024). Proper Linear-time Specifications of Environment Behaviors in Nondeterministic Planning and Reactive Synthesis. In Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (pp. 38–48). IJCAI Organization. https://doi.org/10.24963/kr.2024/4 ( 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)

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)

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)

Fazekas, K., Pollitt, F., Fleury, M., & Biere, A. (2024). Certifying Incremental SAT Solving. In Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 321–340). https://doi.org/10.29007/pdcc ( reposiTUm)

Fazekas, K., Pollitt, F., Fleury, M., & Biere, A. (2024). Incremental Proofs for Bounded Model Checking. In MBMV 2024 : 27. Workshop (pp. 133–143). http://hdl.handle.net/20.500.12708/211103 ( reposiTUm)

Biere, A., Fazekas, K., Fleury, M., & Froleyks, N. (2024). Clausal Congruence Closure. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024), Pune, India. https://doi.org/10.4230/LIPIcs.SAT.2024.6 ( reposiTUm)

Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., & Pollitt, F. (2024). CaDiCaL 2.0. In Computer Aided Verification (pp. 133–152). Springer. https://doi.org/10.1007/978-3-031-65627-9_7 ( 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)

AL-Zu’bi, M., & Weissenbacher, G. (2024). Statistical Profiling of Micro-Architectural Traces and Machine Learning for Spectre Detection: A Systematic Evaluation. In A. Pimentel & V. Bertacco (Eds.), 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE). https://doi.org/10.34726/8339 ( reposiTUm)

Loitzl, A., & Zuleger, F. (2024). Modeling Register Pairs in CompCert. In N. Kosmatov & L. Kovács (Eds.), Integrated Formal Methods : 19th International Conference, IFM 2024 Manchester, UK, November 13–15, 2024 Proceedings (pp. 128–147). Springer. https://doi.org/10.1007/978-3-031-76554-4_8 ( reposiTUm)

Heisinger, S., Heisinger, M., Rebola-Pardo, A., & Seidl, M. (2024). Quantifier Shifting for Quantified Boolean Formulas Revisited. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 325–343). Springer International Publishing. https://doi.org/10.1007/978-3-031-63498-7_20 ( reposiTUm)

Indri, P., Blohm, P., Athavale, A., Bartocci, E., Weissenbacher, G., Maffei, M., Nickovic, D., Gärtner, T., & Malhotra, S. (2024). Distillation based Robustness Verification with PAC Guarantees. In International Conference on Machine Learning 2024 - Next Generation of AI Safety Workshop. International Conference on Machine Learning 2024 - Next Generation of AI Safety Workshop, Vienna, Austria. http://hdl.handle.net/20.500.12708/200890 ( reposiTUm)

Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Ničković, D., & Weissenbacher, G. (2024). Verifying Global Two-Safety Properties in Neural Networks with Confidence. In A. Gurfinkel & V. Ganesh (Eds.), Computer Aided Verification (pp. 329–351). Springer. https://doi.org/10.1007/978-3-031-65630-9_17 ( 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)

Brechelmacher, O., Ničković, D., Nießen, T., Sallinger, S. S., & Weissenbacher, G. (2024). Differential Property Monitoring for Backdoor Detection. In K. Ogata, D. Mery, M. Sun, & S. Liu (Eds.), Formal Methods and Software Engineering (pp. 216–236). Springer. https://doi.org/10.34726/8400 ( reposiTUm)

Biere, A., Fazekas, K., Fleury, M., & Froleyks, N. (2024). Clausal Equivalence Sweeping. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 236–241). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_29 ( 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)

Hader, T., & Ozdemir, A. (2024). An SMT-LIB Theory of Finite Fields. In Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Montreal, Canada, July, 22-23, 2024. 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Montreal, Canada. CEUR Workshop Proceedings. https://doi.org/10.34726/8461 ( 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)

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)

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)

Iosif, R., & Zuleger, F. (2023). Expressiveness Results for an Inductive Logic of Separated Relations. In 34th International Conference on Concurrency Theory (CONCUR 2023). 34th International Conference on Concurrency Theory, CONCUR 2023, Antwerp, Belgium. Schloss-Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.20 ( 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)

Sallinger, S., Weissenbacher, G., & Zuleger, F. (2023). A Formalization of Heisenbugs and Their Causes. In C. Ferreira & T. A. C. Willemse (Eds.), Software Engineering and Formal Methods : 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings (pp. 282–300). Springer. https://doi.org/10.34726/5381 ( 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)

Rebola Pardo, A. (2023). Even Shorter Proofs Without New Variables. In M. Mahajan & F. Slivovsky (Eds.), 26th International Conference on Theory and Applications of Satisfiability Testing (pp. 22:1-22:20). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.SAT.2023.22 ( reposiTUm)

Rawson, M., Wernhard, C., Zombori, Z., & Bibel, W. (2023). Lemmas: Generation, Selection, Application. 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. 153–174). Springer. https://doi.org/10.1007/978-3-031-43513-3_9 ( 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)

Bjørner, N., & Fazekas, K. (2023). On Incremental Pre-processing for SMT. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 41–60). Springer. https://doi.org/10.1007/978-3-031-38499-8_3 ( 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)

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)

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)

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)

Andriushchenko, R., Bartocci, E., Češka, M., Pontiggia, F., & Sallinger, S. S. (2023). Deductive Controller Synthesis for Probabilistic Hyperproperties. In N. Jansen & M. Tribastone (Eds.), Quantitative Evaluation of Systems - 20th International Conference, QEST 2023 (pp. 47–64). Springer. https://doi.org/10.1007/978-3-031-43835-6_20 ( reposiTUm)

Aminof, B., De Giacomo, G., Rubin, S., & Zuleger, F. (2023). Stochastic Best-Effort Strategies for Borel Goals. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Boston, MA, United States of America (the). IEEE. https://doi.org/10.34726/6219 ( 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)

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)

Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., & Biere, A. (2023). IPASIR-UP: User Propagators for CDCL. In M. Mahajan & F. Slivovsky (Eds.), 26th International Conference on Theory and Applications of Satisfiability Testing (pp. 8:1-8:13). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SAT.2023.8 ( 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)

Bhayat, A., Schoisswohl, J., & Rawson, M. (2023). Superposition with Delayed Unification. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 23–40). Springer. https://doi.org/10.1007/978-3-031-38499-8_2 ( 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)

Fazekas, K., Aman, G., & Sakallah, K. (2023). SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 152–161). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_23 ( reposiTUm)

Rozier, K. Y., Shankar, N., Tinelli, C., & Vardi, M. (2023). Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 4–4). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_4 ( reposiTUm)

Hozzová, P., Bendík, J., Nutz, A., & Rodeh, Y. (2023). Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 257–269). EasyChair. https://doi.org/10.29007/h4p7 ( 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)

Pluska, A., & Zuleger, F. (2023). Embedding Intuitionistic into Classical Logic. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 329–349). https://doi.org/10.29007/b294 ( reposiTUm)

Kenison, G., Nieuwveld, J., Ouaknine, J., & Worrell, J. (2023). Positivity Problems for Reversible Linear Recurrence Sequences. In K. Etessami, U. Feige, & G. Puppis (Eds.), 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023) (pp. 1–17). Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2023.130 ( reposiTUm)

Kenison, G., Nosan, K., Shirmohammadi, M., & Worrell, J. (2023). The Membership Problem for Hypergeometric Sequences with Quadratic Parameters. In A. Dickenstein, E. Tsigaridas, & G. Jeronimo (Eds.), ISSAC ’23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation (pp. 407–416). Association for Computing Machinery. https://doi.org/10.1145/3597066.3597121 ( 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)

Kenison, G. (2022). On the Skolem Problem for Reversible Sequences. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) (pp. 61:1-61:15). Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2022.61 ( reposiTUm)

Pagel, J., & Zuleger, F. (2022). Strong-separation Logic. In ESOP 2021: Programming Languages and Systems (pp. 664–692). Springer. https://doi.org/10.1007/978-3-030-72019-3_24 ( 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)

Leutgeb, L., Moser, G., & Zuleger, F. (2022). Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In Computer Aided Verification - 34th International Conference, CAV 2022 (pp. 70–91). https://doi.org/10.1007/978-3-031-13188-2_4 ( reposiTUm)

Leutgeb, L., Moser, G., & Zuleger, F. (2022). ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. In Computer Aided Verification (pp. 99–122). https://doi.org/10.1007/978-3-030-81688-9_5 ( 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)

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)

Holík, L., Peringer, P., Rogalewicz, A., Šoková, V., Vojnar, T., & Zuleger, F. (2022). Low-Level Bi-Abduction. In 36th European Conference on Object-Oriented Programming (ECOOP 2022) (pp. 1–30). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ECOOP.2022.19 ( reposiTUm)

Aminof, B., De Giacomo, G., Rubin, S., & Zuleger, F. (2022). Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (pp. 2525–2531). https://doi.org/10.24963/ijcai.2022/350 ( 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)

Kofnov, A., Moosbrugger, M., Stankovič, M., Bartocci, E., & Bura, E. (2022). Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments. In E. Ábrahám & M. Paolieri (Eds.), Quantitative Evaluation of Systems (pp. 3–25). Springer. https://doi.org/10.1007/978-3-031-16336-4_1 ( reposiTUm)

Rebola Pardo, A. (2022). Interpolants and Interference. In M. Benedikt, P. Rümmer, & C. Wernhard (Eds.), iPRA 2022 : The 4th Workshop on Interpolation: From Proofs to Applications : Book of Abstracts (pp. 27–35). http://hdl.handle.net/20.500.12708/198885 ( reposiTUm)

Eisenhofer, C., & Riener, M. (2022). Automated Instantiation of Control Flow Tracing Exercises. In J. Marcos, W. Neuper, & P. Quaresma (Eds.), Proceedings 10th International Workshop on Theorem Proving Components for Educational Software (pp. 43–58). EPTCS. https://doi.org/10.4204/EPTCS.354.4 ( reposiTUm)

Rawson, M., Suda, M., Hozzová, P., & Reger, G. (2022). Reuse of Introduced Symbols in Automatic Theorem Provers. 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. CEUR-WS.org. https://doi.org/10.34726/4343 ( 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)

Kheterpal, N., Tang, E., & Jeannin, J.-B. (2022). Automating Geometric Proofs of Collision Avoidance with Active Corners. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 359–368). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_43 ( 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)

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)

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)

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)

Pescosta, E., Weissenbacher, G., & Zuleger, F. (2021). Bounded Model Checking of Speculative Non-Interference. In 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD). 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), München, Germany. IEEE. https://doi.org/10.1109/iccad51958.2021.9643462 ( reposiTUm)

Aminof, B., De Giacomo, G., & Rubin, S. (2021). Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. IJCAI 2021 - 30th International Joint Conference on Artificial Intelligence, Montreal, Canada, Canada. https://doi.org/10.24963/ijcai.2021/243 ( reposiTUm)

Aminof, B., De Giacomo, G., Lomuscio, A., Murano, A., & Rubin, S. (2021). Synthesizing Best-effort Strategies under Multiple Environment Specifications. In Proceedings of the Eighteenth International Conference on Principles of Knowledge Representation and Reasoning. KR 2021 - 18th International Conference on Principles of Knowledge Representation and Reasoning, virtual event, Unknown. https://doi.org/10.24963/kr.2021/5 ( 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)

Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2021). Eliminating Message Counters in Synchronous Threshold Automata. In VMCAI 2021: Verification, Model Checking, and Abstract Interpretation (pp. 196–218). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_10 ( reposiTUm)

Durand, T., Fazekas, K., Weissenbacher, G., & Zwirchmayr, J. (2021). Model Checking AUTOSAR Components with CBMC. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 96–101). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_18 ( reposiTUm)

Moosbrugger, M., Bartocci, E., Katoen, J.-P., & Kovács, L. (2021). Automated Termination Analysis of Polynomial Probabilistic Programs. In Programming Languages and Systems (pp. 491–518). Springer. https://doi.org/10.1007/978-3-030-72019-3_18 ( reposiTUm)

Marcel Moosbrugger, Ezio Bartocci, Katoen, J.-P., & Laura Kovács. (2021). The Probabilistic Termination Tool Amber. In Formal Methods. FM 2021 (pp. 667–675). https://doi.org/10.1007/978-3-030-90870-6_36 ( reposiTUm)

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)

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)

Rawson, M., & Reger, G. (2021). A Multithreaded Vampire with Shared Persistent Grounding. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 280–284). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_38 ( 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 (pp. 246–255). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34 ( reposiTUm)

Kenison, G. J., Klurman, O., Lefaucheux, E., Luca, F., Moree, P., Ouaknine, J., Whiteland, M., & Worrell, J. (2021). On Positivity and Minimality for Second-Order Holonomic Sequences. In F. Bonchi & S. Puglisi (Eds.), 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021) (pp. 1–15). Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2021.67 ( reposiTUm)

Fellner, A., Tarrach, T., & Weissenbacher, G. (2020). Language Inclusion for Finite Prime Event Structures. In Verification, Model Checking, and Abstract Interpretation 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16–21, 2020, Proceedings (pp. 314–336). Springer. https://doi.org/10.1007/978-3-030-39322-9_15 ( reposiTUm)

Gleiss, B., & Suda, M. (2020). Layered Clause Selection for Theory Reasoning. In P. Fontaine, K. Korovin, & I. Kotsireas (Eds.), Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop (pp. 34–52). CEUR Workshop Proceedings. http://hdl.handle.net/20.500.12708/58379 ( reposiTUm)

Aminof, B., De Giacomo, G., Lomuscio, A., Murano, A., & Rubin, S. (2020). Synthesizing strategies under expected and exceptional environment behaviors. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization. https://doi.org/10.24963/ijcai.2020/232 ( reposiTUm)

Aminof, B., De Giacomo, G., & Rubin, S. (2020). Stochastic Fairness and Language-Theoretic Fairness in Planning in Nondeterministic Domains. In Proceedings of the Thirtieth International Conference on Automated Planning and Scheduling, Nancy, France (pp. 20–28). AAAI Press. http://hdl.handle.net/20.500.12708/58428 ( reposiTUm)

Pagel, J., & Zuleger, F. (2020). Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. In EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/vkmj ( reposiTUm)

Zuleger, F. (2020). The Polynomial Complexity of Vector Addition Systems with States. In Foundations of Software Science and Computation Structures 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings (pp. 622–641). Springer LNCS. https://doi.org/10.1007/978-3-030-45231-5_32 ( reposiTUm)

Pani, T., Weissenbacher, G., & Zuleger, F. (2020). Thread-modular Counter Abstraction for Parameterized Program Safety. In Formal Methods in Computer-Aided Design (pp. 67–76). TU Wien Academic Press / IEEE. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_13 ( 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)

Labai, N., Simkus, M., & Ortiz de la Fuente, M. M. (2020). An ExpTime Upper Bound for ALC with Integers. In D. Calvanese, E. Erdem, & M. Thielscher (Eds.), Proceedings of the Seventeenth International Conference on Principles of Knowledge Representation and Reasoning. AAAI Press. https://doi.org/10.24963/kr.2020/61 ( 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)

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)

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)

Gleiss, B., & Suda, M. (2020). Layered Clause Selection for Theory Reasoning. In N. Peltier & V. Sofronie-Stokkermans (Eds.), Automated Reasoning (pp. 402–409). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-51074-9_23 ( 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)

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)

Schlaipfer, M., Slivovsky, F., Weissenbacher, G., & Zuleger, F. (2020). Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. In Theory and Applications of Satisfiability Testing – SAT 2020 (pp. 429–446). LNCS. https://doi.org/10.1007/978-3-030-51825-7_30 ( reposiTUm)

Labai, N., Kotek, T., Ortiz, M., & Veith, H. (2020). Pebble-Intervals Automata and FO² with Two Orders. In Language and Automata Theory and Applications (pp. 208–221). Lecture Notes in Computer Science (LNCS). https://doi.org/10.1007/978-3-030-40608-0_14 ( 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). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_33 ( reposiTUm)

Pani, T., Weissenbacher, G., & Zuleger, F. (2020). Thread-modular Counter Abstraction for Parameterized Program Safety. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 67–76). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_13 ( 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)

Damian, A., Drăgoi, C., Militaru, A., & Widder, J. (2019). Communication-Closed Asynchronous Protocols. In Computer Aided Verification (pp. 344–363). Springer. https://doi.org/10.1007/978-3-030-25543-5_20 ( reposiTUm)

Bertrand, N., Konnov, I., Lazić, M., & Widder, J. (2019). Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In W. Fokkink & R. van Glabbeek (Eds.), 30th International Conference on Concurrency Theory (pp. 33:1-33:15). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/LIPIcs.CONCUR.2019.33 ( reposiTUm)

Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2019). Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 357–374). Springer. http://hdl.handle.net/20.500.12708/56804 ( 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)

Aminof, B., De Giacomo, G., Murano, A., & Rubin, S. (2019). Planning under LTL Environment Specifications. In 29th International Conference on Automated Planning and Scheduling (pp. 31–39). AAAI Press. http://hdl.handle.net/20.500.12708/57528 ( reposiTUm)

Aminof, B., Kwiatkowska, M., Maubert, B., Murano, A., & Rubin, S. (2019). Probabilistic Strategy Logic. In 28th International Joint Conference on Artificial Intelligence (pp. 32–38). International Joint Conferences on Artificial Intelligence. http://hdl.handle.net/20.500.12708/57510 ( 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)

Fellner, A., Befrouei, M. T., & Weissenbacher, G. (2019). Mutation Testing with Hyperproperties. In Software Engineering and Formal Methods (pp. 203–221). https://doi.org/10.1007/978-3-030-30446-1_11 ( reposiTUm)

Ignatiev, A., Morgado, A., Marques-Silva, J., & Weissenbacher, G. (2019). Model-Based Diagnosis with Multiple Observations. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence. IJCAI 2019 - 28th International Joint Conference on Artificial Intelligence, Macao, Macao. https://doi.org/10.24963/ijcai.2019/155 ( reposiTUm)

Pagel, J., Matheja, C., & Zuleger, F. (2019). Effective Entailment Checking for Separation Logic with Inductive Definitions. In 25th International Conference, TACAS 2019 (pp. 319–336). Springer. http://hdl.handle.net/20.500.12708/57482 ( reposiTUm)

Sighireanu, M., Pagel, J., Matheja, C., Noll, T., & Zuleger, F. (2019). SL-COMP: Competition of Solvers for Separation Logic. In 25th International Conference, TACAS 2019 (pp. 116–132). Springer. http://hdl.handle.net/20.500.12708/57483 ( reposiTUm)

Metzler, P., Suri, N., & Weissenbacher, G. (2019). Extracting Safe Thread Schedules from Incomplete Model Checking Results. In Model Checking Software (pp. 153–171). LNCS, Springer. https://doi.org/10.1007/978-3-030-30923-7_9 ( 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)

Reger, G., & Suda, M. (2018). Incremental Solving with Vampire. In EPiC Series in Computing. EasyChair, Austria. EasyChair EPiC Series in Computing. https://doi.org/10.29007/6sjl ( reposiTUm)

Gishchenko, I., Maffei, M., & Schneidewind, C. (2018). Foundations and Tools for the Static Analysis of Ethereum Smart Contracts. In G. Weissenbacher & H. Chockler (Eds.), Computer Aided Verification (pp. 51–78). Springer Open. https://doi.org/10.1007/978-3-319-96145-3_4 ( reposiTUm)

Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., & Zuleger, F. (2018). Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. In I. Dillig & J. Palsberg (Eds.), Verification, Model Checking, and Abstract Interpretation : 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Cham. https://doi.org/10.1007/978-3-319-73721-8_1 ( 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)

Kiesl, B., Rebola Pardo, A., & Heule, M. (2018). Extended Resolution Simulates DRAT. In Automated Reasoning (pp. 516–531). LNCS. https://doi.org/10.1007/978-3-319-94205-6_34 ( 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)

Suda, M., & Gleiss, B. (2018). Local Soundness for QBF Calculi. In O. Beyersdorff & C. M. Wintersteiger (Eds.), Theory and Applications of Satisfiability Testing – SAT 2018 (pp. 217–234). LNCS. https://doi.org/10.1007/978-3-319-94144-8_14 ( reposiTUm)

Reger, G., Suda, M., & Voronkov, A. (2018). Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. In D. Beyer & M. Huisman (Eds.), Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (pp. 3–22). LNCS. http://hdl.handle.net/20.500.12708/57680 ( reposiTUm)

Zuleger, F. (2018). Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction. In Static Analysis (pp. 423–444). Springer. https://doi.org/10.1007/978-3-319-99725-4_25 ( reposiTUm)

Kukovec, J., Konnov, I., & Widder, J. (2018). Reachability in Parameterized Systems: All Flavors of Threshold Automata. In S. Schewe & L. Zhang (Eds.), 29th International Conference on Concurrency Theory (CONCUR 2018) (pp. 19:1-19:17). Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CONCUR.2018.19 ( reposiTUm)

Pagel, J., Jovanovic, D., & Weissenbacher, G. (2018). A Separation Logic with Data: Small Models and Automation. In Automated Reasoning (pp. 455–471). LNCS. https://doi.org/10.1007/978-3-319-94205-6_30 ( reposiTUm)

Janota, M., & Suda, M. (2018). Towards Smarter MACE-style Model Finders. In EPiC Series in Computing. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia. EasyChair EPiC Series in Computing. https://doi.org/10.29007/w42s ( reposiTUm)

Barkatou, M. A., & Jaroschek, M. (2018). Desingularization of First Order Linear Difference Systems with Rational Function Coefficients. In M. Kauers (Ed.), Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation. https://doi.org/10.1145/3208976.3208989 ( reposiTUm)

Radiček, I., Barthe, G., Gaboardi, M., Garg, D., & Zuleger, F. (2018). Monadic refinements for relational cost analysis. In Proceedings of the ACM on Programming Languages (pp. 1–32). ACM Digital Library. https://doi.org/10.1145/3158124 ( reposiTUm)

Cadek, P., Danninger, C., Sinn, M., & Zuleger, F. (2018). Using Loop Bound Analysis For Invariant Generation. In 2018 Formal Methods in Computer Aided Design (FMCAD). International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, United States of America (the). FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603005 ( reposiTUm)

Dragoi, C., Lazić, M., & Widder, J. (2018). Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto. In Proceedings of the International Scientific Conference - Sinteza 2018. Sinteza 2018 International Scientific Conference on Information Technology and Data Related Research, Belgrad, Serbia. Singidunum University. https://doi.org/10.15308/sinteza-2018-131-138 ( reposiTUm)

Pani, T., Weissenbacher, G., & Zuleger, F. (2018). Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms. In 2018 Formal Methods in Computer Aided Design (FMCAD). International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, United States of America (the). FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603020 ( 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)

Rebola Pardo, A., & Suda, M. (2018). A Theory of Satisfiability-Preserving Proofs in SAT Solving. In EPiC Series in Computing. International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Montevideo, Uruguay. EasyChair EPiC Series in Computing. https://doi.org/10.29007/tc7q ( reposiTUm)

Radicek, I., Gulwani, S., & Zuleger, F. (2018). Automated clustering and program repair for introductory programming assignments. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. Conference on Programming Language Design and Implementation (PLDI), Ottawa, Canada. ACM. https://doi.org/10.1145/3192366.3192387 ( reposiTUm)

Aminof, B., De Giacomo, G., Murano, A., & Rubin, S. (2018). Synthesis under Assumptions. In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona, 30 October - 2 November 2018 (pp. 615–616). AAAI Press. http://hdl.handle.net/20.500.12708/57751 ( reposiTUm)

Brázdil, T., Chatterjee, K., Kučera, A., Novotný, P., Velan, D., & Zuleger, F. (2018). Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. Symposium on Logic in Computer Science (LICS), Edinburgh, United Kingdom of Great Britain and Northern Ireland (the). ACM. https://doi.org/10.1145/3209108.3209191 ( reposiTUm)

Konnov, I., & Widder, J. (2018). ByMC: Byzantine Model Checker. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems. ISoLA 2018, Proceedings, Part III (pp. 327–342). Springer. https://doi.org/10.1007/978-3-030-03424-5_22 ( reposiTUm)

Forkel, W., Philipp, T., Rebola Pardo, A., & Werner, E. (2017). Fuzzing and Verifying RAT Refutations with Deletion Information. In Florida Artificial Intelligence Research Society Conference (pp. 190–193). AAAI Press. http://hdl.handle.net/20.500.12708/56283 ( reposiTUm)

Suda, M. (2017). CICM 2016 Doctoral Program. In Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016. (p. 1). CEUR-Proceedings. http://hdl.handle.net/20.500.12708/57145 ( reposiTUm)

Philipp, T., & Rebola Pardo, A. (2017). Towards a Semantics of Unsatisfiability Proofs with Inprocessing. In Logic Programming and Automated Reasoning (LPAR) (pp. 65–84). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/57273 ( 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)

Reger, G., Suda, M., & Voronkov, A. (2017). Testing a Saturation-Based Theorem Prover: Experiences and Challenges. In Tests and Proofs (pp. 152–161). Springer. https://doi.org/10.1007/978-3-319-61467-0_10 ( reposiTUm)

Haret, A. (2017). Logic-Based Merging in Fragments of Classical Logic with Inputs from Social Choice Theory. In J. Rothe (Ed.), Algorithmic Decision Theory (pp. 374–378). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-319-67504-6_30 ( reposiTUm)

Reger, G., & Suda, M. (2017). Checkable Proofs for First-Order Theorem Proving. In ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (pp. 55–63). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/57143 ( reposiTUm)

Daviaud, L., Colcombet, T., & Zuleger, F. (2017). Automata and Program Analysis. In Fundamentals of Computation Theory - 21st International Symposium, FCT 2017 (pp. 3–10). http://hdl.handle.net/20.500.12708/57151 ( 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)

Morak, M., Bichler, M., & Woltran, S. (2017). lpopt: A Rule Optimization Tool for Answer Set Programming. In M. Hermenegildo & P. Lopez-Garcia (Eds.), Logic-Based Program Synthesis and Transformation (pp. 114–130). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-319-63139-4_7 ( 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)

Fellner, A., Krenn, W., Schlick, R., Tarrach, T., & Weissenbacher, G. (2017). Model-based, mutation-driven test case generation via heuristic-guided branching search. In Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design. MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, Wien, Austria. ACM. https://doi.org/10.1145/3127041.3127049 ( 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)

Haret, A., & Woltran, S. (2017). Deviation in Belief Change on Fragments of Propositional Logic. In C. Beierle, G. Kern-Isberner, M. Ragni, & F. Stolzenburg (Eds.), Proceedings of the 6th Workshop on Dynamics of Knowledge and Belief (DKB-2017) and the 5th Workshop KI & Kognition (KIK-2017) (p. 13). CEUR Workshop Proceedings. http://hdl.handle.net/20.500.12708/55459 ( reposiTUm)

Labai, N., Homola, M., & Ortiz de la Fuente, M. M. (2017). Constructive Satisfiability Procedure for ALCP(Z) (Preliminary Report). In A. Artale, B. Glimm, & R. Kontchakov (Eds.), Proceedings of the 30th International Workshop on Description Logics (pp. 1–13). CEUR Workshop Proceedings. http://hdl.handle.net/20.500.12708/55478 ( reposiTUm)

Konnov, I., Lazić, M., Veith, H., & Widder, J. (2017). A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Paris, France. ACM. https://doi.org/10.1145/3009837.3009860 ( reposiTUm)

Jakubuv, J., Suda, M., & Urban, J. (2017). Automated Invention of Strategies and Term Orderings for Vampire. In GCAI 2017. 3rd Global Conference on Artificial Intelligence (pp. 121–133). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/57144 ( reposiTUm)

Reger, G., & Suda, M. (2017). Set of Support for Theory Reasoning. In IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017 (pp. 124–134). EasyChair Kalpa Publications in Computing. http://hdl.handle.net/20.500.12708/57149 ( reposiTUm)

Günther, H., Laarman, A., Sokolova, A., & Weissenbacher, G. (2017). Dynamic Reductions for Model Checking Concurrent Software. In Verification, Model Checking, and Abstract Interpretation 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings (pp. 246–265). Springer. https://doi.org/10.1007/978-3-319-52234-0_14 ( reposiTUm)

Lazić, M., Konnov, I., Widder, J., & Bloem, R. (2017). Synthesis of Distributed Algorithms with Parameterized Threshold Guards. In J. Aspnes, A. Bessani, P. Felber, & J. Leitao (Eds.), 21st International Conference on Principles of Distributed Systems (OPODIS 2017) (pp. 32:1-32:20). LIPIcs-Leibniz International Proceedings in Informatics. https://doi.org/10.4230/LIPIcs.OPODIS.2017.32 ( 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)

Shachar, I., Kotek, T., Rinetzky, N., Sagiv, M., Tamir, O., Veith, H., & Zuleger, F. (2017). On the Automated Verification of Web Applications with Embedded SQL. In 20th International Conference on Database Theory, ICDT 2017 (pp. 1–18). http://hdl.handle.net/20.500.12708/57152 ( 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)

Konnov, I., Veith, H., & Widder, J. (2016). What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. In Perspectives of System Informatics : 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (pp. 6–21). Springer. https://doi.org/10.1007/978-3-319-41579-6_2 ( reposiTUm)

Günther, H., Laarman, A., & Weissenbacher, G. (2016). Vienna Verification Tool: IC3 for Parallel Software. In M. Chechik & J.-F. Raskin (Eds.), Tools and Algorithms for the Construction and Analysis of Systems : 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (pp. 954–957). Springer. https://doi.org/10.1007/978-3-662-49674-9_69 ( reposiTUm)

Reger, G., Suda, M., & Voronkov, A. (2016). New Techniques in Clausal Form Generation. In GCAI 2016. 2nd Global Conference on Artificial Intelligence (pp. 11–23). EasyChair. http://hdl.handle.net/20.500.12708/56698 ( reposiTUm)

Suda, M. (2016). Duality in STRIPS planning. In 8th Workshop on Heuristics and Search for Domain-independent Planning (HSDIP), London, UK, June 13, 2016, Proceedings (pp. 21–27). http://hdl.handle.net/20.500.12708/56505 ( reposiTUm)

Hoder, K., Reger, G., Suda, M., & Voronkov, A. (2016). Selecting the Selection. In Automated Reasoning (pp. 313–329). Springer. https://doi.org/10.1007/978-3-319-40229-1_22 ( reposiTUm)

Haret, A., Pfandler, A., & Woltran, S. (2016). Beyond IC Postulates: Classification Criteria for Merging Operators. In G. A. Kaminka, M. Fox, P. Bouquet, E. Hüllermeier, V. Dignum, F. Dignum, & F. van Harmelen (Eds.), ECAI 2016 - 22nd European Conference on Artificial Intelligence (pp. 372–380). IOS Press. http://hdl.handle.net/20.500.12708/56666 ( reposiTUm)

Bichler, M., Morak, M., & Woltran, S. (2016). lpopt: A Rule Optimization Tool for Answer Set Programming. In M. Hermenegildo & P. Lopez-Garcia (Eds.), Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016) (p. 14). http://hdl.handle.net/20.500.12708/56841 ( reposiTUm)

Kotek, T., Veith, H., & Zuleger, F. (2016). Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. In CSL (pp. 1–20). http://hdl.handle.net/20.500.12708/56860 ( reposiTUm)

Beyersdorff, O., Chew, L., Schmidt, R. A., & Suda, M. (2016). Lifting QBF Resolution Calculi to DQBF. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 490–499). Springer. https://doi.org/10.1007/978-3-319-40970-2_30 ( reposiTUm)

Reger, G., Suda, M., & Voronkov, A. (2016). Finding Finite Models in Multi-sorted First-Order Logic. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 323–341). Springer. https://doi.org/10.1007/978-3-319-40970-2_20 ( 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)

Reger, G., Bjørner, N., Suda, M., & Voronkov, A. (2016). AVATAR Modulo Theories. In GCAI 2016. 2nd Global Conference on Artificial Intelligence (pp. 39–52). EasyChair. http://hdl.handle.net/20.500.12708/56715 ( reposiTUm)

Konnov, I., Kotek, T., Wang, Q., Veith, H., Bliudze, S., & Sifakis, J. (2016). Parameterized Systems in BIP: Design and Model Checking. In J. Desharnais & R. Jagadeesan (Eds.), 27th International Conference on Concurrency Theory (CONCUR 2016) (pp. 30:1-30:16). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.30 ( reposiTUm)

Aminof, B., Malvone, V., Murano, A., & Rubin, S. (2016). Extended Graded Modalities in Strategy Logic. In SR (pp. 1–14). http://hdl.handle.net/20.500.12708/56868 ( reposiTUm)

Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2016). Prompt Alternating-Time Epistemic Logics. In KR (pp. 258–267). http://hdl.handle.net/20.500.12708/56836 ( reposiTUm)

Haret, A., Mailly, J.-G., & Woltran, S. (2016). Distributing Knowledge Into Simple Bases. In G. Kern-Isberner & R. Wassermann (Eds.), Proceedings of the 16th International Workshop on Non-monotonic reasoning (p. 9). http://hdl.handle.net/20.500.12708/56764 ( reposiTUm)

Delobelle, J., Haret, A., Konieczny, S., Mailly, J.-G., Rossit, J., & Woltran, S. (2016). Merging of Abstract Argumentation Frameworks. In C. Baral, J. P. Delgrande, & F. Wolter (Eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the 15th International Conference (pp. 33–42). AAAI Press. http://hdl.handle.net/20.500.12708/56766 ( reposiTUm)

Haret, A., Mailly, J.-G., & Woltran, S. (2016). Distributing Knowledge Into Simple Bases. In S. Kambhampati (Ed.), Proceedings of the 25th International Joint Conference on Artificial Intelligence (pp. 1109–1115). IJCAI/AAAI Press. http://hdl.handle.net/20.500.12708/56772 ( 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)

Holzer, A., Schwartz-Narbonne, D., Tabaei Befrouei, M., Weissenbacher, G., & Wies, T. (2016). Error Invariants for Concurrent Traces. In FM 2016: Formal Methods (pp. 370–387). Lecture Notes in Computer Science/Springer. https://doi.org/10.1007/978-3-319-48989-6_23 ( reposiTUm)

Aminof, B., Malvone, V., Murano, A., & Rubin, S. (2016). Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria. In AAMAS (pp. 698–706). http://hdl.handle.net/20.500.12708/56867 ( reposiTUm)

Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2016). Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments. In AAMAS (pp. 1190–1199). http://hdl.handle.net/20.500.12708/56859 ( reposiTUm)

Kotek, T., imkus, M., Veith, H., & Zuleger, F. (2015). Extending ALCQIO with Trees. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), Kyoto, Japan, Austria. IEEE. https://doi.org/10.1109/lics.2015.54 ( reposiTUm)

Blom, S., van Dijk, T., Gijis, K., Laarman, A., Meijer, J., & van de Pol, J. (2015). LTSmin: High-Performance Language-Independent Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 692–707). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_61 ( reposiTUm)

Farzan, A., Holzer, A., & Veith, H. (2015). Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution. In 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST). International Conference on Software Testing, Verification and Validation (ICST), Graz, Austria. https://doi.org/10.1109/icst.2015.7102600 ( reposiTUm)

Weissenbacher, G. (2015). Explaining Heisenbugs. In E. Bartocci & R. Majumdar (Eds.), Runtime Verification (p. XV). Lecture Notes in Computer Science/Springer. http://hdl.handle.net/20.500.12708/56231 ( reposiTUm)

Aminof, B., Rubin, S., & Zuleger, F. (2015). On the expressive power of communication primitives in parameterised systems. 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 (pp. 313–328). Springer. https://doi.org/10.1007/978-3-662-48899-7_22 ( reposiTUm)

Labai, N., & Makowsky, J. A. (2015). Logics of Finite Hankel Rank. In Fields of Logic and Computation II (pp. 237–252). Springer. https://doi.org/10.1007/978-3-319-23534-9_14 ( reposiTUm)

Tabaei Befrouei, M. (2015). Abstraction and mining of traces to explain concurrency bugs. In T. Ströder & W. Thomas (Eds.), Proceedings of the Young Researchers’ Conference “Frontiers of Formal Methods” (p. 5). http://hdl.handle.net/20.500.12708/56440 ( reposiTUm)

Franz, M., Holzer, A., Katzenbeisser, S., Schallhart, C., & Veith, H. (2015). Compilation for Secure Two-Party Computations. In Software Engineering & Management 2015 (pp. 143–145). GI-Edition - Lecture Notes in Informatics (LNI). http://hdl.handle.net/20.500.12708/56383 ( reposiTUm)

Zuleger, F. (2015). Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems. In Computer Science -- Theory and Applications 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings (pp. 426–442). Springer. https://doi.org/10.1007/978-3-319-20297-6_27 ( reposiTUm)

Sinn, M., Veith, H., & Zuleger, F. (2015). Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. In FMCAD (pp. 144–151). http://hdl.handle.net/20.500.12708/56391 ( reposiTUm)

Demyanova, Y., Pani, T., Veith, H., & Zuleger, F. (2015). Empirical Software Metrics for Benchmarking of Verification Tools. In Computer Aided Verification (pp. 561–579). Springer. https://doi.org/10.1007/978-3-319-21690-4_39 ( reposiTUm)

Lewis, M., Kroening, D., & Weissenbacher, G. (2015). Proving Safety with Trace Automata and Bounded Model Checking. In FM 2015: Formal Methods (pp. 325–341). Lecture Notes in Computer Science/Springer. https://doi.org/10.1007/978-3-319-19249-9_21 ( reposiTUm)

Haret, A., Rümmele, S., & Woltran, S. (2015). Merging in the Horn Fragment. In Q. Yang & M. Wooldridge (Eds.), Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence - IJCAI 2015 (pp. 3041–3047). AAAI Press. http://hdl.handle.net/20.500.12708/56274 ( reposiTUm)

Diller, M., Haret, A., Linsbichler, T., Rümmele, S., & Woltran, S. (2015). An extension-based approach to belief revision in abstract argumentation. In Q. Yang & M. Wooldridge (Eds.), Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence - IJCAI 2015 (pp. 2926–2932). AAAI Press. http://hdl.handle.net/20.500.12708/56273 ( reposiTUm)

Aminof, B., Rubin, S., Spegni, F., & Zuleger, F. (2015). Liveness of Parameterized Timed Networks. In Automata, Languages, and Programming (pp. 375–387). Springer. https://doi.org/10.1007/978-3-662-47666-6_30 ( reposiTUm)

Konnov, I., Veith, H., & Widder, J. (2015). SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. In Computer Aided Verification (pp. 85–102). LNCS Springer. https://doi.org/10.1007/978-3-319-21690-4_6 ( reposiTUm)

Kovásznai, G., Veith, H., Fröhlich, A., & Biere, A. (2014). On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. In Mathematical Foundations of Computer Science 2014 (pp. 481–492). Springer / LNCS. https://doi.org/10.1007/978-3-662-44465-8_41 ( reposiTUm)

Colcombet, T., Daviaud, L., & Zuleger, F. (2014). Size-Change Abstraction and Max-Plus Automata. In Mathematical Foundations of Computer Science 2014 (pp. 208–219). Springer / LNCS. https://doi.org/10.1007/978-3-662-44522-8_18 ( reposiTUm)

Fröhlich, A., Kovasznai, G., Biere, A., & Veith, H. (2014). On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. In POS (p. 14). http://hdl.handle.net/20.500.12708/55327 ( reposiTUm)

Kotek, T., Simkus, M., Veith, H., & Zuleger, F. (2014). Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability. In International Workshop on Description Logics (p. 4). http://hdl.handle.net/20.500.12708/55329 ( reposiTUm)

Calvanese, D., Kotek, T., Simkus, M., Veith, H., & Zuleger, F. (2014). Shape and Content: Incorporating Domain Knowledge into Shape Analysis. In International Workshop on Description Logics (p. 4). http://hdl.handle.net/20.500.12708/55330 ( reposiTUm)

Deutsch, T., & Widder, J. (2014). Approaching Verification and Validation Challenges in Smart Grids. In Tagungsband ComForEn 2014 (p. 6). Eigenverlag des Österreich isch en Verbandes für Elektrotec h nik. http://hdl.handle.net/20.500.12708/55738 ( reposiTUm)

Farzan, A., Holzer, A., Razavi, N., & Veith, H. (2014). Concolic Testing of Concurrent Programs. In Software Engineering 2014 (pp. 101–102). LNI. http://hdl.handle.net/20.500.12708/55320 ( reposiTUm)

Calvanese, D., Kotek, T., Šimkus, M., Veith, H., & Zuleger, F. (2014). Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures. In E. Albert & E. Sekerinski (Eds.), Integrated Formal Methods (pp. 3–17). Springer / LNCS. https://doi.org/10.1007/978-3-319-10181-1_1 ( reposiTUm)

Basold, H., Günther, H., Huhn, M., & Milius, S. (2014). An Open Alternative for SMT-Based Verification of Scade Models. In Formal Methods for Industrial Critical Systems (pp. 124–139). Springer / LNCS. https://doi.org/10.1007/978-3-319-10702-8_9 ( reposiTUm)

Beyer, D., Holzer, A., Tautschnig, M., & Veith, H. (2014). Reusing Information in Multi-Goal Reachability Analyses. In Software Engineering 2014 (pp. 97–98). LNI. http://hdl.handle.net/20.500.12708/55321 ( reposiTUm)

Aminof, B., & Rubin, S. (2014). First Cycle Games. In Electronic Proceedings in Theoretical Computer Science (pp. 83–90). EPTCS. https://doi.org/10.4204/eptcs.146.11 ( reposiTUm)

Aminof, B., Kotek, T., Rubin, S., Spegni, F., & Veith, H. (2014). Parameterized Model Checking of Rendezvous Systems. In CONCUR 2014 – Concurrency Theory (pp. 109–124). Springer / LNCS. https://doi.org/10.1007/978-3-662-44584-6_9 ( reposiTUm)

Franz, M., Holzer, A., Katzenbeisser, S., Schallhart, C., & Veith, H. (2014). CBMC-GC: An ANSI C Compiler for Secure Two-Party Computations. In Compiler Construction 23rd International Conference, CC 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (pp. 244–249). Springer / LNCS. https://doi.org/10.1007/978-3-642-54807-9_15 ( reposiTUm)

Konnov, I., Veith, H., & Widder, J. (2014). On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability. In CONCUR 2014 – Concurrency Theory (pp. 125–140). https://doi.org/10.1007/978-3-662-44584-6_10 ( reposiTUm)

Aminof, B., Jacobs, S., Khalimov, A., & Rubin, S. (2014). Parameterized Model Checking of Token-Passing Systems. In Verification, Model Checking, and Abstract Interpretation 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings (pp. 262–281). Springer / LNCS. https://doi.org/10.1007/978-3-642-54013-4_15 ( reposiTUm)

Sastry, S., & Widder, J. (2014). Solvability-Based Comparison of Failure Detectors. In 2014 IEEE 13th International Symposium on Network Computing and Applications. International Symposium on Network Computing and Applications (NCA), Boston, United States of America (the). IEEE Computer Society. https://doi.org/10.1109/nca.2014.46 ( reposiTUm)

Laarman, A., & Wijs, A. (2014). Partial-Order Reduction for Multi-core LTL Model Checking. In Hardware and Software: Verification and Testing (pp. 267–283). Springer / LNCS. https://doi.org/10.1007/978-3-319-13338-6_20 ( reposiTUm)

Gulwani, S., Radiček, I., & Zuleger, F. (2014). Feedback generation for performance problems in introductory programming assignments. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), Hong Kong, Hong Kong. ACM New York, NY, USA. https://doi.org/10.1145/2635868.2635912 ( reposiTUm)

Birgmeier, J., Bradley, A. R., & Weissenbacher, G. (2014). Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR). In Computer Aided Verification (pp. 831–848). Springer / LNCS. https://doi.org/10.1007/978-3-319-08867-9_55 ( reposiTUm)

Zhu, C. S., Weissenbacher, G., & Malik, S. (2014). Silicon fault diagnosis using sequence interpolation with backbones. In ICCAD (pp. 348–355). IEEE Press Piscataway, NJ, USA. http://hdl.handle.net/20.500.12708/55310 ( reposiTUm)

Tabaei Befrouei, M., Wang, C., & Weissenbacher, G. (2014). Abstraction and Mining of Traces to Explain Concurrency Bugs. In Runtime Verification (pp. 162–177). Springer / LNCS. https://doi.org/10.1007/978-3-319-11164-3_14 ( reposiTUm)

Sinn, M., Zuleger, F., & Veith, H. (2014). A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verification (pp. 745–761). Springer / LNCS. https://doi.org/10.1007/978-3-319-08867-9_50 ( reposiTUm)

Günther, H., & Weissenbacher, G. (2014). Incremental bounded software model checking. In Proceedings of the 2014 International SPIN Symposium on Model Checking of Software. International SPIN Symposium on Model Checking of Software (SPIN), Stony Brook, United States of America (the). ACM New York, NY, USA. https://doi.org/10.1145/2632362.2632374 ( reposiTUm)

Drăgoi, C., Henzinger, T. A., Veith, H., Widder, J., & Zufferey, D. (2014). A Logic-Based Framework for Verifying Consensus Algorithms. In Verification, Model Checking, and Abstract Interpretation 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings (pp. 161–181). Springer / LNCS. https://doi.org/10.1007/978-3-642-54013-4_10 ( reposiTUm)

Pötzl, D., & Holzer, A. (2013). Solving Constraints for Generational Search. In 12 (pp. 197–213). Springer / LNCS. https://doi.org/10.1007/978-3-642-38916-0_12 ( 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)

Holzer, A., Schallhart, C., Tautschnig, M., & Veith, H. (2013). On the Structure and Complexity of Rational Sets of Regular Languages. In S. Anil & N. K. Vishnoi (Eds.), FSTTCS 2013 (pp. 377–388). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2013.377 ( reposiTUm)

Cook, B., See, A., & Zuleger, F. (2013). Ramsey vs. Lexicographic Termination Proving. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 47–61). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-36742-7_4 ( reposiTUm)

Kroening, D., Lewis, M., & Weissenbacher, G. (2013). Under-Approximating Loops in C Programs for Fast Counterexample Detection. In Computer Aided Verification (pp. 381–396). Springer / LNCS. https://doi.org/10.1007/978-3-642-39799-8_26 ( reposiTUm)

John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2013). Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms. In Model Checking Software (pp. 209–226). LNCS, Springer. https://doi.org/10.1007/978-3-642-39176-7_14 ( reposiTUm)

Wallner, J. P., Weissenbacher, G., & Woltran, S. (2013). Advanced SAT Techniques for Abstract Argumentation. In Computational Logic in Multi-Agent Systems 14th International Workshop, CLIMA XIV, Corunna, Spain, September 16-18, 2013, Proceedings (pp. 138–154). Springer / LNCS. https://doi.org/10.1007/978-3-642-40624-9_9 ( reposiTUm)

Holzer, A., Karvelas, N., Katzenbeisser, S., & Veith, H. (2013). Challenges in compiler construction for secure two-party computation. In Proceedings of the First ACM workshop on Language support for privacy-enhancing technologies - PETShop ’13. Workshop on language support for privacy-enhancing technologies (PETShop), Berlin, Germany. ACM. https://doi.org/10.1145/2517872.2517876 ( reposiTUm)

Beyer, D., Holzer, A., Tautschnig, M., & Veith, H. (2013). Information Reuse for Multi-goal Reachability Analyses. In Programming Languages and Systems (pp. 472–491). Springer / LNCS. https://doi.org/10.1007/978-3-642-37036-6_26 ( reposiTUm)

Demyanova, Y., Veith, H., & Zuleger, F. (2013). On the concept of variable roles and its use in software analysis. In FMCAD (pp. 226–230). IEEE. http://hdl.handle.net/20.500.12708/54835 ( reposiTUm)

John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2013). Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In FMCAD (pp. 201–209). http://hdl.handle.net/20.500.12708/54827 ( reposiTUm)

John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2013). Brief announcement. In Proceedings of the 2013 ACM symposium on Principles of distributed computing - PODC ’13. ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC), Montreal, Canada. ACM. https://doi.org/10.1145/2484239.2484285 ( reposiTUm)

Farzan, A., Holzer, A., Razavi, N., & Veith, H. (2013). Con2colic testing. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering - ESEC/FSE 2013. Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), Sankt Petersburg, Russian Federation (the). ACM. https://doi.org/10.1145/2491411.2491453 ( reposiTUm)

Franz, M., Holzer, A., Majumdar, R., Parno, B., & Veith, H. (2013). The first workshop on language support for privacy-enhancing technologies (PETShop’13). In Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security - CCS ’13. ACM Conference on Computer and Communications Security (CCS), Washington, United States of America (the). ACM. https://doi.org/10.1145/2508859.2509032 ( reposiTUm)

Leue, S., & Befrouei, M. T. (2013). Mining Sequential Patterns to Explain Concurrent Counterexamples. In Model Checking Software (pp. 264–281). LNCS, Springer. https://doi.org/10.1007/978-3-642-39176-7_17 ( reposiTUm)

Kruckman, A., Rubin, S., Sheridan, J., & Zax, B. (2012). A Myhill-Nerode theorem for automata with advice. In M. Faella & A. Murano (Eds.), Electronic Proceedings in Theoretical Computer Science (pp. 238–246). Electronic Proceedings in Theoretical Computer Science. https://doi.org/10.4204/eptcs.96.18 ( reposiTUm)

Razavi, N., Farzan, A., & Holzer, A. (2012). Bounded-Interference Sequentialization for Testing Concurrent Programs. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. (ISoLA 2012), Proceedings, Part I (pp. 372–387). Springer. https://doi.org/10.1007/978-3-642-34026-0_28 ( reposiTUm)

Sastry, S., Welch, J. L., & Widder, J. (2012). Wait-Free Stabilizing Dining Using Regular Registers. In Principles of Distributed Systems 16th International Conference, OPODIS 2012, Rome, Italy, December 18-20, 2012, Proceedings (pp. 284–299). LNCS / Springer. https://doi.org/10.1007/978-3-642-35476-2_20 ( reposiTUm)

Rabinovich, A., & Rubin, S. (2012). Interpretations in Trees with Countably Many Branches. In 2012 27th Annual IEEE Symposium on Logic in Computer Science. Symposium on Logic in Computer Science (LICS), Edinburgh, United Kingdom of Great Britain and Northern Ireland (the). IEEE. https://doi.org/10.1109/lics.2012.65 ( reposiTUm)

Holzer, A., Kroening, D., Schallhart, C., Tautschnig, M., & Veith, H. (2012). Proving Reachability Using FShell. In C. Flanagan & B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 538–541). Springer. https://doi.org/10.1007/978-3-642-28756-5_43 ( reposiTUm)

Weissenbacher, G. (2012). Interpolant Strength Revisited. In Theory and Applications of Satisfiability Testing – SAT 2012 (pp. 312–326). LNCS / Springer. https://doi.org/10.1007/978-3-642-31612-8_24 ( reposiTUm)

Függer, M., & Widder, J. (2012). Efficient Checking of Link-Reversal-Based Concurrent Systems. In CONCUR 2012- Concurrency Theory 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, September 4-7, 2012. Proceedings (pp. 486–499). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-32940-1_34 ( reposiTUm)

Charlie Shucheng, Z., Weissenbacher, G., & Malik, S. (2012). Coverage-Based Trace Signal Selection for Fault Localisation in Post-silicon Validation. In Hardware and Software: Verification and Testing (pp. 132–147). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-39611-3_16 ( reposiTUm)

Schwartz-Narbonne, D., Weissenbacher, G., & Malik, S. (2012). Parallel Assertions for Architectures with Weak Memory Models. In Automated Technology for Verification and Analysis (pp. 254–268). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-33386-6_21 ( reposiTUm)

Holzer, A., Franz, M., Katzenbeisser, S., & Veith, H. (2012). Secure two-party computations in ANSI C. In Proceedings of the 2012 ACM conference on Computer and communications security - CCS ’12. ACM Conference on Computer and Communications Security (CCS), Washington, United States of America (the). ACM. https://doi.org/10.1145/2382196.2382278 ( 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)

Bünte, S., Zolda, M., Tautschnig, M., & Kirner, R. (2011). Improving the Confidence in Measurement-Based Timing Analysis. In 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC 2011) (pp. 144–151). IEEE. http://hdl.handle.net/20.500.12708/53907 ( reposiTUm)

Zuleger, F., Sinn, M., Gulwani, S., & Veith, H. (2011). Bound Analysis of Imperative Programs with the Size-Change Abstraction. In E. Yahav (Ed.), Static Analysis (pp. 280–297). Springer. https://doi.org/10.1007/978-3-642-23702-7_22 ( reposiTUm)

Holzer, A., Januzaj, V., Kugele, S., Langer, B., Schallhart, C., Tautschnig, M., & Veith, H. (2011). Seamless Testing for Models and Code. In G. Goos, J. Hartmanis, & J. van Leeuwen (Eds.), Fundamental Approaches to Software Engineering (pp. 278–293). Springer. https://doi.org/10.1007/978-3-642-19811-3_20 ( reposiTUm)

Haberl, W., Herrmannsdoerfer, M., Kugele, S., Tautschnig, M., & Wechs, M. (2010). Seamless Model-Driven Development Put into Practice. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification, and Validation (pp. 18–32). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-642-16558-0_4 ( reposiTUm)

Holzer, A., Januzaj, V., Kugele, S., & Tautschnig, M. (2010). Timely Time Estimates. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification, and Validation (pp. 33–46). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-642-16558-0_5 ( reposiTUm)

Holzer, A., Schallhart, C., Tautschnig, M., & Veith, H. (2010). How did you specify your test suite. In C. Pecheur, J. Andrews, & E. Di Nitto (Eds.), Proceedings of the IEEE/ACM international conference on Automated software engineering - ASE ’10. ACM. https://doi.org/10.1145/1858996.1859084 ( reposiTUm)

Holzer, A., Tautschnig, M., Schallhart, C., & Veith, H. (2010). An Introduction to Test Specification in FQL. In S. Barner, J. G. Harris, D. Kroening, & O. Raz (Eds.), Hardware and Software: Verification and Testing (pp. 9–22). Springer. https://doi.org/10.1007/978-3-642-19583-9_5 ( reposiTUm)

Gulwani, S., & Zuleger, F. (2010). The reachability-bound problem. In B. G. Zorn & A. Aiken (Eds.), Proceedings of the 2010 ACM SIGPLAN conference on Programming language design and implementation - PLDI ’10. PLDI’10 Proceedings of teh ACM SIGPLAN conference on Programming language design and implementation. https://doi.org/10.1145/1806596.1806630 ( reposiTUm)

Schmid, U., Steininger, A., & Veith, H. (2007). Towards a Systematic Design of Fault-Tolerant Asynchronous Circuits. In Fachtagung Zuverlässigkeit und Entwurf (pp. 173–174). VDE Verlag. http://hdl.handle.net/20.500.12708/51805 ( reposiTUm)

Samer, M., & Veith, H. (2005). Deterministic CTL Query Solving. In J. Chomicki & D. Toman (Eds.), Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (pp. 156–165). IEEE Computer Society. http://hdl.handle.net/20.500.12708/50996 ( reposiTUm)

Sagar, N., Fenkam, P., Veith, H., Gall, H., Kirda, E., & Jha, S. (2003). Integrating Publish/Subscribe into a Mobile Teamwork Support Platform. In Proceedings of the 15th International Conference on Software Engineering and Knowledge Engineering (pp. 510–517). http://hdl.handle.net/20.500.12708/50936 ( reposiTUm)

Book Contributions

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)

Gmeiner, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2014). Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms. In Formal Methods for Executable Software Models (pp. 122–171). Springer. https://doi.org/10.1007/978-3-319-07317-0_4 ( reposiTUm)

Katzenbeisser, S., Kinder, J., & Veith, H. (2011). Malware Detection. In H. C. A. van Tilborg & S. Jajodia (Eds.), Encyclopedia of Cryptography and Security (pp. 752–755). Springer-Verlag. https://doi.org/10.1007/978-1-4419-5906-5_838 ( reposiTUm)

Samer, M., & Veith, H. (2006). From Temporal Logic Queries to Vacuity Detection. In E. Clarke (Ed.), Verification of Infinite-State Systems with Applications to Security (pp. 149–167). IOS Press. http://hdl.handle.net/20.500.12708/25351 ( reposiTUm)

Books

Computer Aided Verification. (2018). In H. Chockler & G. Weissenbacher (Eds.), Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-319-96142-2 ( reposiTUm)

Computer Aided Verification. (2018). In H. Chockler & G. Weissenbacher (Eds.), Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-319-96145-3 ( reposiTUm)

Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., & Widder, J. (2015). Decidability of Parameterized Verification. In Synthesis Lectures on Distributed Computing Theory (p. 170). Morgan & Claypool Publishers. https://doi.org/10.2200/s00658ed1v01y201508dct013 ( reposiTUm)

CAV. (2013). In N. Sharygina & H. Veith (Eds.), Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-642-39799-8 ( reposiTUm)

Conference Proceedings

Irfan, A., & Kaufmann, D. (Eds.). (2025). Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design – FMCAD 2025 (Vol. 6). TU Wien Academic Press. https://doi.org/10.34727/2025/isbn.978-3-85448-084-6 ( 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)

Stewart, D., & Weissenbacher, G. (Eds.). (2017). Proceedings of Formal Methods in Computer Aided Design, FMCAD 2017. FMCAD Inc. https://doi.org/10.15781/T2JS9HQ7C ( reposiTUm)

Charron-Bost, B., Merz, S., Rybalchenko, A., & Widder, J. (Eds.). (2013). Formal Verification of Distributed Algorithms. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/DagRep.3.4.1 ( reposiTUm)

Presentations

Kovacs, L. (2025, June). Automated Reasoning [Conference Presentation]. Open Science Day 2025, Wien, Austria. https://doi.org/10.34726/9740 ( reposiTUm)

Sextl, F., Rogalewicz, A., Vojnar, T., & Zuleger, F. (2025, January 21). Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract) [Conference Presentation]. Theory and Practice of Static Analysis 2025, Denver, Colorado, United States of America (the). http://hdl.handle.net/20.500.12708/212815 ( reposiTUm)

Kaufmann, D. (2025, September 24). Verifying Arithmetic Circuits with Polynomials [Conference Presentation]. SYNASC 2025: 27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania. ( reposiTUm)

Nießen, T., & Weissenbacher, G. (2024, January 16). Finding counterexamples to ∀∃ hyperproperties [Conference Presentation]. Formal Methods for Incorrectness 2024, London, United Kingdom of Great Britain and Northern Ireland (the). https://doi.org/10.34726/5455 ( reposiTUm)

Sextl, F. (2024, September 17). With Biabduction towards Memory Safety across the Rust-C-FFI [Presentation]. Doctoral Symposium, TU Wien, Austria. http://hdl.handle.net/20.500.12708/204201 ( reposiTUm)

Nastran, M., Peschek, P., Walendzik, I., Rath, J., Fickl, B., Schubert, J. S., Szabo, G., Wilhelm, R. A., Schmidt, J., Eder, D., & Bayer-Skoff, B. (2024, June 24). High-yield liquid phase exfoliation of graphene utilizing low boiling co-solvent solutions and ammonia [Poster Presentation]. NT24, Cambridge, Boston, United States of America (the). http://hdl.handle.net/20.500.12708/203125 ( reposiTUm)

Fazekas, K. (2024, June 26). Incremental SAT Solvers in Practice [Conference Presentation]. SAT/SMT/AR Summer School 2024, Nancy, France. ( reposiTUm)

Fazekas, K. (2024, October 14). SAT modulo IPASIR-UP [Presentation]. Dagstuhl Seminar 24421: SAT and Interactions, Wadern, Germany. ( reposiTUm)

Ait El Manssour, R., Kenison, G. J., Shirmohammadi, M., & Varonka, A. (2024, September 19). Simple Linear Loops: Algebraic Invariants and Synthesis [Presentation]. 18th International Conference on Reachability Problems (RP 2024), Wien, Austria. https://doi.org/10.1007/978-3-031-72621-7 ( reposiTUm)

Fazekas, K., Pollitt, F., Fleury, M., & Biere, A. (2024, July 23). Certifying Incremental SAT Solving [Conference Presentation]. 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Montreal, Canada. http://hdl.handle.net/20.500.12708/210159 ( 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)

Petkovic Komel, A. (2022, May 20). The essence of elaboration [Conference Presentation]. Workshop on Syntax and Semantics of Type Thoery, Stockholm, Sweden. http://hdl.handle.net/20.500.12708/153774 ( 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)

Eisenhofer, C. (2022, September 14). User-Propagation for Custom Theories in SMT Solving [Presentation]. 14th Alpine Verification Meeting, Frauenchiemsee, Germany. http://hdl.handle.net/20.500.12708/154343 ( 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)

Petkovic Komel, A. (2022, July 31). The essence of type-theoretic elaboration [Conference Presentation]. Women In Logic, Haifa, Israel. http://hdl.handle.net/20.500.12708/153703 ( 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)

Rath, J. (2019). Subsumption Demodulation in First-Order Theorem Proving. First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal. http://hdl.handle.net/20.500.12708/86992 ( 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)

Stankovic, M. (2019). Automatic Analysis for Prob-Solvable Loops. 13th Alpine Verification Meeting (AVM), Brno, Czechia. http://hdl.handle.net/20.500.12708/87000 ( 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 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. (2018). Symbol Elimination for Program Analysis. Highlights of Logic, Games and Automata, Paris, France. http://hdl.handle.net/20.500.12708/86841 ( reposiTUm)

Reger, G., & Suda, M. (2017). Measuring progress to predict success: Can a good proof strategy be evolved? AITP 2017 - The Second Conference on Artificial Intelligence and Theorem Proving, Obergurgl, Austria. http://hdl.handle.net/20.500.12708/86616 ( 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)

Weissenbacher, G. (2017). Interpolation-based Model Checking and IC3. Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Znaim, Czechia. http://hdl.handle.net/20.500.12708/86685 ( reposiTUm)

Reger, G., & Suda, M. (2017). Local proofs and AVATAR. Fourth Vampire Workshop - VAMPIRE 2017, Göteborg, Sweden. http://hdl.handle.net/20.500.12708/86626 ( reposiTUm)

Reger, G., Suda, M., & Voronkov, A. (2017). Instantiation and Pretending to be an SMT Solver with Vampire. SMT 2017 - 15th International Workshop on Satisfiability Modulo Theories, Heidelberg, Germany. http://hdl.handle.net/20.500.12708/86623 ( reposiTUm)

Reger, G., & Suda, M. (2017). Incremental Solving with Vampire. Fourth Vampire Workshop - VAMPIRE 2017, Göteborg, Sweden. http://hdl.handle.net/20.500.12708/86625 ( 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. (2017). Symbol Elimination for Program Analysis. ETH Workshop on Software Correctness and Reliability, Zürich, Switzerland. http://hdl.handle.net/20.500.12708/86690 ( reposiTUm)

Reger, G., Suda, M., & Voronkov, A. (2017). Recent Improvements of Theory Reasoning in Vampire. IWIL 2017 - 12th International Workshop on the Implementation of Logics, Maun, Botswana. http://hdl.handle.net/20.500.12708/86627 ( 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)

Reger, G., & Suda, M. (2016). When Should We Add Theory Axioms And Which Ones? 1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016, Obergurgl, Austria. http://hdl.handle.net/20.500.12708/86349 ( 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)

Barkatou, M., & Jaroschek, M. (2016). Desingularization of First Order Linear Difference Systems with Rational Function Coefficients. 22nd Conference on Applications of Computer Algebra, Kassel, Germany. http://hdl.handle.net/20.500.12708/86470 ( reposiTUm)

Jaroschek, M. (2016). Quantifier Elimination Over The Reals. Tutorial on SMT and Polynomial Arithmetic, Gothenburg, Sweden. http://hdl.handle.net/20.500.12708/86471 ( reposiTUm)

Kovacs, L. (2016). Enjoying Research at the Intersection of Math and Computer Science. Women in Science Workshop Series (WISE), Gothenburg, Sweden. http://hdl.handle.net/20.500.12708/86439 ( reposiTUm)

Kovacs, L. (2016). With a Timisoara Background in the Scientific World of Computer Science and. Timisoara Hungarian Science Festival, Timisoara, Romania. http://hdl.handle.net/20.500.12708/86440 ( reposiTUm)

Reger, G., & Suda, M. (2016). Revisiting Global Subsumption. The Third Vampire Workshop, VAMPIRE 2016, Coimbra, Portugal. http://hdl.handle.net/20.500.12708/86350 ( reposiTUm)

Biere, A., Kiesl, B., Seidl, M., & Suda, M. (2016). Blocked clauses in first-order logic. The Third Vampire Workshop, VAMPIRE 2016, Coimbra, Portugal. http://hdl.handle.net/20.500.12708/86389 ( reposiTUm)

Kiesl, B., & Suda, M. (2016). First-Order Logic and Blocked Clauses. 4th International Workshop on Quantified Boolean Formulas (QBF 2016), Bordeaux, France. http://hdl.handle.net/20.500.12708/86390 ( reposiTUm)

Reger, G., Suda, M., & Voronkov, A. (2016). New Techniques in Clausal Form Generation. Prague Automated Reasoning Seminar, Prag, Czechia. http://hdl.handle.net/20.500.12708/86391 ( reposiTUm)

Suda, M. (2016). The mystery of QBF tautologies. Prague Automated Reasoning Seminar, Prag, Czechia. http://hdl.handle.net/20.500.12708/86392 ( reposiTUm)

Lazić, M., Konnov, I., Veith, H., & Widder, J. (2016). Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms. 7th Workshop on Program Semantics, Specification and Verification: Theory and Applications, St. Petersburg, Russian Federation (the). http://hdl.handle.net/20.500.12708/86426 ( reposiTUm)

Weissenbacher, G. (2016). Interpolation algorithms and their applications in model checking. Automata, Logic and Games, Singapore, Singapore. http://hdl.handle.net/20.500.12708/86305 ( reposiTUm)

Jaroschek, M., & Barkatou, M. (2016). Desingularization of First Order Linear Difference Systems with Rational Function Coefficients. RIMS workshop, Algebraic Statistics and Symbolic Computation, Kyoto, Japan. http://hdl.handle.net/20.500.12708/86472 ( reposiTUm)

Konnov, I., Lazić, M., Veith, H., & Widder, J. (2016). Parameterized Verification of Liveness of Distributed Algorithms. Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Wien, Austria. http://hdl.handle.net/20.500.12708/86425 ( reposiTUm)

Aminof, B., Kotek, T., Rubin, S., Spegni, F., & Veith, H. (2014). Parameterized Model Checking of Rendezvous Systems. Algorithmics of Infinite State Systems workshop, Wien, Austria. http://hdl.handle.net/20.500.12708/85898 ( reposiTUm)

Farzan, A., Holzer, A., Razavi, N., & Veith, H. (2014). Concolic Testing of Concurrent Programs. International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2), Wien, Austria. http://hdl.handle.net/20.500.12708/85899 ( reposiTUm)

Kovasznai, G., Veith, H., Fröhlich, A., & Biere, A. (2014). On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. 15th International Workshop on Logic and Computational Complexity and Workshop in Honor of Neil Immerman’s 60th Birthday (LCC 2014/ImmermanFest), Wien, Austria. http://hdl.handle.net/20.500.12708/85894 ( reposiTUm)

Kotek, T. (2014). Explaining the decompositionality of monadic second order logic using applications to combinatorics. Fun With Formal Methods Workshop, Wien, Austria. http://hdl.handle.net/20.500.12708/85897 ( reposiTUm)

Rubin, S. (2014). Parameterised Verification of Robot Protocols: An Automata Theoretic Approach. Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Wien, Austria. http://hdl.handle.net/20.500.12708/85896 ( reposiTUm)

Baaz, M., Eiter, T., & Veith, H. (2014). Vienna Summer of Logic. Vienna Summer of Logic, Wien, Austria, Austria. http://hdl.handle.net/20.500.12708/121057 ( reposiTUm)

Veith, H. (2014). Model Checking of Fault-Tolerant Distributed Algorithms. Summer School 2014: Verification Technology, Systems & Applications, Luxemburg, Luxembourg. http://hdl.handle.net/20.500.12708/86028 ( reposiTUm)

Calimeri, F., Fink, M., Germano, S., Humenberger, A., Ianni, G., Redl, C., Stepanova, D., & Tucci, A. (2014). AngryHEX: An Angry Birds-playing Agent based on HEX-Programs. AngryBirds Competition 2014, Prag, Czechia. http://hdl.handle.net/20.500.12708/85870 ( reposiTUm)

Rubin, S. (2014). First Cycle Games. Highlights of Logic, Games and Automata, Paris, France. http://hdl.handle.net/20.500.12708/85895 ( reposiTUm)

Veith, H. (2014). History of Model Checking. Clarke Symposium 2014: Celebrating 25 Years of Model Checking, Pittsburgh, United States of America (the). http://hdl.handle.net/20.500.12708/86029 ( reposiTUm)

John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Counter Attack against Byzantine Generals. Alpine Verification Meeting, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85359 ( reposiTUm)

John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Who is afraid of Model Checking Distributed Algorithms? PUMA/RISE Seminar, Traunkirchen, Austria. http://hdl.handle.net/20.500.12708/85435 ( reposiTUm)

John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Parameterized Model Checking of Fault-tolerant Distributed Algorithms. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Germany. http://hdl.handle.net/20.500.12708/85432 ( reposiTUm)

Weissenbacher, G. (2012). Labelled Interpolation Systems. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Germany. http://hdl.handle.net/20.500.12708/85433 ( reposiTUm)

Veith, H. (2012). Secure Two-Party Computation in ANSI C. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Germany. http://hdl.handle.net/20.500.12708/85434 ( reposiTUm)

Konnov, I., Veith, H., & Widder, J. (2012). Who is afraid of Model Checking Distributed Algorithms? Workshop on Exploiting Concurrency Efficiently and Correctly, Berkeley, United States of America (the). http://hdl.handle.net/20.500.12708/85358 ( reposiTUm)

Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Microsoft Research Lecture, Microsoft Research Cambridge, UK, EU. http://hdl.handle.net/20.500.12708/84682 ( reposiTUm)

Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Theory Seminar, Queen Mary University, UK, EU. http://hdl.handle.net/20.500.12708/84681 ( reposiTUm)

Zuleger, F. (2011). Resource Bound Analysis of Imperative Programs. RiSE Seminar, Klosterneuburg, Austria. http://hdl.handle.net/20.500.12708/85142 ( reposiTUm)

Függer, M., & Widder, J. (2011). On Efficient Checking of Link-reversal-based Concurrent Systems. PUMA/RISE Seminar, Traunkirchen, Austria. http://hdl.handle.net/20.500.12708/85311 ( reposiTUm)

Zuleger, F. (2011). Termination and Bound Analysis of Imperative Programs. Workshop on Logic and Computer Science, Vienna, Austria. http://hdl.handle.net/20.500.12708/85314 ( reposiTUm)

Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Software Systems Group Seminar, NICTA, Australien, Non-EU. http://hdl.handle.net/20.500.12708/85313 ( reposiTUm)

Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Austrian Society for Rigorous Systems Engineering (ARiSE) workshop together with PUMA workshop, Traunkirchen, Austria, Austria. http://hdl.handle.net/20.500.12708/85312 ( reposiTUm)

Veith, H. (2011). How did you specify your test suite? Alpine Verification Meeting, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85158 ( reposiTUm)

Veith, H. (2002). Verfahren zur Komplexitätsreduktion im Model Checking. Universität Saarbrücken, Saarbrücken, Deutschland, Austria. http://hdl.handle.net/20.500.12708/84104 ( reposiTUm)

Veith, H. (2002). Model Checking - Recent Results and Developments. University of Leeds, Leeds, United Kingdom, Austria. http://hdl.handle.net/20.500.12708/84105 ( reposiTUm)

Veith, H. (2002). Verfahren zur Komplexitätsreduktion im Model Checking. Technische Universität München, Austria. http://hdl.handle.net/20.500.12708/84107 ( reposiTUm)

Veith, H. (2002). Verfahren zur Komplexitätsreduktion im Model Checking. Technische Universität Graz, Austria. http://hdl.handle.net/20.500.12708/84106 ( reposiTUm)

Reports

Codel, C., Fazekas, K., Heule, M. J. H., & Iser, M. (Eds.). (2025). Proceedings of SAT Competition 2025 : Solver and Benchmark Descriptions. https://doi.org/10.34726/10379 ( reposiTUm)

Bichler, M., Bliem, B., Moldovan, M., Morak, M., & Woltran, S. (2016). Treewidth-Preserving Modeling in ASP (DBAI-TR-2016-97). http://hdl.handle.net/20.500.12708/39078 ( reposiTUm)

Preprints

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

Rawson, M. (2022). Linear Refutation and Clause Splitting. EasyChair Preprints. ( reposiTUm)

Labai, N., Simkus, M., & Ortiz, M. (2020). An ExpTime Upper Bound for ALC with Integers (Extended Version). arXiv. https://doi.org/10.48550/arXiv.2006.02078 ( reposiTUm)

Labai, N., Kotek, T., Ortiz, M., & Veith, H. (2019). Pebble-Intervals Automata and FO2 with Two Orders (Extended Version). arXiv. https://doi.org/10.48550/arXiv.1912.00171 ( reposiTUm)