6.0/4.0 VU Formal Methods in Computer Science (185.291)

This page provides some additional information on the course as held until summer 2018. For current information, see the course pages in TISS and TUWEL

Slides for the part on "Deductive Verification of Software"

  1. Intro, Syntax of toy language, Operational semantics
  2. Operational semantics contd., correctness assertions
  3. Ways to prove correctness assertions, assignments, sequential composition
  4. Annotation calculus, conditionals, abort, examples
  5. Loops

If you teach a similar subject and are interested in the LaTeX sources of the slides, send me an email, salzer@logic.at.

Previous exams

2018: 26.1. 16.3. 4.5.
2017: 27.1. 17.3. 5.5. 30.6. 20.10. 12.12.
2016: 29.1. 18.3. 6.5. 1.7. 21.10. 9.12.
2015: 30.1. 27.3. 8.5. 3.7. 16.10. 4.12.
2014: 31.1. 28.3. 9.5. 4.7. 17.10. 5.12.
2013: 1.2. 22.3. 3.5. 28.6. 18.10. 6.12.
2012: 3.2. 23.3. 4.5. 29.6. 19.10. 7.12.
2011: 28.1. 25.3. 6.5. 1.7. 28.10. 9.12.

salzer@logic.at