Elements of mathematics and logic for computer program analysis

Frédéric Blanqui (1)

1 FORMES - Formal Methods for Embedded Systems

In order to be able to rigorously prove the correctness of a program, one must have a formal definition of: what is a program, syntactically; how it is evaluated, that is, what is its semantics; how to formulate the properties we are interested in; and how to prove them. All this requires to understand some basic mathematical notions like induction, terms, formulas, deduction, etc. These notes are intended to give an introduction to some of these notions.

Domaines: Informatique [cs]; Mathématiques [math]

Frédéric Blanqui. Elements of mathematics and logic for computer program analysis. Master. Institute of Applied Mechanics and Informatics (IAMA) of the Vietnamese Academy of Sciences and Technology (VAST) at Ho Chi Minh City, Vietnam, 2013, pp.37. ⟨cel-00934160⟩