Publication

The TL Compiler

Related publications (60)

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.

Refinement Propagation. Towards Automated Construction of Visual Specifications.

Alain Wegmann, Irina Rychkova

Creation and transformation of visual specifications is driven by modeler’s design decisions. After a design decision has been made, the modeler needs to adjust the specification to maintain its correctness. The number of adjustments might make the design ...

2007

From Liveness to Promptness

Liveness temporal properties state that something

good'' eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the

wait time'' for an eventually to be fulfilled. That is,

F\theta

...

2007

Supporting Loop Proofs in KeY by using BLAST

Mathias Krebs

In contrast to beta-testing, formal verification can guarantee correctness of a program against a specification. Two basic verification techniques are theorem proving and model checking. Both have strengths and weaknesses. Theorem proving is powerful, but ...

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

An Extensible and Personalized Approach to QoS-enabled Semantic Web Service Discovery

Karl Aberer, Manfred Hauswirth

We present a framework for the autonomous discovery and selection of Semantic Web services based on their QoS properties. The novelty of our approach is the wide use of semantic technologies for a customizable discovery, which enables both the service user ...

2006

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

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

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

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

From Liveness to Promptness

Liveness temporal properties state that something

good'' eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the

wait time'' for an eventually to be fulfilled. That is,

F\theta

...

2007