Publication

On Correctness of Dynamic Protocol Update

Publications associées (28)

IGCT Based Solid State Resonant Conversion

Driven by the environmental changes, penetration of renewables and the need for more flexible power grid, DC is reemerging as a basis for future power networks. Already established in the area of HVDC for very long distance transmission, more and more atte ...

EPFL2020

Morphology and morphodynamics of braided rivers: an experimental investigation

Daniel Vito Papa

Braided rivers form some of the most fascinating fluvial patterns found on Earth. They are identifiable by their unique morphology of complex networks of intertwined channels that spread across wide floodplains. Detailed knowledge of their dynamics is need ...

EPFL2020

Stoic: Towards Disciplined Capabilities

Martin Odersky, Sandro Stucki, Nada Amin, Fengyun Liu, Paolo Giosuè Giarrusso

Capabilities are widely used in the design of software systems to ensure security. A system of capabilities can become a mess in the presence of objects and functions: objects may leak capabilities and functions may capture capabilities. They make reasonin ...

2020

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 need for improved supporting tools that verify the soft ...

EPFL2019

Reliable and Robust Cyber-Physical Systems for Real-Time Control of Electric Grids

Wajeb Saab

Real-time control of electric grids is a novel approach to handling the increasing penetration of distributed and volatile energy generation brought about by renewables. Such control occurs in cyber-physical systems (CPSs), in which software agents maintai ...

EPFL2019

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

Verifying Software Network Functions with No Verification Expertise

George Candea, Aikaterini Argyraki, Solal Vincenzo Pirelli, Rishabh Ramesh Iyer, Luis David Figueiredo Mascarenhas Moreira Pedrosa, Matteo Rizzo

We present the design and implementation of Vigor, a software stack and toolchain for building and running software network middleboxes that are guaranteed to be correct, while preserving competitive performance and developer productivity. Developers write ...

ACM2019

A Programming Model and Foundation for Lineage-Based Distributed Computation

Philipp Haller, Heather Christine Klug

The most successful systems for "big data'' processing have all adopted functional APIs. We present a new programming model we call function passing designed to provide a more principled substrate, or middleware, upon which to build data-centric distribute ...

Cambridge University Press2018