Paper critique and presentation guidelines.
 

Date	Presenter	Paper
12/04	Aleksey Kalinovski	Simple formally verified compiler in Lean by Leo Okawa Ericson Uppsala Universitet, PhD Dissertation, 2021 @PhdThesis{ericson21:_simpl_lean, author = {Leo Okawa Ericson}, title = {Simple formally verified compiler in Lean}, school = {Uppsala Universitet}, year = 2021}
	Zachary Gordon	A Framework for Debugging Automated Program Verification Proofs via Proof Actions by Cho, Chanhee and Zhou, Yi and Bosamiya, Jay and Parno, Bryan CAV 2024 @InProceedings{10.1007/978-3-031-65627-9_17, author="Cho, Chanhee and Zhou, Yi and Bosamiya, Jay and Parno, Bryan", editor="Gurfinkel, Arie and Ganesh, Vijay", title="A Framework for Debugging Automated Program Verification Proofs via Proof Actions", booktitle="Computer Aided Verification", year="2024", publisher="Springer Nature Switzerland", address="Cham", pages="348--361", abstract="Many program verification tools provide automation via SMT solvers, allowing them to automatically discharge many proofs. However, when a proof fails, it can be hard to understand why it failed or how to fix it. The main feedback the developer receives is simply the verification result (i.e., success or failure), with no visibility into the solver's internal state. To assist developers using such tools, we introduce ProofPlumber, a novel and extensible proof-action framework for understanding and debugging proof failures. Proof actions act on the developer's source-level proofs (e.g., assertions and lemmas) to determine why they failed and potentially suggest remedies. We evaluate ProofPlumber by writing a collection of proof actions that capture common proof debugging practices. We produce 17 proof actions, each only 29--177 lines of code.", isbn="978-3-031-65627-9" }
	Siew Goh	Automatic verification of transparency protocols (extended version) by Vincent Cheval and José Moreira and Mark Ryan arXiv 2023 @misc{cheval2023automaticverificationtransparencyprotocols, title={Automatic verification of transparency protocols (extended version)}, author={Vincent Cheval and José Moreira and Mark Ryan}, year={2023}, eprint={2303.04500}, archivePrefix={arXiv}, primaryClass={cs.CR}, url={https://arxiv.org/abs/2303.04500}, }
12/08	Ashvin Ganesan	Baldur: Whole-Proof Generation and Repair with Large Language Models by First, Emily and Rabe, Markus N. and Ringer, Talia and Brun, Yuriy ESEC/FSE 2023 @inproceedings{10.1145/3611643.3616243, author = {First, Emily and Rabe, Markus N. and Ringer, Talia and Brun, Yuriy}, title = {Baldur: Whole-Proof Generation and Repair with Large Language Models}, year = {2023}, isbn = {9798400703270}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3611643.3616243}, doi = {10.1145/3611643.3616243}, abstract = {Formally verifying software is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by training a model to predict one proof step at a time and using that model to search through the space of possible proofs. This paper introduces a new method to automate formal verification: We use large language models, trained on natural language and code and fine-tuned on proofs, to generate whole proofs at once. We then demonstrate that a model fine-tuned to repair generated proofs further increasing proving power. This paper: (1) Demonstrates that whole-proof generation using transformers is possible and is as effective but more efficient than search-based techniques. (2) Demonstrates that giving the learned model additional context, such as a prior failed proof attempt and the ensuing error message, results in proof repair that further improves automated proof generation. (3) Establishes, together with prior work, a new state of the art for fully automated proof synthesis. We reify our method in a prototype, Baldur, and evaluate it on a benchmark of 6,336 Isabelle/HOL theorems and their proofs, empirically showing the effectiveness of whole-proof generation, repair, and added context. We also show that Baldur complements the state-of-the-art tool, Thor, by automatically generating proofs for an additional 8.7\% of the theorems. Together, Baldur and Thor can prove 65.7\% of the theorems fully automatically. This paper paves the way for new research into using large language models for automating formal verification.}, booktitle = {Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering}, pages = {1229–1241}, numpages = {13}, keywords = {Proof assistants, automated formal verification, large language models, machine learning, proof repair, proof synthesis}, location = {San Francisco, CA, USA}, series = {ESEC/FSE 2023} }
	Ru Aguilar	CoqQ: Foundational Verification of Quantum Programs by Zhou, Li and Barthe, Gilles and Strub, Pierre-Yves and Liu, Junyi and Ying, Mingsheng POPL 2023. @article{10.1145/3571222, author = {Zhou, Li and Barthe, Gilles and Strub, Pierre-Yves and Liu, Junyi and Ying, Mingsheng}, title = {CoqQ: Foundational Verification of Quantum Programs}, year = {2023}, issue_date = {January 2023}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {7}, number = {POPL}, url = {https://doi.org/10.1145/3571222}, doi = {10.1145/3571222}, abstract = {CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.}, journal = {Proc. ACM Program. Lang.}, month = jan, articleno = {29}, numpages = {33}, keywords = {Quantum Programs, Proof Assistants, Program Logics, Mathematical Libraries} }