@article {Simula.sc.934,
	title = {Cardiac Resynchronization: Insight From Experimental and Computational Models},
	journal = {Progress in Biophysics and Molecular Biology},
	volume = {97},
	number = {2-3},
	year = {2008},
	month = {June-July},
	pages = {543-561},
	abstract = {Cardiac resynchronization therapy (CRT) is a promising therapy for heart failure patients with a conduction disturbance, such as left bundle branch block. The aim of CRT is to resynchronize contraction between and within ventricles. However, about 30\% of patients do not respond to this therapy. Therefore, a better understanding is needed for the relation between electrical and mechanical activation. In this paper, we focus on to what extent animal experiments and mathematical models can help in order to understand the pathophysiology of asynchrony to further improve CRT.},
	doi = {10.1016/j.pbiomolbio.2008.02.024},
	author = {Lumens, J. and Vernooy, K. and J. H. {Omens} and L. J. {Mulligan} and Delhaas, T. and Arts, Thomas and Andrew D. {McCulloch} and F. W. {Prinzen}}
}
@misc {Simula.SE.619,
	title = {Experiences From Testing a Radiotherapy Support System With QuickCheck},
	howpublished = {Report No. 5/2008 of the Faculty of Infomatics, Universitat Koblenz-Landau},
	year = {2008},
	note = {This paper was presented at the Second International Conference of Tests and Proofs (TAP 2008), Prato, Italy, April 2008 Editors: Bernhard Beckert and Reiner H{\"a}hnle},
	month = {April},
	abstract = {We present a case study on the use of lightweight formal methods for testing a real-time organ position tracking system used in radiotherapy. Several properties of the system were modeled and verified through automated test cases generated by QuickCheck. QuickCheck was found useful in reducing the complexity inherent to testing medical devices by detecting faults at system level, supporting regression testing, and assisting in the exploration of atypical errors that could later be analyzed and fixed in the system. We suggest that a combination of lightweight formal methods and random test generation, supported by automated simplification of test cases may represent a feasible and cost-effective option in the medical domain; particularly for those projects with high-pace development, a need for proof-based techniques/tools for certification processes, and when the non-deterministic nature of real-time devices demands the exploration identication of heterogeneous fault sources.},
	isbn = {1864-0850},
	author = {Yamashita, Aiko and Bergqvist, Andreas and Arts, Thomas}
}
