Publications

@article{DBLP:journals/cacm/BarbosaBCDKLNNOPRTZ23,
  author       = {Haniel Barbosa and
                  Clark W. Barrett and
                  Byron Cook and
                  Bruno Dutertre and
                  Gereon Kremer and
                  Hanna Lachnitt and
                  Aina Niemetz and
                  Andres N{\"{o}}tzli and
                  Alex Ozdemir and
                  Mathias Preiner and
                  Andrew Reynolds and
                  Cesare Tinelli and
                  Yoni Zohar},
  title        = {Generating and Exploiting Automated Reasoning Proof Certificates},
  journal      = {Commun. {ACM}},
  volume       = {66},
  number       = {10},
  pages        = {86--95},
  year         = {2023},
  url          = {https://doi.org/10.1145/3587692},
  doi          = {10.1145/3587692},
  timestamp    = {Sun, 12 Nov 2023 02:19:18 +0100},
  biburl       = {https://dblp.org/rec/journals/cacm/BarbosaBCDKLNNOPRTZ23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/BordgLH21,
  author       = {Anthony Bordg and
                  Hanna Lachnitt and
                  Yijun He},
  title        = {Certified Quantum Computation in Isabelle/HOL},
  journal      = {J. Autom. Reason.},
  volume       = {65},
  number       = {5},
  pages        = {691--709},
  year         = {2021},
  url          = {https://doi.org/10.1007/s10817-020-09584-7},
  doi          = {10.1007/S10817-020-09584-7},
  timestamp    = {Tue, 15 Jun 2021 17:22:49 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/BordgLH21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BinderLK26,
  code         = {https://doi.org/10.4230/artifacts.27121},
  author       = {Sage Binder and
                  Hanna Lachnitt and
                  Katherine Kosaian},
  editor       = {Ekaterina Komendantskaya and
                  Tobias Nipkow},
  title        = {Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs
                  to Structured Isar},
  booktitle    = {17th International Conference on Interactive Theorem Proving, {ITP}
                  2026, Lisbon, Portugal, July 26-29, 2026},
  series       = {LIPIcs},
  volume       = {382},
  pages        = {18:1--18:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2026},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2026.18},
  doi          = {10.4230/LIPICS.ITP.2026.18},
  timestamp    = {Sat, 12 Sep 2026 15:32:53 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BinderLK26.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cav/ReynoldsSBIJLMNPZJBT26,
  code         = {https://doi.org/10.5281/zenodo.19867026},
  author       = {Andrew Reynolds and
                  Hans{-}J{\"{o}}rg Schurr and
                  Haniel Barbosa and
                  Ofec Israel and
                  Jibiana Jakpor and
                  Hanna Lachnitt and
                  Abdalrhman Mohamed and
                  Aina Niemetz and
                  Mathias Preiner and
                  Yoni Zohar and
                  Robert B. Jones and
                  Clark W. Barrett and
                  Cesare Tinelli},
  editor       = {Eva Darulova and
                  Anthony W. Lin and
                  Philipp R{\"{u}}mmer},
  title        = {The Cooperating Proof Calculus: Comprehensive Proofs for an {SMT}
                  Solver},
  booktitle    = {Computer Aided Verification - 38th International Conference, {CAV}
                  2026, Lisbon, Portugal, July 26-29, 2026, Proceedings, Part {II}},
  series       = {Lecture Notes in Computer Science},
  volume       = {16683},
  pages        = {188--212},
  publisher    = {Springer},
  year         = {2026},
  url          = {https://doi.org/10.1007/978-3-032-32526-6\_9},
  doi          = {10.1007/978-3-032-32526-6\_9},
  timestamp    = {Tue, 08 Sep 2026 16:10:32 +0200},
  biburl       = {https://dblp.org/rec/conf/cav/ReynoldsSBIJLMNPZJBT26.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/LachnittFBJA0SB25,
  author       = {Hanna Lachnitt and
                  Mathias Fleury and
                  Haniel Barbosa and
                  Jibiana Jakpor and
                  Bruno Andreotti and
                  Andrew Reynolds and
                  Hans{-}J{\"{o}}rg Schurr and
                  Clark W. Barrett and
                  Cesare Tinelli},
  editor       = {Yannick Forster and
                  Chantal Keller},
  title        = {Improving the {SMT} Proof Reconstruction Pipeline in Isabelle/HOL},
  booktitle    = {16th International Conference on Interactive Theorem Proving, {ITP}
                  2025, Reykjavik, Iceland, September 28 - October 1, 2025},
  series       = {LIPIcs},
  volume       = {352},
  pages        = {26:1--26:22},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2025},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2025.26},
  doi          = {10.4230/LIPICS.ITP.2025.26},
  timestamp    = {Sun, 21 Jun 2026 17:19:52 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/LachnittFBJA0SB25.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/fmcad/HitarthCLD24,
  author       = {S. Hitarth and
                  Cayden R. Codel and
                  Hanna Lachnitt and
                  Bruno Dutertre},
  editor       = {Nina Narodytska and
                  Philipp R{\"{u}}mmer},
  title        = {Extending {DRAT} to {SMT}},
  booktitle    = {Formal Methods in Computer-Aided Design, {FMCAD} 2024, Prague, Czech
                  Republic, October 15-18, 2024},
  pages        = {1--11},
  publisher    = {{IEEE}},
  year         = {2024},
  url          = {https://doi.org/10.34727/2024/isbn.978-3-85448-065-5\_8},
  doi          = {10.34727/2024/ISBN.978-3-85448-065-5\_8},
  timestamp    = {Tue, 27 Jan 2026 17:17:18 +0100},
  biburl       = {https://dblp.org/rec/conf/fmcad/HitarthCLD24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/smt/LachnittFA0BNBT23,
  code         = {https://doi.org/10.5281/zenodo.10048664},
  author       = {Hanna Lachnitt and
                  Mathias Fleury and
                  Leni Aniva and
                  Andrew Reynolds and
                  Haniel Barbosa and
                  Andres N{\"{o}}tzli and
                  Clark W. Barrett and
                  Cesare Tinelli},
  editor       = {St{\'{e}}phane Graham{-}Lengrand and
                  Mathias Preiner},
  title        = {Automatic Verification of {SMT} Rewrites in Isabelle/HOL},
  booktitle    = {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},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {3429},
  pages        = {78},
  publisher    = {CEUR-WS.org},
  year         = {2023},
  url          = {https://ceur-ws.org/Vol-3429/abstract14.pdf},
  timestamp    = {Sat, 30 Sep 2023 09:57:02 +0200},
  biburl       = {https://dblp.org/rec/conf/smt/LachnittFA0BNBT23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tacas/AndreottiLB23,
  author       = {Bruno Andreotti and
                  Hanna Lachnitt and
                  Haniel Barbosa},
  editor       = {Sriram Sankaranarayanan and
                  Natasha Sharygina},
  title        = {Carcara: An Efficient Proof Checker and Elaborator for {SMT} Proofs
                  in the Alethe Format},
  booktitle    = {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}},
  series       = {Lecture Notes in Computer Science},
  volume       = {13993},
  pages        = {367--386},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-30823-9\_19},
  doi          = {10.1007/978-3-031-30823-9\_19},
  timestamp    = {Wed, 17 May 2023 21:55:33 +0200},
  biburl       = {https://dblp.org/rec/conf/tacas/AndreottiLB23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/isca/MosierLNT22,
  author       = {Nicholas Mosier and
                  Hanna Lachnitt and
                  Hamed Nemati and
                  Caroline Trippel},
  editor       = {Valentina Salapura and
                  Mohamed Zahran and
                  Fred Chong and
                  Lingjia Tang},
  title        = {Axiomatic hardware-software contracts for security},
  booktitle    = {{ISCA} '22: The 49th Annual International Symposium on Computer Architecture,
                  New York, New York, USA, June 18 - 22, 2022},
  pages        = {72--86},
  publisher    = {{ACM}},
  year         = {2022},
  url          = {https://doi.org/10.1145/3470496.3527412},
  doi          = {10.1145/3470496.3527412},
  timestamp    = {Sat, 30 Sep 2023 09:49:51 +0200},
  biburl       = {https://dblp.org/rec/conf/isca/MosierLNT22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tacas/BarbosaBBKLMMMN22,
  author       = {Haniel Barbosa and
                  Clark W. Barrett and
                  Martin Brain and
                  Gereon Kremer and
                  Hanna Lachnitt and
                  Makai Mann and
                  Abdalrhman Mohamed and
                  Mudathir Mohamed and
                  Aina Niemetz and
                  Andres N{\"{o}}tzli and
                  Alex Ozdemir and
                  Mathias Preiner and
                  Andrew Reynolds and
                  Ying Sheng and
                  Cesare Tinelli and
                  Yoni Zohar},
  editor       = {Dana Fisman and
                  Grigore Rosu},
  title        = {cvc5: {A} Versatile and Industrial-Strength {SMT} Solver},
  booktitle    = {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}},
  series       = {Lecture Notes in Computer Science},
  volume       = {13243},
  pages        = {415--442},
  publisher    = {Springer},
  year         = {2022},
  url          = {https://doi.org/10.1007/978-3-030-99524-9\_24},
  doi          = {10.1007/978-3-030-99524-9\_24},
  timestamp    = {Fri, 29 Apr 2022 14:50:36 +0200},
  biburl       = {https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/BarbosaRKLNNOPV22,
  author       = {Haniel Barbosa and
                  Andrew Reynolds and
                  Gereon Kremer and
                  Hanna Lachnitt and
                  Aina Niemetz and
                  Andres N{\"{o}}tzli and
                  Alex Ozdemir and
                  Mathias Preiner and
                  Arjun Viswanathan and
                  Scott Viteri and
                  Yoni Zohar and
                  Cesare Tinelli and
                  Clark W. Barrett},
  editor       = {Jasmin Blanchette and
                  Laura Kov{\'{a}}cs and
                  Dirk Pattinson},
  title        = {Flexible Proof Production in an Industrial-Strength {SMT} Solver},
  booktitle    = {Automated Reasoning - 11th International Joint Conference, {IJCAR}
                  2022, Haifa, Israel, August 8-10, 2022, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {13385},
  pages        = {15--35},
  publisher    = {Springer},
  year         = {2022},
  url          = {https://doi.org/10.1007/978-3-031-10769-6\_3},
  doi          = {10.1007/978-3-031-10769-6\_3},
  timestamp    = {Wed, 07 Dec 2022 23:12:37 +0100},
  biburl       = {https://dblp.org/rec/conf/cade/BarbosaRKLNNOPV22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/mkm/KovacsLS20,
  author       = {Laura Kov{\'{a}}cs and
                  Hanna Lachnitt and
                  Stefan Szeider},
  editor       = {Christoph Benzm{\"{u}}ller and
                  Bruce R. Miller},
  title        = {Formalizing Graph Trail Properties in Isabelle/HOL},
  booktitle    = {Intelligent Computer Mathematics - 13th International Conference,
                  {CICM} 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12236},
  pages        = {190--205},
  publisher    = {Springer},
  year         = {2020},
  url          = {https://doi.org/10.1007/978-3-030-53518-6\_12},
  doi          = {10.1007/978-3-030-53518-6\_12},
  timestamp    = {Sun, 02 Oct 2022 16:12:21 +0200},
  biburl       = {https://dblp.org/rec/conf/mkm/KovacsLS20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-2103-03607,
  author       = {Laura Kov{\'{a}}cs and
                  Hanna Lachnitt and
                  Stefan Szeider},
  title        = {Formalizing Graph Trail Properties in Isabelle/HOL},
  journal      = {CoRR},
  volume       = {abs/2103.03607},
  year         = {2021},
  url          = {https://arxiv.org/abs/2103.03607},
  eprinttype    = {arXiv},
  eprint       = {2103.03607},
  timestamp    = {Mon, 15 Mar 2021 17:30:55 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2103-03607.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-2112-10511,
  author       = {Nicholas Mosier and
                  Hanna Lachnitt and
                  Hamed Nemati and
                  Caroline Trippel},
  title        = {Relational Models of Microarchitectures for Formal Security Analyses},
  journal      = {CoRR},
  volume       = {abs/2112.10511},
  year         = {2021},
  url          = {https://arxiv.org/abs/2112.10511},
  eprinttype    = {arXiv},
  eprint       = {2112.10511},
  timestamp    = {Tue, 04 Jan 2022 15:59:27 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2112-10511.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/BordgLH20,
  pubtype      = {other},
  author       = {Anthony Bordg and
                  Hanna Lachnitt and
                  Yijun He},
  title        = {Isabelle Marries Dirac: a Library for Quantum Computation and Quantum
                  Information},
  journal      = {Arch. Formal Proofs},
  volume       = {2020},
  year         = {2020},
  url          = {https://www.isa-afp.org/entries/Isabelle\_Marries\_Dirac.html},
  timestamp    = {Thu, 10 Dec 2020 13:31:57 +0100},
  biburl       = {https://dblp.org/rec/journals/afp/BordgLH20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}