|
|
 |
Course on Program Correctness, Spring 2010
Marcello Bonsangue
Earliest computer programs were written largely to solve mathematical
problems. In this case a program can be thought of as implicitly
asserting a theorem to the effect that if certain input conditions are
met then the program will solve the specific problem. Making that
theorem true is not merely a matter of being an expert programmer, it
can be aided by a logical analysis of what a program is supposed to
do.
As programming has concentrated more on the mechanics of interacting
with computer's environment (e.g. for reactive systems and Internet
applications) rather than on mathematical problems, the advantage of a
logical analysis has become obvious. It is particularly difficult to
foresee the effects of abnormal events on the behavior of
communicating applications that may lead to inconvenient or even
catastrophic situations.
A body of theory has emerged in the past two decades to make
(automatic) analysis of programs a practical reality. In this course
we will cover both classical and state-of-the-art core techniques in
proving the correctness of imperative and concurrent programs.
Students will be evaluated on the basis of home assignments and a
final written examination. The latter will take place in room t.b.a on
Tuesday June 8th, 2009, from 14:00 to 17:00 o' clock.
The second-chance examination will be in room t.b.a on
Tuesday August 24th, 2009, from 14:00 to 17:00 o'clock.
| Theory class: |
Room WI 403, from 11:15 to 13:00 |
| Practice class: |
Room WI 403, from 13:45 to 15:30 |
|
|
| Class schedule: |
February 5, 12, 19, 26
March 5, 19, 26
April 9, 16,
May 7 21
|
|
|
| Intended Group: |
2nd year Computer Science |
|
|
| Prerequisites: |
Students should have taken the course Logica. |
|
|
| Studypoints: |
5 ECTS |
|
|
| Literature: |
Michael R. A. Huth and Mark D. Ryan
Logic in Computer Science: Modelling and Reasoning about Systems
Cambridge University Press, 2004 (ISBN 052154310X)
|
|
|
| Remark: |
The course is taught in English |
|
|
| Lectures: |
|
|
|
| Bibliography: |
[HR04] Michael R. A. Huth and Mark D. Ryan.
Logic in Computer Science: Modelling and Reasoning about Systems.
Cambridge University Press, 2004.
[Var96] Moshe Y. Vardi. An
automata-theoretic approach to linear temporal logic In Proceedings of the VIII Banff
Higher order workshop conference on Logics for concurrency : structure versus automata, Springer-Verlag,
1996.
[Win93] G. Winskel. The Formal Semantics of
Programming Languages, An Introduction. The MIT Press, 1993.
|
|
|
|
