Publication

Path invariants

Publications associées (44)

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

Programming with Specifications

Philippe Paul Henri Suter

This thesis explores the use of specifications for the construction of correct programs. We go beyond their standard use as run-time assertions, and present algorithms, techniques and implementations for the tasks of 1) program verification, 2) declarative ...

EPFL2012

A Verification Toolkit for Numerical Transition Systems

Viktor Kuncak, Hossein Hojjat

This paper presents a publicly available toolkit and a benchmark suite for rigorous verification of Integer Numerical Transition Systems (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We pres ...

2012

Finding Almost-Invariants in Distributed Systems

Dejan Kostic, Marco Canini, Maysam Yabandeh

It is notoriously hard to develop dependable distributed systems. This is partly due to the difficulties in foreseeing various corner cases and failure scenarios while implementing a system that will be deployed over an asynchronous network. In contrast, r ...

2011

Striking a New Balance Between Program Instrumentation and Debugging Time

Willy Zwaenepoel, Ricardo Bianchini, Olivier Crameri

Although they are helpful in many cases, state-of-the-art bug reporting systems may impose excessive overhead on users, leak private information, or provide little help to the developer in locating the problem. In this paper, we explore a new approach to b ...

Acm Order Department, P O Box 64145, Baltimore, Md 21264 Usa2011

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

Static Analysis of x86 Executables

Johannes Kinder

This dissertation is concerned with static analysis of binary executables in a theoretically well-founded, sound, yet practical way. The major challenge is the reconstruction of a correct control flow graph in presence of indirect jumps, pointer arithmetic ...

Technische Universität Darmstadt2010

Counterexample-Guided Focus

The automated inference of quantified invariants is considered one of the next challenges in software verification. The question of the right precision-efficiency tradeoff for the corresponding program analyses here boils down to the question of the right ...

2010

Runtime Instrumentation for Precise Flow-Sensitive Type Analysis

Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter

We describe a combination of runtime information and static analysis for checking properties of complex and configurable systems. The basic idea of our approach is to 1) let the program execute and thereby read the important dynamic configuration data, the ...

Springer2010

Runtime Instrumentation for Precise Flow-Sensitive Type Analysis

Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter

2010

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