Assistant de preuve

Résumé

En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques. Conception Beaucoup de projets ont été lancés pour formaliser les mathématiques, en 1966, Nicolaas de Bruijn lance le projet Automath, suivi par d'autres projets. Les projets les plus avancés sont le projet Mizar en Pologne, le projet -Isabelle en Grande-Bretagne et aux États-Unis et le projet Coq en France. Ces logiciels permettent à un humain de transcrire les étapes d'une démonstration mathématique dans un processus se dénomme formalisation. Grâce à elle, le logiciel peut ensuite vérifier la validité de la démonstration. -. Le but de ces projets est de mettre à la disposition du mathématicien des outils informatiques pour l’aider à élaborer une version formelle du résultat auquel il

Source officielle

https://fr.wikipedia.org/wiki/Assistant_de_preuve

À 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.

Publications associées (6)

Publications associées

Chargement

Personnes associées (1)

Personnes associées

Chargement

Unités associées (1)

Unités associées

Chargement

Concepts associés (23)

Concepts associés

Chargement

Cours associés (6)

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.

This course reviews some failure cases in public-key cryptography. It introduces some cryptanalysis techniques. It also presents fundamentals in cryptography such as interactive proofs. Finally, it presents some techniques to validate the security of cryptographic primitives.

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a program part or a language. Students will learn how to apply these concepts in their reasoning.

Afficher plus

Cours associés

Chargement

Séances de cours associées (12)

Séances de cours associées

Chargement

Translating Scala Programs to Isabelle/HOL, Automated Reasoning

Viktor Kuncak

We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs) stemming from the input program. Isabelle, on the other hand, is an interactive theorem prover used to verify mathematical specifications using its own input language Isabelle/Isar. Users specify (inductive) definitions and write proofs about them manually, albeit with the help of semi-automated tactics. The integration of these two systems allows us to exploit Isabelle’s rich standard library and give greater confidence guarantees in the correctness of analysed programs.

2016

Chargement

On Decision Procedures for Algebraic Data Types with Abstractions

Mirco Dotta, Viktor Kuncak, Philippe Paul Henri Suter

We describe a parameterized decision procedure that extends the decision procedure for functional recursive algebraic data types (trees) with the ability to specify and reason about abstractions of data structures. The abstract values are specified using recursive abstraction functions that map trees into other data types that have decidable theories. Our result yields a decidable logic which can be used to prove that implementations of functional data structures satisfy recursively specified invariants and conform to interfaces given in terms of sets, multisets, or lists, or to increase the automation in proof assistants.

2009

Chargement

, , ,

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of network functions and proves properties specific to network configuration, such as reachability and absence of loops. Our proof applies directly to the C code of a network function, and it demonstrates the absence of implementation bugs. Prior work argued that this is not feasible (i.e., that verifying a real, stateful network function written in C does not scale) but we demonstrate otherwise: NAT is one of the most popular network functions and maintains per-flow state that needs to be properly updated and expired, which is a typical source of verification challenges. We tackle the scalability challenge with a new combination of symbolic execution and proof checking using separation logic; this combination matches well the typical structure of a network function. We then demonstrate that formally proven correctness in this case does not come at the cost of performance. The NAT code, proof toolchain, and proofs are available at https://vignat.github.io/

Assoc Computing Machinery2017

Chargement