@conference {4829,
	title = {Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants},
	booktitle = {NASA Formal Methods - 9th International Symposium},
	volume = {10227},
	year = {2017},
	month = {05/2017},
	pages = {194-211},
	publisher = {Springer},
	organization = {Springer},
	address = {Moffett Field, CA, USA},
	abstract = {We propose a method for verifying persistence of nonlinear hybrid systems. Given some system and an initial set of states, the method can guarantee that system trajectories always eventually evolve into some specified target subset of the states of one of the discrete modes of the system, and always remain within this target region. The method also computes a time-bound within which the target region is always reached. The approach combines flowpipe computation with deductive reasoning about invariants and is more general than each technique alone. We illustrate the method with a case study concerning showing that potentially destructive stick-slip oscillations of an oil-well drill eventually die away for a certain choice of drill control parameters. The case study demonstrates how just using flow-pipes or just reasoning about invariants alone can be insufficient. The case study also nicely shows the richness of systems that the method can handle: the case study features a mode with non-polynomial (nonlinear) ODEs and we manage to prove the persistence property with the aid of an automatic prover specifically designed for handling transcendental functions.},
	isbn = {978-3-319-57287-1},
	doi = {10.1007/978-3-319-57288-8_14},
	attachments = {https://archive.isis.vanderbilt.edu/sites/default/files/persistence-safety-nfm-2017.pdf},
	author = {Andrew Sogokon and Paul B. Jackson and Taylor T. Johnson}
}
@conference {4794,
	title = {Decoupling Abstractions of Non-linear Ordinary Differential Equations},
	booktitle = {FM 2016, 21st International Symposium on Formal Methods},
	volume = {9995 Lecture Notes in Computer Science},
	year = {2016},
	month = {11/2016},
	pages = {628-644},
	publisher = {Springer},
	organization = {Springer},
	address = {Limassol, Cyprus},
	abstract = {We investigate decoupling abstractions, by which we seek to simulate (i.e. abstract) a given system of ordinary differential equations (ODEs) by another system that features completely independent (i.e. uncoupled) sub-systems, which can be considered as separate systems in their own right. Beyond a purely mathematical interest as a tool for the qualitative analysis of ODEs, decoupling can be applied to verification problems arising in the fields of control and hybrid systems. Existing verification technology often scales poorly with dimension. Thus, reducing a verification problem to a number of independent verification problems for systems of smaller dimension may enable one to prove properties that are otherwise seen as too difficult. We show an interesting correspondence between Darboux polynomials and decoupling simulating abstractions of systems of polynomial ODEs and give a constructive procedure for automatically computing the latter.},
	keywords = {abstraction, Darboux polynomials, decoupling, Ordinary differential equations, simulation},
	doi = {0.1007/978-3-319-48989-6_38},
	url = {https://link.springer.com/chapter/10.1007/978-3-319-48989-6_38},
	attachments = {https://archive.isis.vanderbilt.edu/sites/default/files/decoupling-abstractions-fm-2016.pdf},
	author = {Andrew Sogokon and Khalil Ghorbal and Taylor T. Johnson}
}
