@article {,
	title = {Interactive 3D Human Heart Simulations on Segmented Human MRI Hearts},
	year = {2021},
	url = {https://www.cinc.org/2021/Program/accepted/261.pdf},
	author = {John P. Berman and FLAVIO H. FENTON and ELIZABETH M. CHERRY and Tinen Iles and Paul A. Iaizzo and Abouzar Kaboudian}
}
@article {,
	title = {A Network-based Cardiac Electrophysiology Simulator with Realistic Signal Generation and Response to Pacing Maneuvers},
	journal = {Computing in Cardiology},
	year = {2021},
	url = {https://www.cinc.org/2021/Program/accepted/294_Preprint.pdf},
	author = {Shahriar Iravanian and Ilija Uzelac and Abouzar Kaboudian and Jonathan Langberg and Flavio Fenton}
}
@article {,
	title = {Quantifying arrhythmic long QT effects of hydroxychloroquine and azithromycin with whole-heart optical mapping and simulations},
	journal = {Heart Rhythm O2},
	volume = {2},
	year = {2021},
	month = {08/2021},
	url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:Ug5p-4gJ2f0C},
	author = {Ilija Uzelac and Abouzar Kaboudian and Shahriar Iravanian and Jimena G Siles-Paredes and James C Gumbart and Hiroshi Ashikaga and Neal Bhatia and Robert F Gilmour Jr and Elizabeth M Cherry and Flavio H Fenton}
}
@article {,
	title = {Fatal arrhythmias: another reason why doctors remain cautious about chloroquine/hydroxychloroquine for treating COVID-19},
	journal = {Heart Rhythm},
	volume = {17},
	year = {2020},
	month = {09/2020},
	url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:tYavs44e6CUC},
	author = {Ilija Uzelac and Shahriar Iravanian and Hiroshi Ashikaga and Neal K Bhatia and Conner Herndon and Abouzar Kaboudian and James C Gumbart and Elizabeth M Cherry and Flavio H Fenton}
}
@booklet {,
	title = {Lagrangian Reachtubes: The Next Generation},
	year = {2020},
	author = {Sophie Gruenbacher and Jacek Cyranka and Mathias Lechner and Md. Ariful Islam and Scott A. Smolka and Radu Grosu}
}
@conference {,
	title = {Next-Generation Lagrangian Reachtubes},
	booktitle = {Proceedings of CDC 2020, 59th IEEE Conference on Decision and Control},
	year = {2020},
	month = {12/2020},
	author = {S. Gruenbacher and J. Cyranka and M. Lechner and Md. A. Islam and S. A. Smolka and R. Grosu}
}
@conference {,
	title = {Parallel Acceleration on Removal of Optical Mapping Baseline Wandering},
	booktitle = {2019 Computing in Cardiology (CinC)},
	year = {2019},
	month = {09/2019},
	publisher = {IEEE},
	organization = {IEEE},
	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:L7CI7m0gUJcC},
	author = {Ilija Uzelac and Shahriar Iravanian and Flavio H Fenton}
}
@article {,
	title = {Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans},
	journal = {Theoretical Computer Science},
	volume = {765},
	year = {2019},
	pages = {158{\textendash}169},
	author = {Islam, Md Ariful and Cleaveland, Rance and Fenton, Flavio H and Grosu, Radu and Jones, Paul L and Smolka, Scott A}
}
@article {,
	title = {Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans},
	journal = {Theoretical Computer Science},
	year = {2018},
	month = {02/2018},
	abstract = {<p>Using a probabilistic reachability-based approach, we present a multi-parameter bifurcation analysis of electrical alternans in the two-current Mitchell{\textendash}Schaeffer (MS) cardiac-cell model. Electrical alternans is a phenomenon characterized by a variation in successive Action Potential Durations generated by a cardiac cell or tissue. Alternans are known to initiate re-entrant waves and are an important physiological indicator of an impending life-threatening arrhythmia such as ventricular fibrillation. The multi-parameter bifurcation analysis we perform identifies a bifurcation hypersurface in the MS model parameter space, such that a small perturbation to this region results in a transition from highly likely alternans to highly likely non-alternans behavior. Our approach to this problem rests on encoding alternans-like behavior in the MS model as a five-mode, multinomial hybrid automaton. To perform multi-parameter bifurcation analysis of cardiac alternans, we first treat the parameters in question as bounded random variables. We then apply a sophisticated guided-search-based probabilistic reachability analysis to compute a bounded bifurcation region (possibly very tight) that contains the bifurcation hypersurface (BH). Our probabilistic reachability analysis uses a technique that combines a δ-decision procedure with statistical tests. In the process of computing the bifurcation region, we further partition the parameter space into two more regions such that any valuation chosen from one of the regions will either produce alternans or non-alternans behavior with a probability greater than a user-defined threshold.</p>
},
	keywords = {Bifurcation analysis, Cardiac alternans, Cardiac modeling, Formal methods, Hybrid systems, Probabilistic reachability},
	issn = {0304-3975},
	doi = {https://doi.org/10.1016/j.tcs.2018.02.005},
	url = {http://www.sciencedirect.com/science/article/pii/S0304397518300823},
	author = {Md. Ariful Islam and Rance Cleaveland and FLAVIO H. FENTON and Radu Grosu and Paul L. Jones and Scott A. Smolka}
}
@conference {,
	title = {Lagrangian Reachabililty},
	booktitle = {Computer Aided Verification - 29th International Conference, {CAV} 2017 Proceedings, Part {I}},
	year = {2017},
	abstract = {<p>We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools.</p>
},
	doi = {10.1007/978-3-319-63387-9_19},
	author = {Jacek Cyranka and Md. Ariful Islam and Greg Byrne and Paul L. Jones and Scott A. Smolka and Radu Grosu}
}
@conference {,
	title = {Bifurcation Analysis of Cardiac Alternans Using δ -Decidability.},
	booktitle = {CMSB},
	year = {2016},
	publisher = {Springer},
	organization = {Springer},
	keywords = {dblp},
	isbn = {978-3-319-45176-3},
	url = {http://dblp.uni-trier.de/db/conf/cmsb/cmsb2016.html$\#$IslamBKCCFGJS16},
	author = {Islam, Md. Ariful and Byrne, Greg and Kong, Soonho and Clarke, Edmund M. and Cleaveland, Rance and Fenton, Flavio H. and Grosu, Radu and Jones, Paul L. and Smolka, Scott A.},
	editor = {Bartocci, Ezio and Li{\`o}, Pietro and Paoletti, Nicola}
}
@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 = {Model-Order Reduction of Ion Channel Dynamics Using Approximate Bisimulation},
	journal = {Theoretical Computer Science},
	volume = {599C},
	year = {2015},
	month = {09/2015},
	chapter = {34},
	author = {Md. A. Islam and A. Murthy and E. Bartocci and E. M. Cherry and F. H. Fenton and J. Glimm and S. A. Smolka and R. Grosu}
}
