Page Not Found
Page not found. Your pixels are in another canvas.
Sitemap
A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.
Pages
Page not in menu
This is a page not in th emain menu
Posts
Future Blog Post
Published:
This post will show up by default. To disable scheduling of future posts, edit config.yml and set future: false.
Blog Post number 4
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
Blog Post number 3
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
Blog Post number 2
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
Blog Post number 1
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
publications
Formalizing Graph Trail Properties in Isabelle/HOL
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
Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
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
Certified Quantum Computation in Isabelle/HOL
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
Formalizing Graph Trail Properties in Isabelle/HOL
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
Relational Models of Microarchitectures for Formal Security Analyses
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
Axiomatic hardware-software contracts for security
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
cvc5: A Versatile and Industrial-Strength SMT Solver
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
Flexible Proof Production in an Industrial-Strength SMT Solver
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
Automatic Verification of SMT Rewrites in Isabelle/HOL
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
Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format
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
Generating and Exploiting Automated Reasoning Proof Certificates
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
Extending DRAT to SMT
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
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL
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
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
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
The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver
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