Publication

Decision Procedures for Program Synthesis and Verification

Publications associées (95)

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

Yard Optimization at Sea Container Terminals

Michel Bierlaire, Matteo Salani, Ilaria Vacca

Over the last years, international sea-freight container transportation has grown dramatically and container terminals play nowadays a key-role in the global shipping network. The increased competitiveness among terminals requires more and more efficiency ...

2007

Optimization of Container Terminal Operations

Michel Bierlaire, Matteo Salani, Ilaria Vacca

2007

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

Reasoning on Dynamically Built Reasoning Space with Ontology Modules

Several applications require reasoning over autonomously developed ontologies. Initially conceived to explicit the semantics of a certain domain, these ontologies become a powerful tool for supporting business interactions, once heterogeneities have been s ...

2005

Lazy Shape Analysis

Dirk Thilo Beyer, Grégory Théoduloz

2005

TED+: A Data Structure for Microprocessor Verification

Pejman Lotfi Kamran

Formal verification of microprocessors requires a mechanism for efficient representation and manipulation of both arithmetic and random Boolean functions. Recently, a new canonical and graph-based representation called TED has been introduced for verificat ...

2005

Incorporating Domain Knowledge with Video and Voice Data Analysis in News Broadcasts

This paper addresses the area of video annotation, indexing and retrieval, and shows how a set of tools can be employed, along with domain knowledge, to detect narrative structure in broadcast news. The initial structure is detected using low-level audio v ...

2000

A Simple Logic for Authentication Protocol Design

Levente Buttyan, Uwe Wilhelm

In this paper, we describe a simple logic. The logic uses the notion of channels that are generalisations of communication links with various security properties. The abstract nature of channels enables us to treat the protocol at a higher abstraction leve ...

1998

COMPOSER: A case-based reasoning system for engineering design

Pearl Pu Faltings

The frequent use of past experience by human engineers when solving new problems has led to an interest in the use of case based reasoning (CBR) to help automate engineering design. In engineering design it often occurs that many past experiences must be c ...

Cambridge Univ Press, New York, NY, USA1998

SANDS Tools : an environment for deriving parallel programs

This paper describes the techniques and the tools developed to construct CO-OPN specifications (Concurrent Object Oriented Petri Nets) and to derive parallel programs. CO-OPN is a specification language allowing to describe concurrent aspects and data-stru ...

1994