Concept

Théorème de complétude de Gödel

Publications associées (33)

Orthologic with Axioms

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having po ...

2024

The completeness of the generalized eigenfunctions and an upper bound for the counting function of the transmission eigenvalue problem for Maxwell equations

Hoài-Minh Nguyên, Jean Louis-Alexandre Fornerod

Cakoni and Nguyen recently proposed very general conditions on the coefficients of Maxwell equations for which they established the discreten ess of the set of eigenvalues of the transmission problem and studied their locations. In this paper, we establish ...

2021

Verified Functional Programming

Nicolas Charles Yves Voirol

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

EPFL2019

Real-Time State Estimation and Voltage Stability Assessment of Power Grids: From Theoretical Foundations to Practical Applications

Andreas Martin Kettner

The operators of power distribution systems strive to lower their operational costs and improve the quality of the power service provided to their customers. Furthermore, they are faced with the challenge of accommodating large numbers of Distributed Energ ...

EPFL2019

Foundations of Implicit Function Types

Martin Odersky, Fengyun Liu, Olivier Eric Paul Blanvillain

Implicit parameters are used pervasively in Scala and are also present in a number of other programming and theorem proving languages. This paper describes a generalization of implicit parameters as they are currently found in Scala to implicit function ty ...

2017

Multi-level Logic Benchmarks: An Exactness Study

Giovanni De Micheli, Mathias Soeken, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù, Eleonora Testa, Winston Jason Haaswijk

In this paper, we study exact multi-level logic benchmarks. We refer to an exact logic benchmark, or exact benchmark in short, as the optimal implementation of a given Boolean function, in terms of minimum number of logic levels and/or nodes. Exact benchma ...

Ieee2017

On Satisfiability for Quantified Formulas in Instantiation-Based Procedures

Viktor Kuncak, Nicolas Charles Yves Voirol

Procedures for first-order logic with equality are used in many modern theorem provers and solvers, yet procedure termination in case of interesting sub-classes of satisfiable formulas remains a challenging problem. We present an instantiation-based semi-d ...

2016

Sound Proof of Proximity of Knowledge

Serge Vaudenay

Public-key distance bounding schemes are needed to defeat relay attacks in payment systems. So far, only five such schemes exist, but fail to fully protect against malicious provers. In this paper, we solve this problem. We provide a full formalism to defi ...

2015

A Surface Potential and Current Model for Polarity-Controllable Silicon Nanowire FETs

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Jian Zhang

Silicon nanowire FET (SiNWFET) with dynamic polarity control has been experimentally demonstrated and has shown large potential in circuit applications. To fully explore its circuit-level opportunities, a physics-based compact model of the polarity-control ...

2015

An overview of the Leon verification system: verification by translation to recursive functions

Viktor Kuncak, Etienne Kneuss, Régis William Blanc, Philippe Paul Henri Suter

We present the Leon verification system for a subset of the Scala programming language. Along with several functional features of Scala, Leon supports imperative constructs such as mutations and loops, using a translation into recursive functional form. Bo ...

2013

Graph Chatbot

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.

Connectez-vous pour utiliser Chat avec Graph Search