Publication

Verifying and Synthesizing Software with Recursive Functions

Viktor Kuncak
2014
Conference Papers

Résumé

Our goal is to help people construct software that does what they wish. We develop tools and algorithms that span static and dynamic verification, constraint solving, and program synthesis. I will outline the current state our verification and synthesis system, Leon, which translates software into a functional language and uses SMT solvers to reason about paths in programs and specifications. Certain completeness results partly explain the effectiveness of verification and synthesis procedures implemented within Leon, in particular results on decidability of sufficiently surjective abstraction functions, and the framework of complete functional synthesis.

Source officielle

https://infoscience.epfl.ch/entities/publication/f28e4765-5a38-4df4-97c8-c75b0047987b

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

Viktor Kuncak
2014
Conference Papers

Résumé

Source officielle

https://infoscience.epfl.ch/entities/publication/f28e4765-5a38-4df4-97c8-c75b0047987b

À propos de ce résultat

Concepts associés (29)

Synthèse vocale

La synthèse vocale est une technique informatique de synthèse sonore qui permet de créer de la parole artificielle à partir de n'importe quel texte. Pour obtenir ce résultat, elle s'appuie à la fois sur des techniques de traitement linguistique, notamment pour transformer le texte orthographique en une version phonétique prononçable sans ambiguïté, et sur des techniques de traitement du signal pour transformer cette version phonétique en son numérisé écoutable sur un haut parleur.

High-level synthesis

High-level synthesis (HLS), sometimes referred to as C synthesis, electronic system-level (ESL) synthesis, algorithmic synthesis, or behavioral synthesis, is an automated design process that takes an abstract behavioral specification of a digital system and finds a register-transfer level structure that realizes the given behavior. Synthesis begins with a high-level specification of the problem, where behavior is generally decoupled from low-level circuit mechanics such as clock-level timing.

Synthèse logique

En électronique, la synthèse logique (RTL synthesis) est la traduction d'une forme abstraite de description du comportement d'un circuit (voir Register Transfer Level) en sa réalisation concrète sous forme de portes logiques. Le point de départ peut être un langage de description de matériel comme VHDL ou Verilog, un schéma logique du circuit. D'autres sources sont venues s'additionner depuis les années 2010, comme l'utilisation de la programmation en OpenCL. Le point d'arrivée peut être un code objet pour un CPLD ou FPGA ou la création d'un ASIC.

Afficher plus

Publications associées (28)

Scalable constrained optimization

Maria-Luiza Vladarean

Modern optimization is tasked with handling applications of increasingly large scale, chiefly due to the massive amounts of widely available data and the ever-growing reach of Machine Learning. Consequently, this area of research is under steady pressure t ...

EPFL2024

Scalable Logic Rewriting Using Don’t Cares

Giovanni De Micheli, Alessandro Tempia Calvino

Logic rewriting is a powerful optimization technique that replaces small sections of a Boolean network with better implementations. Typically, exact synthesis is used to compute optimum replacement on-the-fly, with possible support for Boolean don't cares. ...

2024

Learning to Remove Cuts in Integer Linear Programming

Volkan Cevher, Grigorios Chrysos, Efstratios Panteleimon Skoulakis

Cutting plane methods are a fundamental approach for solving integer linear programs (ILPs). In each iteration of such methods, additional linear constraints (cuts) are introduced to the constraint set with the aim of excluding the previous fractional opti ...

2024

Afficher plus