Author name cluster

Bard Bloom

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

SAT Conference 2012 Conference Paper

SatX10: A Scalable Plug&Play Parallel SAT Framework - (Tool Presentation)

Bard Bloom
David Grove
Benjamin Herta
Ashish Sabharwal
Horst Samulowitz
Vijay A. Saraswat

Abstract We propose a framework for SAT researchers to conveniently try out new ideas in the context of parallel SAT solving without the burden of dealing with all the underlying system issues that arise when implementing a massively parallel algorithm. The framework is based on the parallel execution language X10, and allows the parallel solver to easily run on both a single machine with multiple cores and across multiple machines, sharing information such as learned clauses.

Details

TCS Journal 1995 Journal Article

Structural operational semantics for weak bisimulations

Bard Bloom

In this study, we present rule formats for four main notions of bisimulation with silent moves. Weak bisimulation is a congruence for any process algebra defined by WB cool rules; we have similar results for rooted weak bisimulation (Milner's “observational congruence”), branching bisimulation, and rooted branching bisimulation. The theorems stating that, say, observational congruence is an appropriate notion of equality for CCS are corollaries of the results of this paper. We also give sufficient conditions under which equational axiom systems can be generated from operational rules. Indeed, many equational axiom systems appearing in the literature are instances of this general theory.

Details DOI

TCS Journal 1992 Journal Article

Experimenting with process equivalence

Bard Bloom
Albert R. Meyer

Distinctions between concurrent processes based on observable outcomes of computational experiments are examined. The equivalence determined by a general class of experiments involving duplication of processes can be characterized by a notion of ready simulation resembling, but strictly coarser than, Milner's bisimulation equivalence.

Details DOI

I&C Journal 1990 Journal Article

Can LCF be topped? Flat lattice models of typed λ-calculus

Bard Bloom

Plotkin ((1977) Theoret. Comput. Sci. 5: 223–256) examines the denotational semantics of PCF (essentially typed λ-calculus with arithmetic and looping). The standard Scott semantics V is computationally adequate but not fully abstract; with the addition of some parallel facilities, it becomes fully abstract, and with the addition of an existential operator, denotationally universal. We consider carrying out the same program for ⊙, the Scott models built from flat lattices rather than flat cpo's. Surprisingly, no computable extension of PCF can be denotationally universal; perfectly reasonable semantic values such as supremum and Plotkin's “parallel or” cannot be definable. There is an unenlightening fully abstract extension L A (approx), based on Gödel numbering and syntactic analysis. Unfortunately, this is the best we can do; operators defined by PCF-style rules cannot give a fully abstract language. (There is a natural and desirable property, operational extensionality, which prevents full abstraction with respect to ⊙.) However, we show that Plotkin's program can be carried out for a nonconfluent evaluator.

Details DOI