Publication

Interpolation and Quantifiers in Ortholattices

Publications associées (37)

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

GPU Prefilter for Accurate Cubic B-spline Interpolation

Philippe Thévenaz

Achieving accurate interpolation is an important requirement for many signal-processing applications. While nearest-neighbor and linear interpolation methods are popular due to their native GPU support, they unfortunately result in severe undesirable artif ...

Oxford University Press2012

A Verification Toolkit for Numerical Transition Systems

Viktor Kuncak, Hossein Hojjat

This paper presents a publicly available toolkit and a benchmark suite for rigorous verification of Integer Numerical Transition Systems (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We pres ...

2012

Reconstruction of Large, Irregularly Sampled Multidimensional Images. A Tensor-Based Approach

Michaël Unser

Many practical applications require the reconstruction of images from irregularly sampled data. The spline formalism offers an attractive framework for solving this problem; the currently available methods, however, are hard to deploy for large-scale inter ...

IEEE2011

Decision Procedures for Program Synthesis and Verification

Ruzica Piskac

Decision procedures are widely used in software development and verification. The goal of this dissertation is to increase the scope of properties that can be verified using decision procedures. To achieve this goal, we identify three improvements over the ...

EPFL2011

Ordered Sets in the Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints with a rich set of operations. A key challenge is to define such classes of ...

Springer2010

Building a Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets ...

Springer2010

From Lagrange to Shannon...and Back: Another Look at Sampling

Martin Vetterli, Paolo Prandoni

Classical digital signal processing (DSP) lore tells us the tale of a continuous-time primeval signal, of its brutal sampling, and of the magic sinc interpolation that, under the aegis of bandlimitedness, brings the original signal back to (continuous) lif ...

2009

Interpolation and Symbol Elimination

Laura Ildiko Kovacs

We prove several results related to local proofs, interpolation and superposition calculus and discuss their use in predicate abstraction and invariant generation. Our proofs and results suggest that symbol-eliminating inferences may be an interesting alte ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2009

Nonparametric Least Squares Regression for Image Reconstruction on the Sphere

Pascal Frossard, Ivana Tosic, Tamara Tosic

This paper addresses the problem of interpolating signals defined on a 2-d sphere from non-uniform samples. We present an interpolation method based on locally weighted linear and nonlinear regression, which takes into account the differences in importance ...

2009

Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

Motivated by applications in software verification, we explore automated reasoning about the non-disjoint combination of theories of infinitely many finite structures, where the theories share set variables and set operations. We prove a combination theore ...

Springer2009