Concept

Correction (logique)

Publications associées (11)

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based pro ...

Springer International Publishing Ag2024

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

Sound reasoning about integral data types with a reusable SMT solver interface

Viktor Kuncak, Régis William Blanc

We extend the Leon verification system for Scala with support for bit-vector reasoning, thus addressing one of its fundamental soundness limitation with respect to the treatment of integers primitives. We leverage significant progresses recently achieved i ...

ACM Press2015

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

Cryptographic Hash Functions in Groups and Provable Properties

Juraj Sarinay

We consider several "provably secure" hash functions that compute simple sums in a well chosen group (G,*). Security properties of such functions provably translate in a natural way to computational problems in G that are simple to define and possibly also ...

EPFL2011

Capabilities for Uniqueness and Borrowing

Martin Odersky, Philipp Haller

An important application of unique object references is safe and efficient message passing in concurrent object-oriented programming. However, to prevent the ill effects of aliasing, practical systems often severely restrict the shape of messages passed by ...

Springer2010

A Class Of Mean Field Interaction Models for Computer and Communication Systems

Jean-Yves Le Boudec

We consider models of N interacting objects, where the interaction is via a common resource and the distribution of states of all objects. We introduce the key scaling concept of intensity; informally, the expected number of transitions per object per time ...

2008

Robust Distributed Coverage using a Swarm of Miniature Robots

Alcherio Martinoli, Nicolaus Correll

For the multi-robot coverage problem deterministic deliberative as well as probabilistic approaches have been proposed. Whereas deterministic approaches usually provide provable completeness and promise good performance under perfect conditions, probabilis ...

2007

Distributed Coverage: From Deterministic to Probabilistic Models

Alcherio Martinoli, Nicolaus Correll

For the multi-robot coverage problem determin- istic deliberative as well as probabilistic approaches have been proposed. Whereas deterministic approaches usually provide provable completeness and promise good performance under perfect conditions, probabil ...

2007