2025S

• Seminar Formal Methods / 181.221 / SE

• Reducibility Constraints in Superposition / Hajdu, M., Kovács, L., Rawson, M., & Voronkov, A. (2024). Reducibility Constraints in Superposition. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 115–132). https://doi.org/10.1007/978-3-031-63498-7_8
  Download: PDF (541 KB)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model / Jeanteur, S., Kovács, L., Maffei, M., & Rawson, M. (2024). CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. In 2024 IEEE Symposium on Security and Privacy (SP) (pp. 3165–3183). IEEE. https://doi.org/10.1109/SP54263.2024.00246
  Projects: Browsec (2018–2024) / CDL-BOT (2020–2025) / DLDaI (2022–2024) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026) / SPFBT (2020–2024)
• Embedding the Connection Calculus in Satisfiability Modulo Theories / Eisenhofer, C., Kovács, L., & Rawson, M. (2024). Embedding the Connection Calculus in Satisfiability Modulo Theories. In Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) (pp. 54–63). CEUR-WS.org. https://doi.org/10.34726/5394
  Download: PDF (248 KB)
  Projects: ARTIST (2021–2026) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)
• CheckMate: Automated Game-Theoretic Security Reasoning / Brugger, L. S., Kovács, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2023). CheckMate: Automated Game-Theoretic Security Reasoning. In CCS ’23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 1407–1421). Association for Computing Machinery. https://doi.org/10.1145/3576915.3623183
  Download: PDF (1.15 MB)
  Project: SFB SPyCoDe (2023–2026)
• Non-Classical Logics in Satisfiability Modulo Theories / Eisenhofer, C., Alassaf, R., Rawson, M., & Kovács, L. (2023). Non-Classical Logics in Satisfiability Modulo Theories. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 24–36). Springer. https://doi.org/10.1007/978-3-031-43513-3_2
  Download: PDF (423 KB)
  Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
• Lemmas: Generation, Selection, Application / 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
  Project: ARTIST (2021–2026)
• Superposition with Delayed Unification / 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
  Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
• SAT-Based Subsumption Resolution / Coutelier, R., Kovács, L., Rawson, M., & Rath, J. (2023). SAT-Based Subsumption Resolution. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 190–206). Springer. https://doi.org/10.1007/978-3-031-38499-8_11
• Linear Refutation and Clause Splitting / Rawson, M. (2022). Linear Refutation and Clause Splitting. EasyChair Preprints.
• The RAPID Software Verification Framework / Georgiou, P., Gleiss, B., Bhayat, A., Rawson, M., Kovács, L., & Reger, G. (2022). The RAPID Software Verification Framework. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 255–260). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_32
  Download: PDF (308 KB)
• The Vampire Approach to Induction (short paper) / Hajdu, M., Kovács, L., Rawson, M., & Voronkov, A. (2022). The Vampire Approach to Induction (short paper). In B. Konev, C. Schon, & A. Steen (Eds.), PAAR 2022. Practical Aspects of Automated Reasoning 2022.  Proceedings of the Workshop on Practical Aspects of Automated Reasoning. https://doi.org/10.34726/4103
  Download: PDF (836 KB)
• Reuse of Introduced Symbols in Automatic Theorem Provers / 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
  Download: PDF (859 KB)
  Project: ARTIST (2021–2026)
• Automating Security Analysis of Off-Chain Protocols / Brugger, L. S., Kovacs, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2022, August 11). Automating Security Analysis of Off-Chain Protocols [Conference Presentation]. 4th International Workshop on Formal Methods for Blockchains, Haifa, Israel. https://doi.org/10.34726/3523
  Download: PDF (265 KB)
  Project: ARTIST (2021–2026)
• A Multithreaded Vampire with Shared Persistent Grounding / 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
  Download: PDF (289 KB)