@conference {,
	title = {Collision-Free 3D Flocking Using the Distributed Simplex Architecture},
	booktitle = {Proceedings of ISoLA Extra in Rhodes},
	year = {2021},
	month = {10/2021},
	author = {U. Mehmood and R. Grosu and S. A. Smolka and S. D. Stoller}
}
@article {,
	title = {Control and anticontrol of chaos in fractional-order models of Diabetes, HIV, Dengue, Migraine, Parkinson{\textquoteright}s and Ebola virus diseases},
	journal = {Chaos, Solitons \& Fractals},
	volume = {153},
	year = {2021},
	month = {12/2021},
	url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:hCrLmN-GePgC},
	author = {Manashita Borah and Debanita Das and Antara Gayan and Flavio Fenton and Elizabeth Cherry}
}
@article {,
	title = {Controllability of voltage- and calcium-driven cardiac alternans in a map model},
	journal = {Chaos},
	year = {2021},
	author = {Munoz LM and Ampofo MO and Cherry EM}
}
@article {,
	title = {Closed-loop quantitative verification of rate-adaptive pacemakers},
	journal = {ACM Transactions on Cyber-Physical Systems, to appear},
	year = {2017},
	abstract = {<p>Cardiac pacemakers are electrical devices that treat arrhythmias delivering electrical stimuli to the patient heart {\textbullet} Rate-adaptation: regulation of pacing rate according to patient{\textquoteright}s needs (e.g. increased pacing rate during exercise) {\textbullet} Programming of rate-adaptation parameters depends on many patient-specific factors (age, lifestyle, tolerance to rapid pacing, {\textellipsis}) {\textbullet} Effective personalisation achievable only through extensive exercise testing: intolerable for a cardiac patient {\textbullet} We introduce a data-driven and model-based approach for subjectspecific verification of rate-adaptive pacemakers</p>
},
	author = {Nicola Paoletti and Andrea Patan{\`e} and Marta Kwiatkowska}
}
@article {,
	title = {Collision Avoidance for Mobile Robots with Limited Sensing and Limited Information about Moving Obstacles},
	journal = {Formal Methods in System Design},
	year = {2017},
	month = {01/2017},
	author = {D. Phan and J. Yang and R. Grosu and S. A. Smolka and S. D. Stoller}
}
@article {,
	title = {Corrections to "A Menagerie of Timed Automata"},
	journal = {ACM Comput. Surv.},
	volume = {50},
	year = {2017},
	pages = {42:1{\textendash}42:8},
	keywords = {Timed automata, timed transition systems, transition systems},
	issn = {0360-0300},
	doi = {10.1145/3078809},
	url = {http://doi.acm.org/10.1145/3078809},
	author = {Keiren, Jeroen J. A. and Fontana, Peter and Cleaveland, Rance}
}
@article {,
	title = {The Challenges of High-Confidence Medical Device Software},
	journal = {IEEE Computer January Outlook},
	year = {2016},
	author = {Z. Jiang and H. Abbas and K. Jang and R. Mangharam}
}
@article {,
	title = {Computing Compositional Proofs of Input-to-Output Stability Using SOS Optimization and δ-Decidability},
	journal = {Nonlinear Analysis: Hybrid Systems},
	year = {2016},
	month = {05/2016},
	author = {A. Murthy and Md. A. Islam, and S. A. Smolka and R. Grosu}
}
@conference {,
	title = {Cybercardia project: Modeling, verification and validation of implantable cardiac devices},
	booktitle = {2016 IEEE International Conference on Bioinformatics and Biomedicine (BIBM)},
	year = {2016},
	publisher = {IEEE},
	organization = {IEEE},
	author = {Islam, Md Ariful and Lim, Hyunkyung and Paoletti, Nicola and Abbas, Houssam and Jiang, Zhihao and Cyranka, Jacek and Cleaveland, Rance and Gao, Sicun and Clarke, Edmund and Grosu, Radu and others}
}
@article {,
	title = {Comparing model checkers for timed UML activity diagrams},
	journal = {Science of Computer Programming},
	volume = {111},
	year = {2015},
	pages = {277{\textendash}299},
	author = {Daw, Zamira and Cleaveland, Rance}
}
