Publication

Debugging Temporal Specifications with Concept Analysis

Graph Chatbot

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.

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

VISUAL CONTRACTS: A way to reason about states and cardinalities in IT system specifications

Alain Wegmann, Lam Son Lê, José Diego de la Cruz Garcia

Visual modeling languages propose specialized diagrams to represent behaviour and concepts necessary to specify IT systems. As a result, to understand a specification, the modeller needs to analyze these two types of diagrams and, often, additional stateme ...

2006

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

The KeY Tool

KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an in ...

Springer2005

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

Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications

Felix Gaertner

The tolerance theory by Arora and Kulkarni views a fault-tolerant program as the composition of a fault-intolerant program and fault tolerance components called detectors and correctors.At its core, the theory assumes that the correctness specifications un ...

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 (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

Mining Specifications

James Richard Larus

Program verification is a promising approach to improving program quality, because it can search all possible program executions for specific errors. However, the need to formally describe correct behavior or errors is a major barrier to the widespread ado ...

ACM2002

A Formal Analysis of Syverson`s Rational Exchange Protocol

Jean-Pierre Hubaux, Levente Buttyan, Srdan Capkun

In this paper, we provide a formal analysis of a rational exchange protocol proposed by Syverson. A rational exchange protocol guarantees that misbehavior cannot generate benefits, and is therefore discouraged. The analysis is performed using our formal mo ...

2002