Publications by Grégory Théoduloz

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

Program Analysis with Dynamic Precision Adjustment

Dirk Thilo Beyer, Grégory Théoduloz

We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a ...

IEEE2008

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

Dirk Thilo Beyer, 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 are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this p ...

Springer2007

Integrating Shape Analysis into the Model Checker BLAST

Dirk Thilo Beyer, Grégory Théoduloz

Many software model checkers are based on predicate abstraction. Values of variables in branching conditions are represented abstractly using predicates. The strength of this approach is its path-sensitive nature. However, if the control flow depends heavi ...

2006

Lazy Shape Analysis

Dirk Thilo Beyer, Grégory Théoduloz

Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analy ...

Springer2006

Lazy Shape Analysis

Dirk Thilo Beyer, Grégory Théoduloz

2005

Grégory Théoduloz

Graph Chatbot

Chat with Graph Search

Software Verification by Combining Program Analyses of Adjustable Precision

Shape Refinement through Explicit Heap Analysis

Program Analysis with Dynamic Precision Adjustment

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

Integrating Shape Analysis into the Model Checker BLAST

Lazy Shape Analysis

Lazy Shape Analysis

Software Verification by Combining Program Analyses of Adjustable Precision

Shape Refinement through Explicit Heap Analysis

Integrating Shape Analysis into the Model Checker BLAST

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

Lazy Shape Analysis

Program Analysis with Dynamic Precision Adjustment

Lazy Shape Analysis