Publication

Supporting Loop Proofs in KeY by using BLAST

Publications associées (83)

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

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

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

EPICURE : A Partitioning and CoDesign Framework For Reconfigurable Computing

Sébastien Bilavarn

This paper presents a new global design methodology capable to bridge the gap between an abstract specification level and a heterogeneous reconfigurable architecture level. The Epicure contribution is the result of a joint study on abstraction/refinement m ...

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

Expressing Systemic Contexts in Visual Models of System Specifications

Gil Regev, Alain Wegmann, José Diego de la Cruz Garcia

Decision support systems can be used to manage systems. Managed systems are described by system specifications. System specification notations, such as UML, often separate in different diagrams the static specification and the dynamic specification of the ...

2005

Detecting Malicious Code by Model Checking

Johannes Kinder

The ease of compiling malicious code from source code in higher programming languages has increased the volatility of malicious programs: The first appearance of a new worm in the wild is usually followed by modified versions in quick succession. As demons ...

Springer2005

The CHT Play

Rachid Guerraoui, Felix Gaertner

This note gives a high level and informal account of the necessary part of the proof that Ω is the weakest failure detector to implement consensus with a majority of correct processes. The proof originally appeared in a widely cited but rarely understood p ...

2004

Debugging Temporal Specifications with Concept Analysis

James Richard Larus

Program verification tools (such as model checkers and static analyzers) can find many errors in programs. These tools need formal specifications of correct program behavior, but writing a correct specification is difficult, just as writing a correct progr ...

ACM2003

Modeling Consensus in a Process Calculus

Rachele Fuzzati, Massimo Merro

We give a process calculus model that formalizes a well known algorithm (introduced by Chandra and Toueg) solving consensus in the presence of a particular class of failure detectors (Diamond S); we use our model to formally prove that the algorithm satisf ...

2003

Modeling Consensus in a Process Calculus

Rachele Fuzzati, Massimo Merro

We give a process calculus model that formalizes a well-known algorithm (introduced by Chandra and Toueg) solving consensus in the presence of a particular class of failure detectors; we use our model to formally prove that the algorithm satisfies its spec ...

2003