Skip to Main content Skip to Navigation
Lectures

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 :
Lectures
Complete list of metadatas

Cited literature [2 references]  Display  Hide  Download

https://cel.archives-ouvertes.fr/cel-00934160
Contributor : Frédéric Blanqui <>
Submitted on : Tuesday, January 21, 2014 - 4:08:04 PM
Last modification on : Tuesday, March 17, 2020 - 1:34:46 AM
Long-term archiving on: : Tuesday, April 22, 2014 - 1:20:22 PM

Identifiers

  • HAL Id : cel-00934160, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

1020

Files downloads

1113