Computer Aided Verification
Bachelor
Computer aided verification is an emerging technology to use computers to verify the correctness of programs. The field has produced many powerful tools. Do some experiment with them, or join us developing new verification tools.
Project examples:
- Experimenting with tool X (e.g. Isabelle, COQ, PVS) for benchmarking.
- Building verification plug-ins (e.g. DNF normalizer, wp calculator).
- Experimenting with self-validating programs.
- Building a logic trainer for students.
- Java front-end for verification tools.