Publications by Dirk Thilo Beyer

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

Algorithms for Interface Synthesis

Vasu Singh, Dirk Thilo Beyer

A temporal interface for a software component is a ﬁnite automaton that speciﬁes the legal sequences of calls to functions that are provided by the component. We compare and evaluate three different algorithms for automatically extracting temporal interfac ...

Springer2007

Implementation of a Modeling Tool Using Alloy as Meta-Modeling Language and CrocoPat as Validation Tool

Alain Wegmann, Lam Son Lê, Dirk Thilo Beyer, Lotfi Hussami

The context of our work is a project that focuses on methods and tools for modeling enterprise architectures. An enterprise architecture model represents the structure of an enterprise across multiple levels, from the markets in which it operates down to t ...

2006

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

Path Invariants

Dirk Thilo Beyer, Andrey Rybalchenko

The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a new method for automated abstraction refinement, which overcomes the inherent limitations of predicate discovery schemes. In ...

2006

Dirk Thilo Beyer

Graph Chatbot

Chat with Graph Search

Shape Refinement through Explicit Heap Analysis

Program Analysis with Dynamic Precision Adjustment

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

Path invariants

Algorithms for Interface Synthesis

An Interface Formalism for Web Services

Implementation of a Modeling Tool Using Alloy as Meta-Modeling Language and CrocoPat as Validation Tool

Integrating Shape Analysis into the Model Checker BLAST

Lazy Shape Analysis

Path Invariants

Implementation of a Modeling Tool Using Alloy as Meta-Modeling Language and CrocoPat as Validation Tool

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

Algorithms for Interface Synthesis

Program Analysis with Dynamic Precision Adjustment

Path invariants

Lazy Shape Analysis

An Interface Formalism for Web Services

Integrating Shape Analysis into the Model Checker BLAST

Path Invariants

Shape Refinement through Explicit Heap Analysis