As long as requirements to computer designs are formulated in an ambiguous human language and as long as these designs are implemented by humans not insured against possible carelessness and misunderstandings, computer systems will contain errors. For the time being, the only way to guarantee the absence of errors in a computer system is to exploit rigorous formal methods of mathematics for specifying a system's intended behavior and proving that the actual system's implementation meets the desired specification.

In the seminar, we will consider articles describing how logic and mathematics could be applied for precise specification and subsequent verification of selected computer systems, e.g., processors, compilers, and microkernels.

Why participate in this seminar?

  • learn about research developments in formal specification and verification
  • block seminar on 1-2 days
  • scientific talks and discussions
  • supervision and feedback
Join the seminar: register via TUCaN, the seminar will start with a mandatory online kick-off meeting on
Thursday, 15.4.2021, at 15:15

Course website: https://www.mais.informatik.tu-darmstadt.de/formspec-ss21.html