Publication

On Accelerating Interpolants

Related publications (32)

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.

On Static Analysis for Expressive Pattern Matching

Viktor Kuncak, Philippe Paul Henri Suter, Mirco Dotta

Pattern matching is a widespread programming language construct that enables definitions of values by cases, generalizing if-then-else and case statements. The cases in a pattern matching expression should be exhaustive: when the value does not match any o ...

2008

Belief Propagation on Uncertain Schema Mappings in Peer Data Management Systems

Karl Aberer, Philippe Cudré-Mauroux

Until recently, most data integration techniques involved central components, e.g., global schemas, to enable transparent access to heterogeneous databases. Today, however, with the democratization of tools facilitating knowledge elicitation in machine-pro ...

IOSPress2006

Probabilistic Message Passing in Peer Data Management Systems

Karl Aberer, Philippe Cudré-Mauroux

IEEE2006

Foundations for SCALA

Vincent Cremet

SCALA is an attractive programming language because it is both very expressive and statically strongly typed. This marriage against nature comes at the price of a certain complexity in the language constructs and the static analysis. This complexity makes ...

EPFL2006

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

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

2005

The Definition of Transitive Closure with OCL - Limitations and applications

The Object Constraint Language (OCL) is based on rst- order logic and set theory. As the most well-known application, OCL is used to formulate well-formedness rules in the UML metamodel. Here, the transitive closure of a relationship is de ned in terms of ...

2003

The Definition of Transitive Closure with OCL: Limitations and Applications

The Object Constraint Language (OCL) is based on first-order logic and set theory. As the most well-known application, OCL is used to formulate well-formedness rules in the UML metamodel. Here, the transitive closure of a relationship is defined in terms o ...

2003

A Functional View of Join

Martin Odersky, Matthias Zenger

Join calculus, usually presented as a process calculus, is suitable as a foundation of both sequential and concurrent programming. We give a new operational semantics of join calculus, expressed as a reduction system with a single reduction rule similar to ...

1999