Skip to Main content Skip to Navigation

Elements of mathematics and logic for computer program analysis

Frédéric Blanqui 1 
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : 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.
Document type :
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Tuesday, January 21, 2014 - 4:08:04 PM
Last modification on : Thursday, February 3, 2022 - 11:17:00 AM
Long-term archiving on: : Tuesday, April 22, 2014 - 1:20:22 PM


  • HAL Id : cel-00934160, version 1



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⟩



Record views


Files downloads