Published in CICM, 2020
Recommended citation: Laura Kovács, Hanna Lachnitt, and Stefan Szeider. “Formalizing Graph Trail Properties in Isabelle/HOL.” Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, 2020. https://doi.org/10.1007/978-3-030-53518-6_12
Published in Arch. Formal Proofs, 2020
Recommended citation: Anthony Bordg, Hanna Lachnitt, and Yijun He. “Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information.” Arch. Formal Proofs, 2020. https://www.isa-afp.org/entries/Isabelle_Marries_Dirac.html
Published in J. Autom. Reason., 2021
Recommended citation: Anthony Bordg, Hanna Lachnitt, and Yijun He. “Certified Quantum Computation in Isabelle/HOL.” J. Autom. Reason., 2021. https://doi.org/10.1007/S10817-020-09584-7
Published in arXiv:2103.03607, 2021
Recommended citation: Laura Kovács, Hanna Lachnitt, and Stefan Szeider. “Formalizing Graph Trail Properties in Isabelle/HOL.” arXiv:2103.03607, 2021. https://arxiv.org/abs/2103.03607
Published in arXiv:2112.10511, 2021
Recommended citation: Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. “Relational Models of Microarchitectures for Formal Security Analyses.” arXiv:2112.10511, 2021. https://arxiv.org/abs/2112.10511
Published in ISCA, 2022
Recommended citation: Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. “Axiomatic hardware-software contracts for security.” ISCA '22: The 49th Annual International Symposium on Computer Architecture, New York, New York, USA, June 18 - 22, 2022, 2022. https://doi.org/10.1145/3470496.3527412
Published in TACAS, 2022
Recommended citation: 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.” 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, 2022. https://doi.org/10.1007/978-3-030-99524-9_24
Published in IJCAR, 2022
Recommended citation: 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.” Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, 2022. https://doi.org/10.1007/978-3-031-10769-6_3
Published in SMT, 2023
Recommended citation: 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.” 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, 2023. https://ceur-ws.org/Vol-3429/abstract14.pdf
Published in TACAS, 2023
Recommended citation: Bruno Andreotti, Hanna Lachnitt, and Haniel Barbosa. “Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format.” 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, 2023. https://doi.org/10.1007/978-3-031-30823-9_19
Published in Commun. ACM, 2023
Recommended citation: Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, and Yoni Zohar. “Generating and Exploiting Automated Reasoning Proof Certificates.” Commun. ACM, 2023. https://doi.org/10.1145/3587692
Published in FMCAD, 2024
Recommended citation: S. Hitarth, Cayden R. Codel, Hanna Lachnitt, and Bruno Dutertre. “Extending DRAT to SMT.” Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, 2024. https://doi.org/10.34727/2024/ISBN.978-3-85448-065-5_8
Published in ITP, 2025
Recommended citation: Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, and Cesare Tinelli. “Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL.” 16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025, 2025. https://doi.org/10.4230/LIPICS.ITP.2025.26
Published in ITP, 2026
Recommended citation: Sage Binder, Hanna Lachnitt, and Katherine Kosaian. “Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar.” 17th International Conference on Interactive Theorem Proving, ITP 2026, Lisbon, Portugal, July 26-29, 2026, 2026. https://doi.org/10.4230/LIPICS.ITP.2026.18
Published in CAV, 2026
Recommended citation: Andrew Reynolds, Hans-Jörg Schurr, Haniel Barbosa, Ofec Israel, Jibiana Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, Yoni Zohar, Robert B. Jones, Clark W. Barrett, and Cesare Tinelli. “The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver.” Computer Aided Verification - 38th International Conference, CAV 2026, Lisbon, Portugal, July 26-29, 2026, Proceedings, Part II, 2026. https://doi.org/10.1007/978-3-032-32526-6_9