Publication

Developing Verified Software Using Leon

Publications associées (40)

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

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

Contract-Based Resource Verification for Higher-Order Functions with Memoization

Viktor Kuncak, Ravichandhran Kandhadai Madhavan, Sumith Kulal

We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. a ...

Assoc Computing Machinery2017

Elastic Program Transformations

Jonas Benedict Wagner

Performance and reliability are important yet conflicting properties of systems software. Software today often crashes, has security vulnerabilities and data loss, while many techniques that could address such issues remain unused due to performance concer ...

EPFL2017

Static estimation of resource utilisation of programs is a challenging and important problem with numerous applications. In this thesis, I present new algorithms that enable users to specify and verify their desired bounds on resource usage of functional p ...

EPFL2017

We report our progress in scaling deductive synthesis and repair of recursive functional Scala programs in the Leon tool. We describe new techniques, including a more precise mechanism for encoding the space of meaningful candidate programs. Our techniques ...

2017

Deductive Synthesis and Repair

Etienne Kneuss

In this thesis, we explore techniques for the development of recursive functional programs over unbounded domains that are proved correct according to their high-level specifications. We present algorithms for automatically synthesizing executable code, st ...

EPFL2016

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

Verifying Resource Bounds of Programs with Lazy Evaluation and Memoization

Viktor Kuncak, Ravichandhran Kandhadai Madhavan, Sumith Kulal

We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy eval- uation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. ...

2016

Function Passing: A Model for Typed, Distributed Functional Programming

Philipp Haller, Jocelyn Boullier

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 on which to build data-centric distributed systems. A key id ...

Assoc Computing Machinery2016

IX Open-source version 1.1 - Deployment and Evaluation Guide

Edouard Bugnion, Evangelos Marios Kogias, Christos Kozyrakis, Georgios Prekas, Mia Primorac, Bernard Gütermann, Ana Klimovic

This Technical Report provides the deployment and evaluation guide of the IX dataplane operating system, as of its first open-source release on May 27, 2016. To facilitate the reproduction of our results, we include in this report the precise steps needed ...

2016