Student research contest talks
summary
Six five-minute student reports present concrete artifacts and results: a semantics for higher-order hardware descriptions with a normalization theorem and soundness proof plus a prototype that reduces to verilog; a tool called Cookie that enumerates slight design variants and finds reproducible completeness holes in multiple FPGA compilers; a study of equality saturation drivability variants showing different initialization choices change derivability and performance; Mic that auto-generates QuickCheck tests for OCaml module signatures; sketch-guided FPGA synthesis work; ZX-diagram visualization in Coq.
AI-written summary · about
chapters (8)
- 0:00Welcome to competition
- 1:05Hardware description semantics
- 6:02Hardware compiler completeness
- 10:42Rule set quality saturation
- 16:11Differential testing for OCaml
- 21:53Synthesis for FPGA compilation
- 27:20Visualizing Coq proofs
- 31:31Poster session & Q&A
related talks
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
11mDemo: More Than Point Tools: RISC-V Solutions
53mSemantics-based program manipulation in the age of LLMs
56mProof Assistants At the Hardware-Software Interface
16mThe Morello ISA semantics, proof, and test generation
31mFormal Specification
18mThe Essence of Verilog: A Tractable and Tested Operational Semantics for Verilo...
11mLightning Talks