Publication

On Deciding Functional Lists with Sublist Sets

Publications associées (88)

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

On an Efficient Decision Procedure for Imperative Tree Data Structures

Viktor Kuncak

We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invari ...

2011

A Model Predictive Control Approach to Trajectory Tracking Problems via Time-Varying Level Sets of Lyapunov Functions

Timm Faulwasser

We discuss a model predictive control approach to trajectory tracking problems of constrained nonlinear con- tinuous time systems, where the reference trajectory is a priori known and asymptotically constant. The proposed NMPC scheme is able to explicitly ...

2011

How Important is the Detection of Changes in Active Constraints in Real-Time Optimization?

Dominique Bonvin, Saurabh Anand Deshpande

In real-time optimization, enforcing the constraints that need to be active is important for optimality. In fact, it has been established in the context of parametric variations that, if these constraints are not satisfied, the optimality loss would be O($ ...

2011

Satisfiability Modulo Recursive Programs

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of expressive correctness properties of recursive first-order functional programs. In our approach, both properties and programs are expressed in the same language, a subset of Scala. We impl ...

Springer-Verlag Berlin2011

MDD propagators with explanation

Radoslaw Szymanek

Multi-valued decision diagrams (MDDs) are a convenient approach to representing many kinds of constraints including table constraints, regular constraints, complex set and multiset constraints, as well as ad-hoc problem specific constraints. This paper int ...

2011

Decision Procedures for Automating Termination Proofs

Ruzica Piskac

Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current too ...

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

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

On Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Philippe Paul Henri Suter, Robin Steiger

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier- ...

2010

Drawing Hamiltonian cycles with no large angles

János Pach

Let n >= 4 be even. It is shown that every set S of n points in the plane can be connected by a (possibly self-intersecting) spanning tour (Hamiltonian cycle) consisting of n straight-line edges such that the angle between any two consecutive edges is at m ...

Springer-Verlag2010

Computing in Social Networks

Rachid Guerraoui, Anne-Marie Kermarrec, Kévin Clément Huguenin, Andrei Giurgiu

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 function f : V -> U of their inputs in a set of constant size, in a sca ...

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