Publications Search Tool

@article{Cassidy:2005:STC:1705513.1705661,
title = {Source Transformation for Concurrency Analysis},
author = {Timothy Cassidy and James R Cordy and Thomas R Dean and Juergen Dingel},
url = {http://dx.doi.org/10.1016/j.entcs.2005.05.012},
doi = {10.1016/j.entcs.2005.05.012},
issn = {1571-0661},
year = {2005},
date = {2005-01-01},
journal = {Electron. Notes Theor. Comput. Sci.},
volume = {141},
number = {4},
pages = {57-75},
publisher = {Elsevier},
keywords = {},
pubstate = {published},
tppubtype = {article}
}

@article{Dingel2002,
title = {A Refinement Calculus for Shared-Variable Parallel and Distributed Programming},
author = {Juergen Dingel},
url = {http://dx.doi.org/10.1007/s001650200032},
doi = {10.1007/s001650200032},
issn = {1433-299X},
year = {2002},
date = {2002-12-01},
journal = {Formal Aspects of Computing},
volume = {14},
number = {2},
pages = {123-197},
abstract = {Parallel computers have not yet had the expected impact on mainstream computing. Parallelism adds a level of complexity to the programming task that makes it very error-prone. Moreover, a large variety of very different parallel architectures exists. Porting an implementation from one machine to another may require substantial changes. This paper addresses some of these problems by developing a formal basis for the design of parallel programs in the form of a refinement calculus. The calculus allows the stepwise formal derivation of an abstract, low-level implementation from a trusted, high-level specification. The calculus thus helps structuring and documenting the development process. Portability is increased, because the introduction of a machine-dependent feature can be located in the refinement tree. Development efforts above this point in the tree are independent of that feature and are thus reusable. Moreover, the discovery of new, possibly more efficient solutions is facilitated. Last but not least, programs are correct by construction, which obviates the need for difficult debugging. Our programming/specification notation supports fair parallelism, shared-variable and message-passing concurrency, local variables and channels. The calculus rests on a compositional trace semantics that treats shared-variable and message-passing concurrency uniformly. The refinement relation combines a context-sensitive notion of trace inclusion and assumption-commitment reasoning to achieve compositionality. The calculus straddles both concurrency paradigms, that is, a shared-variable program can be refined into a distributed, message-passing program and vice versa.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}

@article{Dingel1998,
title = {Towards a Formal Treatment of Implicit Invocation Using Rely/Guarantee Reasoning},
author = {Juergen Dingel and David Garlan and Somesh Jha and David Notkin},
url = {http://dx.doi.org/10.1007/s001650050011},
doi = {10.1007/s001650050011},
issn = {1433-299X},
year = {1998},
date = {1998-03-01},
journal = {Formal Aspects of Computing},
volume = {10},
number = {3},
pages = {193-213},
abstract = {Implicit invocation [SuN92, GaN91] has become an important architectural style for large-scale system design and evolution. This paper addresses the lack of specification and verification formalisms for such systems. A formal computational model for implicit invocation is presented. We develop a verification framework for implicit invocation that is based on Jones' rely/guarantee reasoning for concurrent systems [Jon83, Stø91]. The application of the framework is illustrated with several examples. The merits and limitations of the rely/guarantee paradigm in the context of implicit invocation systems are also discussed.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}