Software Engineering
Document Actions

Static Checkers for Java and C# (Seminar)

The ultimate goal of program verification is to prove the correctness of real-world programs at compile time. Static checkers, such as Spec# or ESCJava, have taken us a big step towards this goal and will continue in the future. A static checker takes a program annotated with assertions such as pre- and post-conditions of methods and invariants. It automatically proves that these assertions hold for all program runs and warn about assertions that may possibly be violated. In this seminar we will take a look behind the covers of these checkers. Every student is supposed to choose a paper, which explains one of the aspects of static checkers. You will present this paper in the block seminar at the end of the semester.



Note: This course requires registration.