2024W

• Formal Methods in Computer Science / 185.A93 / UE
• Formal Methods in Computer Science / 185.291 / VU

2025S

• Program and System Verification / 184.741 / VU

• Even Shorter Proofs Without New Variables / 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
  Project: LCS (2017–2025)
• Interpolants and Interference / 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
  Project: LCS (2017–2025)
• Interference-based proofs in SAT solving / Rebola-Pardo, A. (2021). Interference-based proofs in SAT solving [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.102507
  Download: PDF (2.86 MB)
• Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs / Altmanninger, J., & Rebola Pardo, A. (2020). Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs. In J. Blanchette & C. Hritcu (Eds.), CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM. https://doi.org/10.1145/3372885.3373821
  Download: PDF (737 KB)
• RAT Elimination / Rebola Pardo, A., & Weissenbacher, G. (2020). RAT Elimination. In L. Kovacs & E. Albert (Eds.), EPiC Series in Computing. EasyChair. https://doi.org/10.29007/fccb
• Extended Resolution Simulates DRAT / 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
• A Theory of Satisfiability-Preserving Proofs in SAT Solving / 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, Austria. EasyChair EPiC Series in Computing. https://doi.org/10.29007/tc7q
• Towards a Semantics of Unsatisfiability Proofs with Inprocessing / 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
  Project: BITVECTOR (2016–2020)
• Fuzzing and Verifying RAT Refutations with Deletion Information / 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
  Project: BITVECTOR (2016–2020)
• DRAT proofs for XOR reasoning / Philipp, T., & Rebola-Pardo, A. (2016). DRAT proofs for XOR reasoning. In L. Michael & A. Kakas (Eds.), Logics in Artificial Intelligence : 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings. Springer Cham. https://doi.org/10.1007/978-3-319-48758-8_27
  Download: PDF (390 KB)

• A Tiny tweak to proof generation in miniSat-based SAT solvers & a complete and efficient DRAT proof checker / Altmanninger, J. (2019). A Tiny tweak to proof generation in miniSat-based SAT solvers & a complete and efficient DRAT proof checker [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.62440
  Download: PDF (3.44 MB)