Synthèse de programmes | EPFL Graph Search

Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?

Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.

Découvrez-en plus sur les applications Graph.

En informatique, la synthèse de programmes consiste à construire automatiquement un programme à partir d'une spécification. La spécification est décrite dans un langage logique, par exemple en logique temporelle linéaire. La synthèse de programmes s'appuie sur des techniques de vérification formelle de programmes. Le problème de synthèse de programmes remonte aux travaux d'Alonzo Church. Manna et Waldinger ont proposé une méthode déductive pour synthétiser un programme à partir d'une spécification en logique du premier ordre. vignette|Un robot, comme l'Atlas, peut exécuter un programme synthétisé afin de réaliser une tâche et pouvoir réagir à toutes les éventualités de l'environnement. Le programme de synthèse de programmes consiste à générer un plan pour un agent (par exemple un robot) qui réussit face à toutes les éventualités de l'environnement. Par exemple, la synthèse de programme réactif avec une spécification en logique temporelle linéaire a été appliqué en robotique. En 2015, à la compétition DARPA Robotics en 2015, la synthèse de programmes a été implémentée dans un robot Atlas. Plusieurs méthodes ont été proposés, par Büchi et Landweber et par Rabin. Le problème de synthèse se réduit à tester si le langage d'un automate d'arbre est vide et de voir la solution comme un jeu à deux joueurs. Dans ces travaux préliminaires, la spécification du système était donné par une formule de S1S (logique monadique du second ordre avec un successeur). Le problème de synthèse et réalisabilité en logique temporelle linéaire (LTL) a été introduit par Pnueli et Rosner et indépendamment par Abadi, Lamport et Wolper, en 1989. Les travaux de Pnueli et Rosner font suite aux travaux préliminaires de Clarke et Emerson et ceux de Manna et Wolper, qui réduisent le problème de synthèse à un problème de satisfiabilité, en ignorant le fait que l'environnement doit être considéré comme un adversaire.

À 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 (1)

Personnes associées (2)

Concepts associés (4)

Cours associés (2)

Séances de cours associées (3)

MOOCs associés (2)

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.

Synthèse de programmes

Problème SAT

vignette|Une instance du Sudoku peut être transformée en une formule de logique propositionnelle à satisfaire. Une assignation des variables propositionnelles donne une grille complétée. En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le problème de décision, qui, étant donné une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie. Ce problème est important en théorie de la complexité.

Parallel programming

With every smartphone and computer now boasting multiple processors, the use of functional ideas to facilitate parallel programming is becoming increasingly widespread. In this course, you'll learn th

Parallel programming

Vérification formelle et synthèse des programmes

Explore les recherches de Viktor Kuncak sur la vérification formelle, la synthèse de programmes et les activités d'enseignement à l'EPFL.

Vérification formelle et synthèse des programmes

Par l’instructeur Viktor Kuncak explore les activités de vérification formelle, de synthèse de programme et d’enseignement à l’EPFL.

Programmation assistée par solvant pour tous

Couvre la programmation assistée par solveur, intégrant les résolveurs SMT pour la vérification, la synthèse et le débogage des programmes, ainsi que les défis dans la construction d'outils assistés par solveur.

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent

EPFL2019

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 u