-
Living Reference Work Entry In depth
Bit-Level Model Checking
Ensuring that a design conforms to its specification is an indispensable part of the modern design automation flow. Model checking is an automated verification technique for checking whether a given system satisf...
-
Chapter and Conference Paper
Finding All Minimal Safe Inductive Sets
Computing minimal (or even just small) certificates is a central problem in automated reasoning and, in particular, in automated formal verification. For unsatisfiable formulas in CNF such certificates take th...
-
Article
Lagrangian isotopy of tori in \({S^2\times S^2}\) and \({{\mathbb{C}}P^2}\)
We show that, up to Lagrangian isotopy, there is a unique Lagrangian torus inside each of the following uniruled symplectic four-manifolds: the symplectic vector space
-
Article
On computing minimal independent support and its applications to sampling and counting
Constrained sampling and counting are two fundamental problems arising in domains ranging from artificial intelligence and security, to hardware and software testing. Recent approaches to approximate solutions...
-
Chapter and Conference Paper
Mining Backbone Literals in Incremental SAT
In incremental SAT solving, information gained from previous similar instances has so far been limited to learned clauses that are still relevant, and heuristic information such as activity weights and scores....
-
Chapter and Conference Paper
Speeding up MUS Extraction with Preprocessing and Chunking
In this paper we present several improvements to extraction of a minimal unsatisfiable subformula (MUS) of a Boolean formula. As our first contribution, we describe model rotation on preprocessed formulas and ...
-
Chapter and Conference Paper
Generating Modulo-2 Linear Invariants for Hardware Model Checking
We present an algorithm to automatically extract inductive modulo-2 linear invariants from a design. This algorithm makes use of basic linear algebra and is realized on top of an incremental SAT solver. The ex...
-
Chapter and Conference Paper
Computing Interpolants without Proofs
We describe an incremental algorithm for computing interpolants for a pair ϕ A , ϕ B of formulas in propositional logic. ...
-
Chapter and Conference Paper
Perfect Hashing and CNF Encodings of Cardinality Constraints
We study the problem of encoding cardinality constraints (threshold functions) on Boolean variables into CNF. Specifically, we propose new encodings based on (perfect) hashing that are efficient in terms of th...
-
Chapter and Conference Paper
On Efficient Computation of Variable MUSes
In this paper we address the following problem: given an unsatisfiable CNF formula \({\mathcal{F}}\) , find a minimal su...
-
Article
Ruled 4-manifolds and isotopies of symplectic surfaces
We study symplectic surfaces in ruled symplectic 4-manifolds which are disjoint from a given symplectic section. As a consequence, in any symplectic 4-manifold, two homologous symplectic surfaces which are C ...
