Séance de cours

Introduction à la vérification formelle

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Description

Cette séance de cours présente les principes et la pratique de la vérification formelle, en mettant l'accent sur la construction de logiciels vérifiés à l'aide d'outils et la compréhension des principes sous-jacents. Le cours met l'accent sur la preuve rigoureuse que les systèmes informatiques satisfont aux spécifications, en contrastant la vérification formelle avec les tests. Il couvre des sujets tels que la démonstration automatique des théorèmes, la compilation de programmes en formules et limportance des modèles mathématiques pour assurer lexactitude du système.

Source officielle

Concepts associés (32)

Software verification and validation

In software project management, software testing, and software engineering, verification and validation (V&V) is the process of checking that a software system meets specifications and requirements so that it fulfills its intended purpose. It may also be referred to as software quality control. It is normally the responsibility of software testers as part of the software development lifecycle.

Méthode formelle (informatique)

En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur un programme informatique ou du matériel électronique numérique, afin de démontrer leur validité par rapport à une certaine spécification. Elles reposent sur les sémantiques des programmes, c'est-à-dire sur des descriptions mathématiques formelles du sens d'un programme donné par son code source (ou, parfois, son code objet).

Vérification formelle

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Test (informatique)

vignette|Une programmeuse écrivant du code Java avec JUnit. En informatique, un test désigne une procédure de vérification partielle d'un système. Son objectif principal est d'identifier un nombre maximal de comportements problématiques du logiciel. Il permet ainsi, dès lors que les problèmes identifiés seront corrigés, d'en augmenter la qualité. D'une manière plus générale, le test désigne toutes les activités qui consistent à rechercher des informations quant à la qualité du système afin de permettre la prise de décisions.

Software verification

Software verification is a discipline of software engineering, programming languages, and theory of computation whose goal is to assure that software satisfies the expected requirements. A broad definition of verification makes it related to software testing. In that case, there are two fundamental approaches to verification: Dynamic verification, also known as experimentation, dynamic testing or, simply testing. - This is good for finding faults (software bugs).

Afficher plus

Séances de cours associées (39)

Correspondance logicielle: Test et vérification

Explore l'exactitude des logiciels grâce à des tests, à la vérification, au flou de propriété et au contrôle dynamique du flux d'information.

Groupes fondamentaux

Explore les groupes fondamentaux, les classes d'homotopie et les revêtements dans les variétés connectées.

Test basé sur la propriété: QuickChick

Explore les tests basés sur des propriétés en utilisant QuickChick, en mettant l'accent sur l'exactitude des logiciels, les spécifications et le contrôle dynamique du flux d'information.

Propositions inductives : comprendre l’évaluation dans Coq

Couvre les propositions inductives en Coq, en se concentrant sur les règles dévaluation pour les expressions arithmétiques et leurs applications dans la définition des fonctions partielles et non déterministes.

Qu’est-ce que la vérification formelle?

Introduit la vérification formelle et ses avantages par rapport aux méthodes de test traditionnelles, en discutant de la démonstration automatique des théorèmes et en compilant les déclarations d'exactitude dans des conditions de vérification.

Afficher plus

Concepts associés (32)

Software verification and validation

Méthode formelle (informatique)

Vérification formelle

Test (informatique)

Software verification

Afficher plus