Hardware & Software Verification

This is the homepage of the above-named module, which is offered to MSc and 4th-year MEng students at Imperial College London.

• The module is run by Dr John Wickerson.

• Worksheets are available for Dafny, Isabelle, and SymbiYosys.

• The module is assessed by a series of three practical tests in the last three Mondays of Autumn term 2026. These tests will be run on department computers, and taken individually.

• In previous years, the module was assessed by take-home coursework. All of those coursework exercises are available below, with full solutions.

Summary of past coursework questions

Click on the links below to access the coursework questions (with model answers) from previous years.

• Dafny 2019: bubble sort; selection sort; insertion sort; shellsort; Johnsort.

• Isabelle 2019: irrationality of 2*sqrt(2); L-numbers; pyramidal numbers; opt-NOT is effective; opt-NOT is idempotent; opt-DM is sound; opt-DM and opt-NOT never increase area; opt-DM and opt-NOT never increase delay; constant folding; circuits with fan-out.

• Dafny 2020: zeroing an array; backwards selection sort; recursive selection sort; early-termination bubble sort; cocktail-shaker sort.

• Isabelle 2020: irrationality of 3/sqrt(2); centred pentagonal numbers; Lucas numbers; balanced circuits; NAND gates.

• Dafny 2021: array of multiples of two; exchange sort; Fung sort; odd/even sort; bubble sort with triples.

• Isabelle 2021: factorising circuits; divisibility of powers; binary coded decimal.

• Dafny 2022: counting squares in a grid; binary search; quicksort.

• Isabelle 2022: full adders; fifth powers; opt-ident is sound and never increases area; opt-redundancy is sound and never increases area.

• Dafny 2023: integer square roots; analogue-to-digital conversion; stupidsort.

• Isabelle 2023: introducing and eliminating XOR gates; lists of clones; analogue-to-digital conversion; Fermat's Last Theorem.

• SymbiYosys 2023: binary-to-BCD conversion; verifying a circular queue.

• Dafny 2024: verifying SAT solvers.

• Isabelle 2024: introducing and eliminating NAND gates; conversions between numbers and lists of digits; verifying SAT solvers.

• SymbiYosys 2024: verifying a multiplier.

• Isabelle 2025: estimating computational complexity of opt-NOT and factorise; proving that even-length palindromes are divisible by 11; reducing SAT queries to 3SAT form.

• Dafny 2025: doublesort.

• SymbiYosys 2025: verifying a divider.