Publication

Scaling Language Features for Program Verification

Related publications (134)

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Trust as a Programming Primitive

Adrien Ghosn

Programming has changed; programming languages have not.Modern software embraced reusable software components, i.e., public libraries, and runs in the cloud, on machines that co-locate applications from various origins.This new programming paradigm leads t ...

EPFL2021

Representing Monads with Capabilities

Martin Odersky, Aleksander Slawomir Boruch-Gruszecki, Jonathan Immanuel Brachthäuser

Programming with monads can be advantageous even in imperative languages with builtin support for side effects. However, in these languages composing monadic programs is different from composing side effecting imperative programs. This does not need to be ...

2021

Formal Verification of Rust with Stainless

Writing correct software is hard, yet in systems that have a high failure cost or are not easily upgraded like blockchains, bugs and security problems cannot be tolerated. Therefore, these systems are perfect use cases for formal verification, the task of ...

2021

Stoic: Towards Disciplined Capabilities

Martin Odersky, Nada Amin, Fengyun Liu, Sandro Stucki, 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

Type-Safe Metaprogramming and Compilation Techniques For Designing Efficient Systems in High-Level Languages

Lionel Emile Vincent Parreaux

Software engineering practices have been steadily moving towards higher-level programming languages and away from lower-level ones. High-level languages tend to greatly improve safety, productivity, and code maintainability because they handle various impl ...

EPFL2020

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

Finally, a Polymorphic Linear Algebra Language

Amir Shaikhha, Lionel Emile Vincent Parreaux

Many different data analytics tasks boil down to linear algebra primitives. In practice, for each different type of workload, data scientists use a particular specialised library. In this paper, we present Pilatus, a polymorphic iterative linear algebra la ...

2019

Refutation-based synthesis in SMT

Viktor Kuncak, Andrew Joseph Reynolds

We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...

SPRINGER2019

A Programming Model and Foundation for Lineage-Based Distributed Computation

Philipp Haller

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

Verification by Reduction to Functional Programs

Régis William Blanc

In this thesis, we explore techniques for the development and verification of programs in a high-level, expressive, and safe programming language. Our programs can express problems over unbounded domains and over recursive and mutable data structures. We p ...

EPFL2017