Concept

2-satisfiability

Related publications (49)

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.

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

Scala to the Power of Z3: Integrating SMT and Programming

Viktor Kuncak, Philippe Paul Henri Suter

We describe a system that integrates the SMT solver Z3 with the Scala programming language. The system supports the use of the SMT solver for checking satisfiability, unsatisfiability, as well as solution enumeration. The embedding of formula trees into Sc ...

Springer-Verlag Berlin2011

Verification of consensus algorithms using satisfiability solving

André Schiper

Consensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms ...

Springer Verlag2011

Fast Randomized Test-and-Set and Renaming

Rachid Guerraoui, Seth Gilbert, Dan Alistarh, Hagit Albo Attiya, Andrei Giurgiu

Most people believe that renaming is easy: simply choose a name \emph{at random}; if more than one process selects the same name, then try again. We highlight the issues that occur when trying to implement such a scheme and shed new light on the read-write ...

2010

On Deciding Functional Lists with Sublist Sets

Viktor Kuncak

Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functional lists. We first show how to decide in NP the satisfiability problem for lo ...

2010

Fast Randomized Test-and-Set and Renaming

Rachid Guerraoui, Seth Gilbert, Dan Alistarh, Hagit Albo Attiya, Andrei Giurgiu

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

Conditional hardness of precedence constrained scheduling on identical machines

Ola Nils Anders Svensson

Already in 1966, Graham showed that a simple procedure called list scheduling yields a 2-approximation algorithm for the central problem of scheduling precedence constrained jobs on identical machines to minimize makespan. Till this date it has remained th ...

ACM2010

Approximating Parameterized Convex Optimization Problems.

Martin Jaggi

We extend Clarkson's framework by considering parameterized convex optimization problems over the unit simplex, that depend on one parameter. We provide a simple and efficient scheme for maintaining an ε-approximate solution (and a corresponding ε-coreset) ...

2010

On Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

We explore the problem of automated reasoning about the non-disjoint combination of theories that share set variables and operations. We prove a combination theorem and apply it to show the decidability of the satisfiability problem for a class of formulas ...

2009

Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars

Viktor Kuncak, Ruzica Piskac

We present decision procedures for logical constraints that support reasoning about collections of elements such as sets, multisets, and fuzzy sets. Element membership in such collections is given by a characteristic function from a finite universe (of unk ...

2008