@booklet {,
	title = {Adversarial Training is Not Ready for Robot Learning},
	year = {2021},
	author = {Mathias Lechner and Ramin Hasani and Radu Grosu and Daniela Rus and Thomas A. Henzinger}
}
@article {,
	title = {Accelerating simulations of cardiac electrical dynamics through a multi-GPU platform and an optimized data structure},
	journal = {Concurrency and Computation: Practice and Experience},
	volume = {32},
	year = {2020},
	month = {03/2020},
	url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&cstart=20\&pagesize=80\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:vDijr-p_gm4C},
	author = {Eduardo C Vasconcellos and Esteban WG Clua and Flavio H Fenton and Marcelo Zamith}
}
@article {,
	title = {Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems},
	journal = {IEEE Access},
	year = {2020},
	author = {F. Shmarov and S. Soudjani and N. Paoletti and E. Bartocci and S. Lin and S. A. Smolka and P. Zuliani}
}
@article {,
	title = {An Algebraic Framework for Runtime Verification},
	journal = {CoRR},
	volume = {abs/1802.03775},
	year = {2018},
	url = {http://arxiv.org/abs/1802.03775},
	author = {Stefan Jaksic and Ezio Bartocci and Radu Grosu and Dejan Nickovic}
}
@conference {,
	title = {Automated Specification Extraction and Analysis with Specstractor},
	booktitle = {Software Engineering and Formal Methods - 16th International Conference, {SEFM} 2018, Held as Part of {STAF} 2018, Toulouse, France, June 27-29, 2018, Proceedings},
	year = {2018},
	doi = {10.1007/978-3-319-92970-5\_3},
	url = {https://doi.org/10.1007/978-3-319-92970-5\_3},
	author = {Christoph Schulze and Rance Cleaveland and Mikael Lindvall}
}
@article {,
	title = {Alternans promotion in cardiac electrophysiology models by delay differential equations},
	journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science},
	volume = {27},
	year = {2017},
	pages = {093915},
	abstract = {<p>Cardiac electrical alternans is a state of alternation between long and short action potentials and is frequently associated with harmful cardiac conditions. Different dynamic mechanisms can give rise to alternans; however, many cardiac models based on ordinary differential equations are not able to reproduce this phenomenon. A previous study showed that alternans can be induced by the introduction of delay differential equations (DDEs) in the formulations of the ion channel gating variables of a canine myocyte model. The present work demonstrates that this technique is not model-specific by successfully promoting alternans using DDEs for five cardiac electrophysiology models that describe different types of myocytes, with varying degrees of complexity. By analyzing results across the different models, we observe two potential requirements for alternans promotion via DDEs for ionic gates: (i) the gate must have a significant influence on the action potential duration and (ii) a delay must significantly impair the gate{\textquoteright}s recovery between consecutive action potentials.</p>
},
	issn = {1054-1500},
	doi = {10.1063/1.4999471},
	url = {http://aip.scitation.org/doi/10.1063/1.4999471},
	author = {Gomes, Johnny M. and dos Santos, Rodrigo Weber and Cherry, Elizabeth M.}
}
@conference {,
	title = {Automated Closed-Loop Model Checking of Implantable Pacemakers using Abstraction Trees},
	booktitle = {Medical Cyber Physical Systems Workshop 2016},
	year = {2016},
	abstract = {<p>Autonomous medical devices such as implantable cardiac pacemakers are capable of diagnosing the patient condition and delivering therapy without human intervention. Their ability to autonomously affect the physiological state of the patient makes them safety-critical. Sufficient evidence for the safety and efficacy of the device software, which makes these autonomous decisions, should be provided before these devices can be released on the market. Formal methods like model checking can provide safety evidence that the devices can safely operate under a large variety of physiological conditions. The challenge is to develop physiological models that are general enough to cover the large variability of human physiology, and also expressive enough to provide physiological contexts to counter-examples returned by the model checker. In this paper, the authors develop a set of physiological abstraction rules that introduce physiological constraints to heart models. By applying these abstraction rules to a initial set of heart models, an abstraction tree is created. The root model covers all possible inputs to a pacemaker and derived models cover inputs from different heart conditions. If a counter-example is returned by the model checker, the abstraction tree is traversed so that the most concrete counter-example(s) with physiological contexts can be returned to the domain experts for validity check. The abstraction tree framework replaces the manual abstraction and refinement framework, which reduced the amount of domain knowledge required to perform closed-loop model checking. It encourages the use of model checking during the development of autonomous medical devices, and identifies safety risks earlier in the design process.</p>
},
	author = {Zhihao Jiang and Houssam Abbas and Pieter J Mosterman and Rahul Mangharam}
}
@article {,
	title = {Abstract Model Repair},
	journal = {Logical Methods in Computer Science},
	volume = {3:11},
	year = {2015},
	author = {G. Chatzieleftheriou and B. Bonakdarpour and P. Katsaros and S. A. Smolka}
}
