Publications

Search

Show only items where

Author

Type

Term

Year

Keyword

Export 73 results:

Filters: First Letter Of Last Name is C [Clear All Filters]

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

V

Verification of Neural ODEs with Stochastic Guarantees, Gruenbacher, S., Cyranka J., Lechner M., Smolka S. A., and Grosu R. , Proceedings of AAAI-21, 35th AAAI Conference on Artificial Intelligence, 02/2021, (2021)

On The Verification of Neural ODEs with Stochastic Guarantees, Gruenbacher, Sophie, Hasani Ramin, Lechner Mathias, Cyranka Jacek, Smolka Scott A., and Grosu Radu , (2020)

U

UML-VT: A Formal Verification Environment for UML Activity Diagrams., Daw, Zamira, Mangino John, and Cleaveland Rance , P&D@ MoDELS, (2015)

T

Towards Automated Comprehension and Alignment of Cardiac Models at the System Invariant Level, Huang, Samuel, Diep Madeline, Jang Kuk, Cherry Elizabeth M., Fenton Flavio H., Cleaveland Rance, Lindvall Mikael, Mangharam Rahul, and Porter Adam , CSBio'20: Proceedings of the Eleventh International Conference on Computational Systems-Biology and Bioinformatics, (2020)

Towards Automated Comprehension and Alignment of Cardiac Models at the System Invariant Level, Huang, Samuel, Diep Madeline, Jang Kuk, Cherry Elizabeth M., Fenton Flavio H., Cleaveland Rance, Lindvall Mikael, Mangharam Rahul, and Porter Adam , CSBio'20: Proceedings of the Eleventh International Conference on Computational Systems-Biology and Bioinformatics, (2020)

Timed Automata Benchmark Description, Fontana, Peter, and Cleaveland Rance , arXiv preprint arXiv:2005.13151, (2020)

Temporal-logic query checking over finite data streams, Huang, Samuel, and Cleaveland Rance , International Conference on Formal Methods for Industrial Critical Systems, (2020)

A tableau construction for finite linear-time temporal logic, Huang, Samuel, and Cleaveland Rance , arXiv preprint arXiv:1910.09339, (2019)

S

Swarm Model Checking on the GPU, DeFrancisco, R., Cho S., Ferdman M., and Smolka S. A. , International Journal on Software Tools for Technology Transfer, (2020)

Spatiotemporal correlation uncovers characteristic lengths in cardiac tissue, Loppini, Alessandro, Gizzi Alessio, Cherubini Christian, CHERRY ELIZABETH M., FENTON FLAVIO H., and Filippi Simonetta , Physical Review E, Volume 100, (2019)

Spatiotemporal correlation uncovers characteristic lengths in cardiac tissue, Loppini, Alessandro, Gizzi Alessio, Cherubini Christian, CHERRY ELIZABETH M., FENTON FLAVIO H., and Filippi Simonetta , Physical Review E, Volume 100, (2019)

Single-variable delay-differential equation approximations of the Fitzhugh-Nagumo and Hodgkin-Huxley models, Rameh, Raffael Bechara, CHERRY ELIZABETH M., and Santos Rodrigo Weber dos , Communications in Nonlinear Science and Numerical Simulation, Volume 82, p.105066, (2020)

Simultaneous Quantification of Spatially Discordant Alternans in Voltage and Intracellular Calcium in Langendorff-Perfused Rabbit Hearts and Inconsistencies with Models of Cardiac Action Potentials and Ca Transients, Uzelac, Ilija, Ji Yanyan C., Hornung Daniel, Schröder-Scheteling Johannes, Luther Stefan, Gray Richard A., CHERRY ELIZABETH M., and FENTON FLAVIO H. , Frontiers in Physiology, Volume 8, (2017)

SHARP BOUNDARY ELECTROCARDIAC SIMULATIONS, XUE, SHUAI, LIM HYUNKYUNG, GLIMM JAMES, FENTON FLAVIO H., and CHERRY ELIZABETH M. , Stony Brook, (2016)

(725.88 KB)

Security assurance cases for medical cyber–physical systems, Ray, Arnab, and Cleaveland Rance , IEEE Design & Test, Volume 32, p.56–65, (2015)

Scott Smolka and Me, Cleaveland, Rance , From Reactive Systems to Cyber-Physical Systems, p.1–6, (2019)

R

The role of conductivity discontinuities in design of cardiac defibrillation, Lim, Hyunkyung, Cun Wenjing, Wang Yue, Gray Richard A., and Glimm James , Chaos: An Interdisciplinary Journal of Nonlinear Science, Volume 28, p.013106, (2018)

(3 MB)

(552.91 KB)

The role of conductivity discontinuities in design of cardiac debrillation, LIM, HYUNKYUNG, Cun Wenjing, Gray Richard A., and GLIMM JAMES , (2017)

(1.36 MB)

(552.91 KB)

(2.25 MB)

Real-time interactive simulations of large-scale systems on personal computers and cell phones: Toward patient-specific heart modeling and other applications, Kaboudian, Abouzar, CHERRY ELIZABETH M., and FENTON FLAVIO H. , Science Advances, Volume 5, p.eaav6019, (2019)

Q

Query Checking for Linear Temporal Logic, Huang, Samuel, and Cleaveland Rance , 25 August 2017, (2017)

Quantifying arrhythmic long QT effects of hydroxychloroquine and azithromycin with whole-heart optical mapping and simulations, Uzelac, Ilija, Kaboudian Abouzar, Iravanian Shahriar, Siles-Paredes Jimena G., Gumbart James C., Ashikaga Hiroshi, Bhatia Neal, Gilmour, Jr Robert F., Cherry Elizabeth M., and Fenton Flavio H. , Heart Rhythm O2, 08/2021, Volume 2, Issue 4, (2021)

P

Programming is modeling, Cleaveland, Rance , International Symposium on Leveraging Applications of Formal Methods, (2018)

Process Algebra and Model Checking, Cleaveland, Rance, Roscoe A. W., and Smolka Scott A. , Handbook of Model Checking., p.1149–1195, (2018)

Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans, Islam, Md Ariful, Cleaveland Rance, Fenton Flavio H., Grosu Radu, Jones Paul L., and Smolka Scott A. , Theoretical Computer Science, Volume 765, p.158–169, (2019)

Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans, Islam, Md. Ariful, Cleaveland Rance, FENTON FLAVIO H., Grosu Radu, Jones Paul L., and Smolka Scott A. , Theoretical Computer Science, 02/2018, (2018)

(1.99 MB)

Pages