Verification of Generic VHDL Designs and Their Translation to Rocq
Abstract elided by the publisher.
Related papers
- Hardware software co-design in Haskell Haskell 2017
- Verification of timing Properties of VHDL CAV 1993
- The Rocq-NN-Roll Prover: Soundly Verifying Hyperproperties of Neural Networks in Rocq CAV 2026
- Formal Verification of Hardware Synthesis CAV 2013
- A Refinement Calculus for the Synthesis of Verified Hardware Descriptions in VHDL TOPLAS 1997
- Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic POPL 2026
- Formal verification of translation validators: a case study on instruction scheduling optimizations POPL 2008
- Checking Safety Properties of Behavioral VHDL Descriptions by Abstract Interpretation SAS 2002