|Formal Methods for Software Development||TDA294/DIT271, LP1, HT2017|
About This Course
The course assistants Mauricio (room 5446, EDIT building), Raúl (room 5447, EDIT building) and Andreas (room 5461, EDIT building) offer scheduled office hours to help you with questions. You can make an appointment with one of them by email. It is not very likely that they are available if you just drop in.
If you have any general questions regarding the course, please post in our google group. This will reach all teachers and your fellow students. This way, there can be an exchange of questions, hints, and discussions among all of us. Please make use of this forum. If you are not yet a member of the group, you have to
All kinds of questions (and answers) on the content of the course are welcome. (But don't post lab solutions!)
ExaminationTo pass the course a student must
Two courses in one
The course is available both for Chalmers and GU students:
The lectures and exercises are held in room EA.
Formal Methods is a generic term for system design, analysis, and implementation methods that are described and used with mathematical rigor. The purpose is to construct, with high confidence, systems that behave according to their specification. The course introduces practically and theoretically the two most important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced using a concrete tool.
On the model checking side, the advantage of an automated method at the same time places restrictions on the kind of properties that can be verified. Accordingly, we concentrate on the verification of safety properties. The lectures cover the following topics:
For the deductive verification side, we use KeY, an integrated tool for the formal specification and verification of Java programs. The tool, which is partly developed at Chalmers and Gothenburg University, supports formal specification in the Java Modeling Language (JML), and translation from JML into logic. An interactive theorem prover is used to formally verify statements about specifications and programs. The lectures cover the following topics:
|Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools||W. Ahrendt, Aug 28, 2017|