- Daniel Kroening
- SMT Lists/Sets/Maps
- Google groups:
Formal Techniques for
Hardware/Software Co-Verification
Materials
- Slides (PDF)
- demo1.zip – binary search
- demo2.zip – RTL vs C
- demo3.zip – k-induction
- demo4.zip – State Charts
Related Papers
- Verification of SpecC using Predicate Abstraction
- Formal Verification of SystemC by Automatic Hardware/Software Partitioning
- Checking Consistency of C and Verilog using Predicate Abstraction and Induction
- Hardware Verification using ANSI-C Programs as a Reference
- Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking