Publication

Programming with Specifications

Publications associées (108)

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

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

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

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

On Decision Procedures for Algebraic Data Types with Abstractions

Viktor Kuncak, Philippe Paul Henri Suter, Mirco Dotta

We describe a parameterized decision procedure that extends the decision procedure for functional recursive algebraic data types (trees) with the ability to specify and reason about abstractions of data structures. The abstract values are specified using r ...

2009

Programming with Undo

Ersoy Bayramoglu

This thesis is about objects that can undo their state changes. Based on an earlier work on data structure persistence, we propose generating undo methods for classes from annotated classes automatically. As opposed to ephemeral data structures, persistent ...

2009

On Set-Driven Combination of Logics and Verifiers

Viktor Kuncak

We explore the problem of automated reasoning about the non-disjoint combination of logics that share set variables and operations. We prove a general combination theorem, and apply it to show the decidability for the quantifier-free combination of formula ...

2009

Efficient Data Structures For Decision Diagrams

Stéphane Rabie

Dynamic Programming Optimization (DPOP) is an algorithm proposed to solve distributed constraint optimization problems. In order to represent the multi-values functions manipulated in this algorithm, a data structure called Hypercube was implemented. A mor ...

2009

Elastic Transactions

Rachid Guerraoui, Vincent Gramoli, Pascal Felber

This paper presents elastic transactions, a variant of the transactional model. Upon conflict detection, an elastic transaction might drop what it did so far within a separate transaction that immediately commits, and initiate a new transaction which might ...

2009

Simplifying Distributed System Development

Viktor Kuncak, Dejan Kostic, Maysam Yabandeh, Nedeljko Vasic

Distributed systems are difficult to design and develop. The difficulties arise both in basic safety correctness properties, and in achieving high performance. As a result of this complexity, the implementation of a distributed system often contains the ba ...

2009

Elastic Transactions

Rachid Guerraoui, Vincent Gramoli, Pascal Felber

Springer2009