| [1] | Bruno Andreotti, Hanna Lachnitt, and Haniel Barbosa. Carcara: An efficient proof checker and elaborator for SMT proofs in the alethe format. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I, volume 13993 of Lecture Notes in Computer Science, pages 367--386. Springer, 2023. [ bib | DOI | https ] |
| [2] | Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, and Cesare Tinelli. Automatic verification of SMT rewrites in isabelle/hol. In Stéphane Graham-Lengrand and Mathias Preiner, editors, Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), Rome, Italy, July, 5-6, 2023, volume 3429 of CEUR Workshop Proceedings, page 78. CEUR-WS.org, 2023. [ bib | .pdf ] |
| [3] | Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 415--442. Springer, 2022. [ bib | DOI | https ] |
| [4] | Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, and Clark W. Barrett. Flexible proof production in an industrial-strength SMT solver. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 15--35. Springer, 2022. [ bib | DOI | https ] |
| [5] | Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. Axiomatic hardware-software contracts for security. In Valentina Salapura, Mohamed Zahran, Fred Chong, and Lingjia Tang, editors, ISCA '22: The 49th Annual International Symposium on Computer Architecture, New York, New York, USA, June 18 - 22, 2022, pages 72--86. ACM, 2022. [ bib | DOI | https ] |
| [6] | Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. Relational models of microarchitectures for formal security analyses. CoRR, abs/2112.10511, 2021. [ bib | arXiv | https ] |
| [7] | Anthony Bordg, Hanna Lachnitt, and Yijun He. Certified quantum computation in isabelle/hol. J. Autom. Reason., 65(5):691--709, 2021. [ bib | DOI | https ] |
| [8] | Laura Kovács, Hanna Lachnitt, and Stefan Szeider. Formalizing graph trail properties in isabelle/hol. In Christoph Benzmüller and Bruce R. Miller, editors, Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science, pages 190--205. Springer, 2020. [ bib | DOI | https ] |
| [9] | Anthony Bordg, Hanna Lachnitt, and Yijun He. Isabelle marries dirac: a library for quantum computation and quantum information. Arch. Formal Proofs, 2020, 2020. [ bib | .html ] |
