Inhalt
[ 921SOENFMSK13 ] KV Formal Methods in Software Development
|
|
|
| Es ist eine neuere Version 2024W dieser LV im Curriculum Master's programme Business Informatics 2024W vorhanden. |
|
| (*) Unfortunately this information is not available in english. |
 |
| Workload |
Education level |
Study areas |
Responsible person |
Hours per week |
Coordinating university |
| 4,5 ECTS |
M1 - Master's programme 1. year |
Computer Science |
Wolfgang Schreiner |
3 hpw |
Johannes Kepler University Linz |
|
|
|
| Detailed information |
| Original study plan |
Master's programme Computer Science 2013W |
| Objectives |
Students understand the basic concepts of the formal specification of programs and systems and of the formal reasoning about the correctness of implementations with respect to the specification. They are able to apply software tools that support this process.
|
| Subject |
Role of formal methods in software development, specification and verification of imperative programs (Hoare calculus, Dijkstra's calculus of weakest preconditions and strongest postconditions, relational calculus), specification and verification of Java programs (Java Modeling Language JML), specification and verification of concurrent systems (transition systems, temporal logic); practical application of proving assistants (RISC ProofNavigator), integrated verification environments (RISC ProgramExplorer, KeY), extended static checkers (ESC/Java2), model checkers (Spin).
|
| Criteria for evaluation |
Homework exercises (50%), final written exam (50%).
|
| Methods |
Integrated course that combines the theoretical presentation with the practical demonstration of the application of systems on concrete examples.
|
| Language |
English |
| Study material |
Supporting Literature:
- Apt, Krzysztof et al: Verification of Sequential and Concurrent Programs, 3rd edition, Springer, 2009.
- Beckert, B.; Hähnle, R.; Schmitt, P. H. (Eds.): Verification of Object-Oriented Software: The KeY Approach. Springer, Berlin, 2007.
- Huth, M.; Ryan, M.: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge University Press, Cambridge, 2nd edition, 2004.
- Schumann, J. M.: Automated Theorem Proving in Software Engineering. Springer, Berlin, 2001.
Special literature in the form of original papers.
|
| Changing subject? |
No |
| Corresponding lecture |
(*)INMSPKVFMSD: KV Formal Methods in Software Development (4,5 ECTS)
|
|
|
|
| On-site course |
| Maximum number of participants |
- |
| Assignment procedure |
Direct assignment |
|
|
|
