Publication

On Deductive Program Repair in Leon

Related publications (42)

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.

An Update on Deductive Synthesis and Repair in the Leon Tool

Viktor Kuncak, Etienne Kneuss

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

A Study on the Programming Structures for RRAM-based FPGA Architectures

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Xifan Tang, Gain Kim

Field Programmable Gate Arrays (FPGAs) can benefit non-volatility and high-performance by exploiting Resistive Random Access Memories (RRAMs). In RRAM-based FPGAs, the memories do not only replace the SRAMs and store configurations, but they can also repla ...

Ieee-Inst Electrical Electronics Engineers Inc2016

Automating Verification of Functional Programs with Quantified Invariants

Viktor Kuncak, Nicolas Charles Yves Voirol

We present the foundations of a verifier for higher-order functional programs with generics and recursive algebraic data types. Our ver- ifier supports finding sound proofs and counterexamples even in the presence of certain quantified invariants and recur ...

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

Deductive Program Repair, Computer Aided Verification

Viktor Kuncak, Etienne Kneuss

We present an approach to program repair and its application to programs with recursive functions over unbounded data types. Our approach formulates program repair in the framework of deductive synthesis that uses existing program structure as a hint to gu ...

2015

Traversal Query Language For Scala.Meta

Eugene Burmako, Eric Beguet

With the rise of metaprogramming in Scala, manipulating ASTs has become a daily job. Yet the standard API provides only low-level mechanisms to transform or to collect information on those data structures. Moreover, those mechanisms often force the program ...

2015

Grammar-based generation of equilibrium structures through graphic statics

Corentin Jean Dominique Fivet

This paper proposes a grammar-based structural design methodology using graphic statics. By combining shape grammars with graphic statics, this method enables the designer to: 1) rapidly generate unique, yet functional structures that fall outside of the e ...

IASS2015

On Integrating Deductive Synthesis and Verification Systems

Viktor Kuncak, Etienne Kneuss, Ivan Kuraj, Philippe Paul Henri Suter

We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete synt ...

2013

, , ,

2013