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.
*Method: * hoorcollege + werkcollege
Examination: schriftelijk
Objective: The goal is to cover both classical and state-of-the-art core techniques in proving the correctness of systems and imperative programs.
Prior knowledge: Inleiding Informatica, Logica voor Informatici
Literature: Michael R. A. Huth and Mark D. Ryan. “Logic in Computer Science: Modelling and Reasoning about Systems”, Cambridge University Press, 1999 (ISBN 0521656028).
*Website: * http://www.liacs.nl/~marcello/penc.html
Remarks: Het college wordt in het Engels gegeven.