Publication

Proving memory safety of floating-point computations by combining static and dynamic program analysis

Publications associées (74)

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

Selective Symbolic Execution

George Candea, Cristian Zamfir, Vitaly Chipounov

Symbolic execution is a powerful technique for analyzing program behavior, finding bugs, and generating tests, but suffers from severely limited scalability: the largest programs that can be symbolically executed today are on the order of thousands of line ...

2009

Constraint Solving for Software Reliability and Text Analysis

Viktor Kuncak

We will develop and implement new algorithms for constraint solving and apply them to construct two classes of tools: 1) bug finding and verification tools building on tools such as Java PathFinder and Jahob; 2) tools for deep semantic analysis of texts co ...

2008

Program Analysis with Dynamic Precision Adjustment

Dirk Thilo Beyer, Grégory Théoduloz

We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a ...

IEEE2008

Implementation of batch-based particle filters for multi-sensor tracking

Volkan Cevher

In this paper, we demonstrate fixed-point FPGA implementations of state space systems using Particle Filters, especially multi-target beating and range tracking systems. These trackers operate either as independent organic trackers or as a joint tracker to ...

2007

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

Dynamic Texture on Fixed-Point Architectures

Sabine Süsstrunk, Luciano Sbaiz, Roberto Costantini

Dynamic textures are sequences of images showing temporal regularity; they can be found in videos representing smoke, flames, flowing water, or moving grass, for instance. Recently, one method based on linear dynamic system theory was proposed to synthesiz ...

2006

Rigorous solution techniques for numerical constraint satisfaction problems

Xuan-Ha Vu

A constraint satisfaction problem (e.g., a system of equations and inequalities) consists of a finite set of constraints specifying which value combinations from given variable domains are admitted. It is called numerical if its variable domains are contin ...

EPFL2005

Adding limited reconfigurability to superscalar processors

Marc Epalza

For the last thirty years, electronics, at first built with discrete components, and then as Integrated Circuits (IC), have brought diverse and lasting improvements to our quality of life. Examples might include digital calculators, automotive and airplane ...

EPFL2004

The IF toolset

Joseph Sifakis

This paper presents an overview on the IF toolset which is an environment for modelling and validation of heterogeneous real-time systems. The toolset is built upon a rich formalism, the IF notation, allowing structured automata-based system representation ...

2004

Schubfestigkeit und Durchstanzen von Platten ohne Querkraftbewehrung

Aurelio Muttoni

A general calculation model is developed and described starting from the effective load-carrying mechanisme of edge- and point supported (punching shear) slabs. This leads to a simplified and practical design process for shear. This method, originally deve ...

Beton- und Stahlbetonbau2003