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.

Shape Refinement through Explicit Heap Analysis

Dirk Thilo Beyer, Grégory Théoduloz, Damien Zufferey

Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structu ...

Springer2010

Software Verification by Combining Program Analyses of Adjustable Precision

Grégory Théoduloz

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers, on one hand, are still mostly concerned with precision, e.g., the removal of spurious counterexampl ...

EPFL2010

Deprecating the Observer Pattern

Martin Odersky, Tiark Rompf, Ingo Maier

Programming interactive systems by means of the observer pattern is hard and error-prone yet is still the implementation standard in many production environments. We present an approach to gradually deprecate observers in favor of reactive programming abst ...

2010

Reasoning algebraically about P-solvable loops

Laura Ildiko Kovacs

We present a method for generating polynomial invariants for a subfamily of imperative loops operating on numbers, called the P-solvable loops. The method uses algorithmic combinatorics and algebraic techniques. The approach is shown to be complete for som ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2008

Autonomous-System Interfaces

The current Internet is characterized by a growing tension between the "core" (the Internet service providers) and the "edge" (the operators of edge networks and distributed applications). Much of this tension concerns path visibility and control -- where ...

2007

not available ...

2002

Fast Functional Lists, Hash-Lists, Deques and Variable Length Arrays

Since its inception Functional Programming, J. McCarthy, has almost universally used the Linked List as the underpinning data structure. This paper introduces a new data structure, the VList, that is compact, thread safe and significantly faster to use tha ...

2002

Specifying System Behavior in UML

Shane Sendall

The purpose of the paper is to present our approach for specifying system behavior. Our approach is based on operation schemas and a system interface protocol (SIP). Operation schemas describe the functionality of system operations by pre- and post-conditi ...

2000

Programming with Variable Functions

Martin Odersky

What is a good method to specify and derive imperative programs? This paper argues that a new form of functional programming fits the bill, where variable functions can be updated at specified points in their domain. Traditional algebraic specification and ...

1998

Automatic implementations of abstract data types (ADT) from algebraic specifications are currently all done in either functional, logical or purely imperative languages. In this paper we show how object-oriented languages naturally facilitate this job, and ...

1995