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.

• All coursework is to be done in pairs. Please use this spreadsheet from October 2025 to support this. The spreadsheet contains two sheets. The first sheet contains students who have already paired up. The second sheet contains students who are still looking for a pair. Please enter yourself initially onto the second sheet, and then once you have found a pair, please move yourselves over to the first sheet.

• All coursework is due at 15:00 on Friday 12 December 2025 (the last day of Autumn term).

• The Isabelle coursework for 2025 is now available.

• The Dafny coursework for 2025 is now available.

• The SymbiYosys coursework for 2025 is now available.

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.