CS-550: Formal verification

Résumé

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

Source officielle

https://edu.epfl.ch/coursebook/fr/formal-verification-CS-550

Page Moodle

http://go.epfl.ch/CS-550

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Enseignant

Séances de ce cours (86)

Concepts associés (645)

Cours associés (158)

MOOCs associés (58)

Analysis

Analysis (: analyses) is the process of breaking a complex topic or substance into smaller parts in order to gain a better understanding of it. The technique has been applied in the study of mathematics and logic since before Aristotle (384–322 B.C.), though analysis as a formal concept is a relatively recent development. The word comes from the Ancient Greek ἀνάλυσις (analysis, "a breaking-up" or "an untying;" from ana- "up, throughout" and lysis "a loosening"). From it also comes the word's plural, analyses.

Théorie

Une théorie (du grec theoria, « contempler, observer, examiner ») est un ensemble cohérent, si elle prétend à la scientificité, d'explications, de notions ou d'idées sur un sujet précis, pouvant inclure des lois et des hypothèses, induites par l'accumulation de faits provenant de l'observation, l'expérimentation ou, dans le cas des mathématiques, déduites d'une base axiomatique donnée : théorie des matrices, des torseurs, des probabilités.

Predicate abstraction

In logic, predicate abstraction is the result of creating a predicate from a sentence. If Q is any formula then the predicate abstract formed from that sentence is (λy.Q), where λ is an abstraction operator and in which every occurrence of y occurs bound by λ in (λy.Q). The resultant predicate (λx.Q(x)) is a monadic predicate capable of taking a term t as argument as in (λx.Q(x))(t), which says that the object denoted by 't' has the property of being such that Q. The states ( λx.

Software reliability testing

Software reliability testing is a field of software-testing that relates to testing a software's ability to function, given environmental conditions, for a particular amount of time. Software reliability testing helps discover many problems in the software design and functionality. Software reliability is the probability that software will work properly in a specified environment and for a given amount of time. Using the following formula, the probability of failure is calculated by testing a sample of all available input states.

Verification condition generator

A verification condition generator is a common sub-component of an automated program verifier that synthesizes formal verification conditions by analyzing a program's source code using a method based upon Hoare logic. VC generators may require that the source code contains logical annotations provided by the programmer or the compiler such as pre/post-conditions and loop invariants (a form of proof-carrying code). VC generators are often coupled with SMT solvers in the backend of a program verifier.