Bio

I am a fourth year PhD student advised by Clark Barrett and part of the CENTAUR lab at Stanford University. My research interests lie in automated reasoning and formal verification. I am currently working on proofs for SMT solvers.

Contact

Additional Info

  • Mail Code: 9025

All Publications

  • Generating and Exploiting Automated Reasoning Proof Certificates COMMUNICATIONS OF THE ACM Barbosa, H., Barrett, C., Cook, B., Dutertre, B., Kremer, G., Lachnitt, H., Niemetz, A., Notzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Tinelli, C., Zohar, Y. 2023; 66 (10): 86-95

    View details for DOI 10.1145/3587692

    View details for Web of Science ID 001075786500018

  • cvc5: A Versatile and Industrial-Strength SMT Solver Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Notzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y., Fisman, D., Rosu, G. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 415-442

    View details for DOI 10.1007/978-3-030-99524-9_24

    View details for Web of Science ID 000782396700024

  • Flexible Proof Production in an Industrial-Strength SMT Solver Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., Notzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y., Tinelli, C., Barrett, C., Blanchette, J., Kovacs, L., Pattinson, D. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 15-35

    View details for DOI 10.1007/978-3-031-10769-6_3

    View details for Web of Science ID 000876376400003

  • Axiomatic Hardware-Software Contracts for Security Mosier, N., Lachnitt, H., Nemati, H., Trippel, C., ACM ASSOC COMPUTING MACHINERY. 2022: 72-86

    View details for DOI 10.1145/3470496.3527412

    View details for Web of Science ID 000852702500006

  • Certified Quantum Computation in Isabelle/HOL. Journal of automated reasoning Bordg, A., Lachnitt, H., He, Y. 2021; 65 (5): 691-709

    Abstract

    In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch's algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory.

    View details for DOI 10.1007/s10817-020-09584-7

    View details for PubMedID 34720282

    View details for PubMedCentralID PMC8550268

  • Certified Quantum Computation in Isabelle/HOL JOURNAL OF AUTOMATED REASONING Bordg, A., Lachnitt, H., He, Y. 2020

    View details for DOI 10.1007/s10817-020-09584-7

    View details for Web of Science ID 000601507400001