The PROSPER Toolkit

The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they may be treated as components. A system incorporating such tools becomes another component that can be embedded in an application. This paper describes the PROSPER Toolkit which enables this. The nature of communication between components is specified in a language-independent way. It is implemented in several common programming languages to allow a wide variety of tools to have access to the toolkit.

Integrating SVC and HOL with the PROSPER Toolkit

We describe an integration of the SVC decision procedure with the HOL theorem prover. This integration was achieved using the PROSPER toolkit. The SVC decision procedure operates on rational numbers, an axiomatic theory for which was provided in HOL. The decision procedure also returns counterexamples and a framework has been devised for handling counterexamples in a HOL setting.

Calcium oscillations

Changes in cellular calcium concentration control a wide range of physiological processes, from the subsecond release of synaptic neurotransmitters, to the regulation of gene expression over months or years. Calcium can also trigger cell death through both apoptosis and necrosis, and so the regulation of cellular calcium concentration must be tightly controlled through the concerted action of pumps, channels and buffers that transport calcium into and out of the cell cytoplasm. A hallmark of cellular calcium signalling is its spatiotemporal complexity: stimulation of cells by a hormone or neurotransmitter leads to oscillations in cytoplasmic calcium concentration that can vary markedly in time course, amplitude, frequency, and spatial range. In this chapter we review some of the biological roles of calcium, the experimental characterisation of complex dynamic changes in calcium concentration, and attempts to explain this complexity using computational models. We consider the "toolkit" of cellular proteins which influence calcium concentration, describe mechanistic models of key elements of the toolkit, and fit these into the framework of whole cell models of calcium oscillations and waves. Finally, we will touch on recent efforts to use stochastic modelling to elucidate elementary calcium signal events, and how these may evolve into global signals.