Publication

Formal Verification of Rust with Stainless

Publications associées (54)

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

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

A zero-copy key-value store in Rust

Ogier Quentin Bouvier

To provide a key-value store with consistent latency independent from keys and values sizes we need to eliminate copies from the key-value store's datapath while still ensuring reliable delivery of responses to requests. We leverage several feature of the ...

2019

Verifying Software Network Functions with No Verification Expertise

George Candea, 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

Cross-Platform Language Design

Sébastien Jean R Doeraene

Programming languages are increasingly compiled to multiple runtimes, each featuring their own rich structures such as their object model. Furthermore, they need to interact with other languages targeting said runtimes. A language targeting only one runtim ...

EPFL2018

LMS-Verify: Abstraction without Regret for Verified Systems Programming’

Tiark Rompf, Nada Amin

Performance critical software is almost always developed in C, as programmers do not trust high-level languages to deliver the same reliable performance. This is bad because low-level code in unsafe languages attracts security vulnerabilities and because d ...

Assoc Computing Machinery2017

Extending Safe C Support In Leon

Marco Adriano Antognini

As hardware designs get more robust and efficient, software can solve a wider range of challenges, each one more advanced than the previous one. The direct consequence is that software complexity grows continuously. Despite being used more frequently in de ...

2017

Unification of Compile-Time and Runtime Metaprogramming in Scala

Eugene Burmako

Metaprogramming is a technique that consists in writing programs that treat other programs as data. This paradigm of software development contributes to a multitude of approaches that improve programmer productivity, including code generation, program anal ...

EPFL2017

metaSMT: focus on your application and not on solver integration

Mathias Soeken, Heinz Riener

Many applications from artificial intelligence and formal methods use decision procedures as their core solving engines. In this context, automated reasoning based on Satisfiability (SAT) or Satisfiability Modulo Theories (SMT) is very effective. For a giv ...

Springer Verlag2017

Miniphases: Compilation using Modular and Efficient Tree Transformations

Martin Odersky, Dmytro Petrashko, Ondrej Lhoták

Production compilers commonly perform dozens of transformations on an intermediate representation. Running those transformations in separate passes harms performance. One approach to recover performance is to combine transformations by hand in order to red ...

Assoc Computing Machinery2017

Decrypting Local Type Inference

Hubert Plociniczak

Statically typed languages verify programs at compile-time. As a result many programming mistakes are detected at an early stage of development. A programmer does not have to specify types for every single term manually, however. Many programming languages ...

EPFL2016