Interpolation for Synthesis on Unbounded Domains

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.

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem ...

We give a construction of an efficient one-out-of-many proof system, in which a prover shows that he knows the pre-image for one element in a set, based on the hardness of lattice problems. The construction employs the recent zero-knowledge framework of Ly ...

Background: The increasingly common applications of machine-learning schemes to atomic-scale simulations have triggered efforts to better understand the mathematical properties of the mapping between the Cartesian coordinates of the atoms and the variety o ...

On ten loose handwritten folios dating back from April 1679, Leibniz gradually devised, in the course of three days, a full-blown theory of thought that nonetheless remained unpublished and still has received little attention from scholars. Conceiving of a ...

Thermodynamic phase diagrams are the cornerstones to develop synthesis of new materials. Zinc phosphide has evolved into a prospective semicontuctor for next generation solar cells, thanks to its abundance and functional properties. Here we derive an optim ...

Hard-wired carry chains in FPGAs are designed to improve efficiency of important arithmetic primitives. Although they are proven to be effective for arithmetic-rich functions, there are very few studies on the optimization opportunities of carry chains for ...

In the present thesis, we delve into different extremal and algebraic problems arising from combinatorial geometry. Specifically, we consider the following problems. For any integer

n\ge 3

, we define

e(n)

to be the minimum positive integer such that an ...

We present a formalism, algorithms and tools to synthesise reactive systems that behave efficiently, i.e., which achieve an optimal trade-off between a given cost and reward model. Synthesis aims to automatically generate a program from a specification. Mo ...

Let parallel to.parallel to be a norm in R-d whose unit ball is B. Assume that V subset of B is a finite set of cardinality n, with Sigma(v is an element of V) v = 0. We show that for every integer k with 0

We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1) interaction logics for the specification of arch ...

We extend the Leon verification system for Scala with support for bit-vector reasoning, thus addressing one of its fundamental soundness limitation with respect to the treatment of integers primitives. We leverage significant progresses recently achieved i ...

This paper defines the problem of Scalable Secure computing in a Social network: we call it the S-3 problem. In short, nodes, directly reflecting on associated users, need to compute a symmetric function f : V-n -> U of their inputs in a set of constant si ...

Let r : S x S -> R+ be the jump rates of an irreducible random walk on a finite set S, reversible with respect to some probability measure m. For alpha > 1, let g : N -> R+ be given by g(0) = 0, g(1) = 1, g(k) = (k/k - 1)(alpha), k >= 2. Consider a zero ra ...

Our brain-actuated wheelchair uses shared control to couple the user input with the contextual information about the surroundings in order to perform natural manoeuvres both safely and efficiently. In this study, we investigate the feasibility of using our ...

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 ...

Systems on Chip (SoCs) and Systems in Package (SiPs) are key parts of a continuously broadening range of products, from chip cards and mobile phones to cars. Besides an increasing amount of digital hardware and software for data processing and storage, the ...

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 ...

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 ...

Interpolation for Synthesis on Unbounded Domains

Chat with Graph Search

Orthologic with Axioms

LISA – A Modern Proof System

Formula Normalizations in Verification

BLOOM: Bimodal Lattice One-out-of-Many Proofs and Applications

Local invertibility and sensitivity of atomic structure-feature mappings

An Ink–and–Paper Automaton: The Conceptual Mechanization of Cognition and the Practical Automation of Reasoning in Leibniz’s De Affectibus (1679)

Thermodynamic re-assessment of the Zn–P binary system

Improving Circuit Mapping Performance Through MIG-based Synthesis for Carry Chains

On some algebraic and extremal problems in discrete geometry

Synthesizing efficient systems in probabilistic environments

Small subset sums

Configuration Logics: Modelling Architecture Styles

Sound reasoning about integral data types with a reusable SMT solver interface

Computing in social networks

Metastability of reversible condensed zero range processes on a finite set

Driving a BCI Wheelchair: A Patient Case Study

Decision Procedures for Program Synthesis and Verification

Efficient Modelling and Simulation Methodology for the Design of Heterogeneous Mixed-Signal Systems on Chip

Ordered Sets in the Calculus of Data Structures

Building a Calculus of Data Structures