Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs

Po-Chun Chien, Nian-Ze Lee, Armin Biere +1

Formal verification of software programs and hardware designs shares the common goal of reasoning about state-transition systems, yet the two communities have largely developed sep…