Concept

Formule booléenne quantifiée

Publications associées (39)

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

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

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

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

Modeling stochasticity and robustness in gene regulatory networks

Giovanni De Micheli, Abhishek Garg, Ioannis Xenarios

Motivation: Understanding gene regulation in biological processes and modeling the robustness of underlying regulatory networks is an important problem that is currently being addressed by computational systems biologists. Lately, there has been a renewed ...

2009

Non-Clausal Satisfiability Modulo Theories

Philippe Paul Henri Suter

This thesis presents NC(T), an extension of the DPLL(T) scheme [16, 29] for decision procedures for quantifier-free first-order logics. In DPLL(T), a general Boolean DPLL engine is instantiated with a theory solver for the theory T. The DPLL engine is resp ...

2008

Information Visualization of Multi-dimensional Cellular Automata using GPU Programming

Stéphane Gobron

We propose a method for generating all possible rules of multidimension Boolean cellular automata (CA). Based on an original encoding method and the programming of graphical processor units (GPU), this method allows us to visualize the CA information flow ...

IEEE Computer Society2007

EP theorems and linear complementary problems

Let A be a rational n × n square matrix and b be a rational n-vector for some positive integer n. The linear complementarity problem (abbreviated by LCP) is to find a vector (x, y) in R^(2n) satisfying y = Ax + b (x, y) >= 0 and the complementarity conditi ...

1998

A Boolean Approach to Construct Neural Networks for Non-Boolean Problems

A neural network construction method for problems specified for data sets with in- and/or output values in the continuous or discrete domain is described and evaluated. This approach is based on a Boolean approximation of the data set and is generic for va ...

1996

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