Concept

Lean (assistant de preuve)

Publications associées (8)

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

2023

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

A proof of a sumset conjecture of Erdős

Florian Karl Richter

In this paper we show that every set A ⊂ ℕ with positive density contains B + C for some pair B, C of infinite subsets of ℕ , settling a conjecture of Erdős. The proof features two different decompositions of an arbitrary bounded sequence into a structured ...

2019

A Formally Verified NAT

George Candea, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh, Luis David Figueiredo Mascarenhas Moreira Pedrosa

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

Assoc Computing Machinery2017

Architecture Internalisation in BIP

Joseph Sifakis, Simon Bliudze

We consider two approaches for building component-based systems, which we call respectively architecture-based and architecture-agnostic. The former consists in describing coordination constraints in a purely declarative manner through parameterizable glue ...

ACM2014

Architecture Internalisation in BIP

Joseph Sifakis, Simon Bliudze

Architectures allow shifting the focus of developers from low-level code to high-level structures ensuring coordination in component-based systems. If the architecture description language is expressive enough, it is possible to describe architectures in a ...

2014

On Decision Procedures for Algebraic Data Types with Abstractions

Viktor Kuncak, Philippe Paul Henri Suter, Mirco Dotta

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

2009

On the flux phase conjecture at half filling: an improved proof

Nicolas Macris

We present a simplification of Lieb's proof of the flux phase conjecture for interacting fermion systems--such as the Hubbard model--at half-filling on a general class of graphs. The main ingredient is a procedure which transforms a class of fermionic Hami ...

1996

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