Attempts to design hardware using dafny
summary
Uses Dafny with SMT solver to write programs that generate hardware and prove properties about them; attempts include a function that turns a circuit struct into a directed graph and a proof that validity of the input circuit implies validity of the graph. Builds a combinational full adder construction as a circuit-producing function (three input nodes to two output nodes). Work currently struggles with helping the SMT solver—proofs require many helper lemmas and manual breadcrumbs and are only partially complete.
AI-written summary · about
related talks
14mEmbedding Quantum Program Verification into Dafny
21mVerified VCG and Verified Compiler for Dafny
19mLean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
17mGenerating Circuits with Generators
21mHelping users to reduce Brittleness in their Dafny programs - a success story
18mBaking for Dafny: A CakeML Backend for Dafny
01h 02mLanguage Design meets Verifying Compilers
18mDeferring the Details and Deriving Programs