More Like this

1. A formally certified end-to-end implementation of Shor’s factorization algorithm

   https://doi.org/10.1073/pnas.2218775120  

   Peng, Yuxiang; Hietala, Kesha; Tao, Runzhou; Li, Liyi; Rand, Robert; Hicks, Michael; Wu, Xiaodi (May 2023, Proceedings of the National Academy of Sciences)

   Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but it is useful only if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors—“bugs.” Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. With such methods, a programmer writes a mathematical specification alongside the program and semiautomatically proves the program correct with respect to it. The proof’s validity is automatically confirmed—certified—by a “proof assistant.” Formal methods have successfully yielded high-assurance classical software artifacts, and the underlying technology has produced certified proofs of major mathematical theorems. As a demonstration of the feasibility of applying formal methods to quantum programming, we present a formally certified end-to-end implementation of Shor’s prime factorization algorithm, developed as part of a framework for applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain a high-assurance implementation of large-scale quantum applications in a principled way. 

   more » « less
2. Foundational Integration Verification of a Cryptographic Server

   https://doi.org/10.1145/3656446  

   Erbsen, Andres; Philipoom, Jade; Jamner, Dustin; Lin, Ashley; Gruetter, Samuel; Pit-Claudel, Clément; Chlipala, Adam (June 2024, Proceedings of the ACM on Programming Languages)

   We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of functional programs including compilers for C-like and functional languages. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Connecting these components is a minimalistic specification style based on functional programs and assertions over simple objects, omnisemantics for program execution, and basic separation logic for memory layout. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through public-key authenticated network messages, and its proof shows total functional correctness including static bounds on memory usage. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks. 

   more » « less
3. Student use of three registers for representing set relationships to reason about logic in undergraduate transition to proof courses

   Dawkins, PC; Roh, KH; Bruner, O; Gonzalez, M (November 2024, Psychology in Mathematics Education - North America)

   In transition to proof courses for undergraduates, we conducted teaching experiments supporting students to learn logic and proofs rooted in set-based meanings. We invited students to reason about sets using three representational systems: set notation (including symbolic expressions and set-builder notation), mathematical statements (largely in English), and Euler diagrams. In this report, we share evidence regarding how these three representations provided students with tools for reasoning and communicating about set relationships to explore the logic of statements. By analyzing student responses to tasks that asked them to translate between the representational systems, we gain insight into the accessibility and productivity of these tools for such instruction. 

   more » « less
4. Verified sequential Malloc/Free

   https://doi.org/10.1145/3381898.3397211  

   Appel, Andrew W.; Naumann, David A. (June 2020, International Symposium on Memory Management)

   null (Ed.)

   We verify the functional correctness of an array-of-bins (segregated free-lists) single-thread malloc/free system with respect to a correctness specification written in separation logic. The memory allocator is written in standard C code compatible with the standard API; the specification is in the Verifiable C program logic, and the proof is done in the Verified Software Toolchain within the Coq proof assistant. Our "resource-aware" specification can guarantee when malloc will successfully return a block, unlike the standard Posix specification that allows malloc to return NULL whenever it wants to. We also prove subsumption (refinement): the resource-aware specification implies a resource-oblivious spec. 

   more » « less
5. Structural temporal logic for mechanized program verification

   Ioannidis, Eleftherios; Zakowski, Yannick; Zdancewic, Steve; Angel, Sebastian (October 2025, Proceedings of the ACM on programming languages)

   Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of models such as traces and automata. Reasoning happens at a very low-level, requiring complex nested (co-)inductive proof techniques and familiarity with proof assistant mechanics (e.g., the guardedness checker). Further, reasoning at the level of models instead of program constructs creates a verification gap that loses the benefits of modularity and composition enjoyed by structural program logics such as Hoare Logic. To address this verification gap, and the lack of compositional proof techniques for temporal specifications, we propose Ticl, a new structural temporal logic. Using Ticl, we encode complex (co-)inductive proof techniques as structural lemmas and focus our reasoning on variants and invariants. We show that it is possible to perform compositional proofs of general temporal properties in a proof assistant, while working at a high level of abstraction. We demonstrate the benefits of Ticl by giving mechanized proofs of safety and liveness properties for programs with scheduling, concurrent shared memory, and distributed consensus, demonstrating a low proof-to-code ratio. 

   more » « less