Formal Methods and Specifications

Přednášející:

Stefan Ratschan (gar.)

Cvičící:

Stefan Ratschan (gar.)

Předmět zajišťuje:

katedra softwarového inženýrství

Anotace:

Students are able to describe semantics of software formally and to use sound reasoning for construction of correct software. They learn to use some software tools that allow to prove basic properties of software.

Požadavky:

Knowledge of basic notions of mathematical logic and set theory and ability to use them.

Osnova přednášek:

1. Predicate logic as a specification language.

2. Proof techniques for predicate logic.

3. [2] Basic techniques for giving formal semantics to programming language: Operational semantics, denotational semantics, axiomatic semantics.

4. Hoare Logic (HL) and its practical use.

5. HL: Partial vs. total program correctness. Loop invariants.

6. HL: Termination. Correctness of subroutine calls.

7. HL: Formal correctness of object-oriented programs.

8. Formal methods and specifications for reactive systems. Temporal logics.

9. Manual verification of reactive systems.

10. Automatic verification of reactive systems: bounded model checking.

11. Automatic verification of reactive systems: unbounded model checking.

12. Formal methods for embedded systems.

Osnova cvičení:

Cíle studia:

The goal of the module is to provide students with the ability to apply formal reasoning in software development. On one hand, this includes the ability to base their own software development activities on sound reasoning, even within an environment that does not systematically employ formal methods. On the other hand, this includes the ability to understand and use automated techniques and tools for supporting formal methods within the software development process.

Studijní materiály:

1. Aaron R. Bradley and Zohar Manna: ''The Calculus of Computation'', Springer Verlag, 2007

2. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled: ''Model Checking'', MIT Press, 1999

3. Zohar Manna and Amir Pnueli: ''Temporal Verification of Reactive Systems'', Springer Verlag, 1995

4. Glynn Winskel: ''Formal Semantics of Programming Languages'', MIT Press, Cambridge, Massachusetts, 1993

Poznámka:

Rozsah=prednasky+proseminare+cviceni2p+1c, Prednasejici: Dipl.-Ing. Dr. techn. Stefan Ratschan

Rozvrh na zimní semestr 2011/2012:

Rozvrh není připraven

Rozvrh na letní semestr 2011/2012:

Rozvrh není připraven

Předmět je součástí následujících studijních plánů:

• Software Engineering, Presented in English, Version for Students, who Enrolled in 2010 and 2011 (povinný předmět zaměření)
• Master Informatics, Presented in English - Version for Students who Enrolled in 2010 (VO)
• Master Informatics, Presented in English - Version for Students who Enrolled in 2011 (VO)
• Master Informatics, Presented in English - Version for Students who Enrolled in 2012 (VO)
• Software Engineering, Presented in English - Version for Students who Enrolled in 2012 (povinný předmět zaměření)