Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Axiomes de Peano

Publications associées (8)

Extractable Witness Encryption for the Homogeneous Linear Equations Problem

Serge Vaudenay, Bénédikt Minh Dang Tran

Witness encryption is a cryptographic primitive which encrypts a message under an instance of an NP language and decrypts the ciphertext using a witness associated with that instance. In the current state of the art, most of the witness encryption construc ...

Springer2023

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...

EPFL2019

Solving quantified linear arithmetic by counterexample-guided instantiation

Viktor Kuncak, Andrew Joseph Reynolds

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedur ...

2017

A Divide-and-Conquer Approach for Solving Interval Algebra Networks

Jingshi Li

Deciding consistency of constraint networks is a fundamental problem in qualitative spatial and temporal reasoning. In this paper we introduce a divide-and-conquer method that recursively partitions a given problem into smaller sub-problems in deciding con ...

2009

Decision Procedures for Multisets with Cardinality Constraints

Viktor Kuncak, Ruzica Piskac

Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these scenarios. Multisets arise for analogous reasons as sets: abstracting the c ...

Springer2008

Linear Arithmetic with Stars

Viktor Kuncak, Ruzica Piskac

We consider an extension of integer linear arithmetic with a “star” operator takes closure under vector addition of the solution set of a linear arithmetic subformula. We show that the satisfiability problem for this extended language remains in NP (and th ...

Springer2008

Weak metrics on Euclidean domains

Marc Troyanov

A weak metric on a set is a function that satisfies the axioms of a metric except the symmetry and the separation axioms. The aim of this paper is to present some interesting weak metrics and to study some of their properties. In particular, we introduce a ...

2007

Discrete choice models with multiplicative error terms

Michel Bierlaire

The conditional indirect utility of many random utility maximization (RUM) discrete choice models is specified as a sum of an index V depending on observables and an independent random term P. In general, the universe of RUM consistent models is much large ...

2007

Publications associées (8)