Abstract
Verifying that computer systems behave as expected is a complex task. Experience shows that these systems generally contain errors that are more or less critical for the user and more or less difficult for the designer to correct. A great deal of work has gone into proposing specialized formalisms for modeling the system and the desired behavior, as well as methods and algorithms for actually proving its adequacy.
A number of questions then arise concerning the correctness of the proposed methods: have we actually modeled the right program and the right behavior? Are the method and its implementation correct? Are they powerful enough? These are not just theoretical questions, as they are of direct concern to the manufacturers who develop critical computer codes, and who must guarantee their correct behavior by providing sufficient justification to the certification body.
Ultimately, our conviction that a method is correct is based on an interpretation of the problem in mathematical terms and logical reasoning. However, the intrinsic complexity of mathematical program models means that they need to be processed by computer.
Since the 1970s, a class of tools has developed alongside those specifically designed for program analysis, dealing with general mathematical theories. Theory description languages and proof formalisms vary from system to system.
During the seminar, we will present and motivate several possible approaches (from first-order logic to type theory). Using the example of the Coq proof assistant, we will illustrate the state of the art of what can currently be achieved in terms of formalized mathematics on computers.
