Publication

Ordered Sets in the Calculus of Data Structures

Related publications (104)

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.

A Theory Agenda for Component-Based Design

Joseph Sifakis, Simon Bliudze

The aim of the paper is to present a theory agenda for component-based design based on results that motivated the development of the BIP component framework, to identify open problems and discuss further research directions. The focus is on proposing a sem ...

Springer International Publishing2015

Lower bounds for Pythagoras numbers of function fields

David Maximilian Grimm

We show that the transcendence degree of a real function field over an arbitrary real base field is a strict lower bound for its Pythagoras number and a weak lower bound for all its higher Pythagoras numbers. ...

European Mathematical Soc2015

Sampling Curves with Finite Rate of Innovation

Thierry Blu, Hanjie Pan, Pier Luigi Dragotti

In this paper, we extend the theory of sampling signals with finite rate of innovation (FRI) to a specific class of two-dimensional curves, which are defined implicitly as the zeros of a mask function. Here the mask function has a parametric representation ...

Institute of Electrical and Electronics Engineers2014

Verifying and Synthesizing Software with Recursive Functions (Invited Contribution)

Viktor Kuncak

Our goal is to help people construct software that does what they wish. We develop tools and algorithms that span static and dynamic verification, constraint solving, and program synthesis. I will outline the current state our verification and synthesis sy ...

Springer-Verlag Berlin2014

Odd linking and bifurcation in gaps: the weakly indefinite case

In this paper, we consider nonlinear Schrodinger equations of the following type: -Delta u(x) + V (x) u(x) -q(x)|u(x)|sigma u(x) =lambda u(x), x is an element of R-N, u is an element of H-1(R-N) \ {0}, where N >= 2 and sigma > 0. We concentrate on situatio ...

Royal Society of Edinburgh Scotland Foundation, Cambridge2013

Interpolation for Synthesis on Unbounded Domains

Viktor Kuncak, Régis William Blanc

Synthesis procedures compile relational specifications into functions. In addition to bounded domains, synthesis procedures are applicable to domains such as mathematical integers, where the domain and range of relations and synthesized code is unbounded. ...

Ieee2013

Conductance Switching and Many-Valued Logic in Porphyrin Assemblies

Nicola Marzari

We investigate quantum interference in the transport properties of porphyrin-based molecular devices, and are able to develop a minimal but qualitatively accurate model of conductance based on the maximally localized Wannier functions of just the isolated ...

Amer Chemical Soc2013

Tree Interpolation in Vampire

Régis William Blanc, Laura Ildiko Kovacs, Ashutosh Gupta

We describe new extensions of the Vampire theorem prover for computing tree interpolants. These extensions generalize Craig interpolation in Vampire, and can also be used to derive sequence interpolants. We evaluated our implementation on a large number of ...

Springer Berlin Heidelberg2013

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

Bilinear Control Systems with Forced Integrable Filtration

Philippe Müllhaupt, Basile Graf

A class of nonlinear systems and a filtration of the corresponding codistributions are presented. The filtration enjoys some strong integrability property which allows an easy computation of a linearizing normal form whenever the algorithm terminates with ...

American Institute of Physics2012