An Update on Deductive Synthesis and Repair in the Leon Tool

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.

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

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 ...

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to ...

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 ...

Software network functions (NFs), such as a network address translator, load balancer, or proxy, promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs. However, continuous updates and flexibility typically c ...

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 ...

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 ...

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 ...

Adaptive design strategies have been employed to improve structural performances in terms of load-bearing efficiency and energetic impact as well as to achieve multi-functionality. In this work, we investigate a passive adaptation strategy that employs var ...

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 ...

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 ...

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 ...

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 ...

As of today, programming has never been so accessible. Yet, it remains a challenge for end-users: students, non-technical employees, experts in their domains outside of computer science, and so on. With its forecast potential for solving problems by only o ...

Understanding a program entails understanding its context; dependencies, configurations and even implementations are all forms of contexts. Modern programming languages and theorem provers offer an array of constructs to define contexts, implicitly. Scala ...

Synthesis from examples enables non-expert users to generate programs by specifying examples of their behavior. A domain-specific form of such synthesis has been recently deployed in a widely used spreadsheet software product. In this paper we contribute t ...

We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs ...

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 ...

An Update on Deductive Synthesis and Repair in the Leon Tool

Chat with Graph Search

Automated Formal Verification of Software Network Functions

Degrees of Separation: A Flexible Type System for Safe Concurrency

Scaling Language Features for Program Verification

Representing Monads with Capabilities

Proving and Disproving Equivalence of Functional Programming Assignments

Trust as a Programming Primitive

Verification of Software Network Functions with No Verification Expertise

Verified Functional Programming

Scaling Functional Synthesis and Repair

Refutation-based synthesis in SMT

Structural Adaptation through Stiffness Tuning

A Programming Model and Foundation for Lineage-Based Distributed Computation

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

Verification by Reduction to Functional Programs

Algorithmic Resource Verification

Interactive Programming by Example

Simplicitly: Foundations and Applications of Implicit Function Types

Proactive Synthesis of Recursive Tree-to-String Functions from Examples

Translating Scala Programs to Isabelle/HOL, Automated Reasoning

Deductive Synthesis and Repair