% AUTO-GENERATED by src/generate_bibtex_website.py from data/papers.xlsx.
% Do not hand-edit entries here - edit papers.xlsx and regenerate.
% The @STRING author-homepage macros below ARE hand-curated and are
% carried over verbatim on each regeneration.

@STRING{hp_Hoang-DungTran="https://sites.google.com/site/trhoangdung/"}
@STRING{hp_TaylorT.Johnson="http://www.taylortjohnson.com/"}
@STRING{hp_JohnsonTaylorT="http://www.taylortjohnson.com/"}
@STRING{hp_SayanMitra="http://users.crhc.illinois.edu/mitras/"}
@STRING{hp_ParasaraSridharDuggirala="http://www.cs.illinois.edu\~duggira3/"}
@STRING{hp_SairajDhople="http://www.ece.umn.edu\~sdhople/"}
@STRING{hp_SergiyBogomolov="http://www.sergiybogomolov.com/"}
@STRING{hp_AlexandreDonze="http://www.eecs.berkeley.edu\~donze/"}
@STRING{hp_GoranFrehse="https://sites.google.com/site/frehseg/"}
@STRING{hp_RaduGrosu="http://ti.tuwien.ac.at/cps/people/grosu"}
@STRING{hp_AndreasPodelski="http://www.informatik.uni-freiburg.de\~podelski/"}
@STRING{hp_MartinWehrle="http://ai.cs.unibas.ch/people/mwehrle/"}
@STRING{hp_CedricLangbort="http://aerospace.illinois.edu/directory/profile/langbort"}
@STRING{hp_MarcoCaccamo="http://pertsserver.cs.uiuc.edu\~mcaccamo/"}
@STRING{hp_LuiSha="http://publish.illinois.edu/cpsintegrationlab/people/lui-sha/"}
@STRING{hp_StanleyBak="http://stanleybak.com/"}
@STRING{hp_LeonardoBobadilla="http://users.cis.fiu.edu\~jabobadi/"}
@STRING{hp_AmyLaViers="http://www.amylaviers.com"}
@STRING{hp_SebastianFischmeister="https://uwaterloo.ca/embedded-software-group/people-profiles/sebastian-fischmeister"}
@STRING{hp_ChristianSchilling="http://swt.informatik.uni-freiburg.de/staff/christian_schilling"}
@STRING{hp_KhalilGhorbal="http://www.lix.polytechnique.fr\~ghorbal/"}
@STRING{hp_KhazaAnuarulHoque="http://www.uta.edu/faculty/hoqueka/"}
@STRING{hp_OsmanHasan="http://ohasan.seecs.nust.edu.pk/"}
@STRING{hp_WeimingXiang="https://scholar.google.com/citations?user=Vm_7JP8AAAAJ&hl=en"}
@STRING{hp_XiangWeiming="https://scholar.google.com/citations?user=Vm_7JP8AAAAJ&hl=en"}

@inproceedings{brix2023vnncomp,
  title = {The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results},
  author = {Christopher Brix and Stanley Bak and Changliu Liu and Taylor T. Johnson},
  year = {2023},
  publabel = {R12},
  pubtype = {R},
  pdf = "research/brix2023vnncomp.pdf",
}
@inproceedings{sasaki2026saiv,
  title = {n2v: Neural Network Verification in Python (Competition Contribution)},
  author = {Samuel Sasaki and Ben Wooding and Hanchen David Wang and Anne M. Tumlin and Meiyi Ma and Taylor T. Johnson},
  year = {2026},
  month = jul,
  booktitle = {3rd International Symposium on AI Verification (SAIV 2026)},
  publisher = {Springer},
  publabel = {C70},
  pubtype = {C},
  pdf = "research/sasaki2026saiv.pdf",
}
@inproceedings{zhang2026cdc,
  title = {Control Barrier Function Synthesis for Differential-Algebraic Systems},
  author = {Hongchao Zhang and Mohamad Kazma and Ben Wooding and Meiyi Ma and Taylor T. Johnson and Ahmad Taha},
  year = {2026},
  month = dec,
  booktitle = {65th IEEE Conference on Decision and Control (CDC'26), Honolulu, HI, USA},
  publisher = {IEEE},
  publabel = {C75},
  pubtype = {C},
}
@inproceedings{kazma2026cdc,
  title = {Safe Control of Semi-Explicit Differential-Algebraic Systems: Control Barrier Functions with SOS Verification},
  author = {Mohamad Kazma and Hongchao Zhang and Abdallah Alalem Albustami and Ben Wooding and Meiyi Ma and Taylor T. Johnson and Ahmad Taha},
  year = {2026},
  month = dec,
  booktitle = {65th IEEE Conference on Decision and Control (CDC'26), Honolulu, HI, USA},
  publisher = {IEEE},
  publabel = {C74},
  pubtype = {C},
}
@inproceedings{wooding2026cdc,
  title = {Safe Autonomous Takeover for Unknown Descriptor Systems},
  author = {Ben Wooding and Mohamad Kazma and Hongchao Zhang and Ahmad Taha and Meiyi Ma and Taylor T. Johnson},
  year = {2026},
  month = dec,
  booktitle = {65th IEEE Conference on Decision and Control (CDC'26), Honolulu, HI, USA},
  publisher = {IEEE},
  publabel = {C73},
  pubtype = {C},
}
@inproceedings{tumlin2026atva,
  title = {NNV3: Expanding Neural Network Verification to New Architectures and Domains},
  author = {Anne M. Tumlin and Samuel Sasaki and Ben Wooding and Diego Manzanas Lopez and Muhammad Usama Zubair and Navid Hashemi and Hongchao Zhang and Waseem Abbas and Ipek Oguz and Meiyi Ma and Taylor T. Johnson},
  year = {2026},
  month = dec,
  booktitle = {24th International Symposium on Automated Technology for Verification and Analysis (ATVA 2026), Hong Kong},
  publisher = {Springer},
  publabel = {C72},
  pubtype = {C},
}
@inproceedings{guo2026eccv,
  title = {Indelible Backdoors: On the Limits of Post-Training Defenses},
  author = {Jingyi Guo and Dung Thuy Nguyen and Taylor T. Johnson and Kevin Leach},
  year = {2026},
  month = sep,
  booktitle = {European Conference on Computer Vision (ECCV'26)},
  publisher = {Springer},
  publabel = {C71},
  pubtype = {C},
  pdf = "research/guo2026eccv.pdf",
}
@inproceedings{pham2026saiv,
  title = {MetaMoE: Formal Verification of Compositional Robustness and Scalability of Mixture-of-Experts Architecture},
  author = {Quang Pham and Ben Wooding and Luke Nam and Samuel Sasaki and Taylor T. Johnson},
  year = {2026},
  month = jul,
  booktitle = {3rd International Symposium on AI Verification (SAIV 2026)},
  pages = {167--190},
  publisher = {Springer},
  doi = {10.1007/978-3-032-32357-6_8},
  publabel = {C69},
  pubtype = {C},
  dblp = {conf/saiv/PhamWNSJ26},
  s2id = {290967443},
  pdf = "research/pham2026saiv.pdf",
}
@inproceedings{wooding2026saiv,
  title = {A Self-correcting Neuro-symbolic AI Reasoning Framework},
  author = {Ben Wooding and Kiersten Brennan and Anne M. Tumlin and Hongchao Zhang and Taylor T. Johnson},
  year = {2026},
  month = jul,
  booktitle = {3rd International Symposium on AI Verification (SAIV 2026)},
  pages = {191--211},
  publisher = {Springer},
  doi = {10.1007/978-3-032-32357-6_9},
  publabel = {C68},
  pubtype = {C},
  pdf = "research/wooding2026saiv.pdf",
}
@inproceedings{tumlin2026saiv,
  title = {Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features},
  author = {Anne M. Tumlin and Ben Wooding and Zhenxuan Shao and Diego Manzanas Lopez and Tyler Derr and Taylor T. Johnson},
  year = {2026},
  month = jul,
  booktitle = {3rd International Symposium on AI Verification (SAIV 2026)},
  pages = {271--298},
  publisher = {Springer},
  doi = {10.1007/978-3-032-32357-6_13},
  publabel = {C67},
  pubtype = {C},
  dblp = {conf/saiv/TumlinWSLDJ26},
  s2id = {290974965},
  pdf = "research/tumlin2026saiv.pdf",
}
@inproceedings{liu2026icml,
  title = {Modeling Spectral Energy Shifts in Spatio-Temporal Graph Anomaly Detection},
  author = {Yilin Liu and Hongchao Zhang and Ahmad Taha and Taylor T. Johnson and Meiyi Ma},
  year = {2026},
  month = jul,
  booktitle = {43rd International Conference on Machine Learning (ICML'26)},
  url = {https://openreview.net/forum?id=sgNhWbqXfJ},
  publabel = {C66},
  pubtype = {C},
  pdf = "research/liu2026icml.pdf",
}
@inproceedings{robinette2026cvprw_safe,
  title = {MorphoMod: Visible Watermark Removal with Morphological Dilation},
  author = {Preston K. Robinette and Taylor T. Johnson},
  year = {2026},
  month = jun,
  booktitle = {SAFE: Synthetic \& Adversarial ForEnsics Workshop at the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR 2026)},
  doi = {10.48550/arXiv.2502.02676},
  publabel = {W34},
  pubtype = {W},
  arxiv = {2502.02676},
  pdf = "research/robinette2026cvprw_safe.pdf",
}
@inproceedings{potteiger2026neus,
  title = {Reward Shaping and Action Masking for Compositional Tasks using Behavior Trees and LLMs},
  author = {Nicholas Potteiger and Ankita Samaddar and Taylor T. Johnson and Xenofon D. Koutsoukos},
  year = {2026},
  booktitle = {3rd International Conference on Neuro-symbolic Systems (NeuS'26)},
  publisher = {PMLR},
  keywords = {reward shaping, action masking, behavior trees, LLMs, compositional reinforcement learning, neurosymbolic},
  publabel = {C65},
  pubtype = {C},
  dblp = {journals/corr/abs-2605-05795},
  pdf = "research/potteiger2026neus.pdf",
}
@inproceedings{wooding2026neus,
  title = {k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics},
  author = {Ben Wooding and Hongchao Zhang and Taylor T. Johnson and Abolfazl Lavaei},
  year = {2026},
  booktitle = {3rd International Conference on Neuro-symbolic Systems (NeuS'26)},
  publisher = {PMLR},
  keywords = {barrier certificates, neural networks, k-induction, nonlinear systems, safety verification, neurosymbolic},
  publabel = {C64},
  pubtype = {C},
  dblp = {journals/corr/abs-2605-20108},
  pdf = "research/wooding2026neus.pdf",
}
@incollection{dubey2026neurosymbolic,
  title = {Toward Assured Autonomy Using Neurosymbolic Components and Systems},
  author = {Abhishek Dubey and Taylor T. Johnson and Xenofon Koutsoukos and Baiting Luo and Diego Manzanas Lopez and Miklos Maroti and Ayan Mukhopadhyay and Nicholas Potteiger and Serena Serbinowska and Daniel Stojcsics and Yunuo Zhang and Gabor Karsai},
  year = {2026},
  booktitle = {Neurosymbolic AI (Wiley book, edited by G. Karsai et al.), Chapter 4},
  pages = {89--118},
  publisher = {Wiley},
  doi = {10.1002/9781394302406.ch04},
  url = {https://onlinelibrary.wiley.com/doi/abs/10.1002/9781394302406.ch04},
  keywords = {neurosymbolic, assured autonomy, cyber-physical systems, formal verification, DARPA ANSR},
  publabel = {BC4},
  pubtype = {BC},
}
@incollection{johnson2026letstalk,
  title = {Let's Talk AI with Computer Science Expert Taylor T. Johnson},
  author = {Taylor T. Johnson and Barbara Steffen},
  year = {2026},
  month = oct,
  booktitle = {Let's Talk AI, Lecture Notes in Computer Science (LNCS)},
  volume = {15000},
  pages = {130--137},
  publisher = {Springer},
  doi = {10.1007/978-3-032-09008-9_15},
  url = {https://link.springer.com/chapter/10.1007/978-3-032-09008-9_15},
  keywords = {AI, formal verification, neural networks, trust},
  publabel = {BC3},
  pubtype = {BC},
}
@article{wang2026jair,
  title = {Towards Verified and Targeted Explanations through Formal Methods},
  author = {Hanchen David Wang and Diego Manzanas Lopez and Preston K. Robinette and Ipek Oguz and Taylor T. Johnson and Meiyi Ma},
  year = {2026},
  month = jul,
  journal = {Journal of Artificial Intelligence Research},
  volume = {86},
  publisher = {AAAI Press},
  doi = {10.1613/jair.1.20924},
  publabel = {J33},
  pubtype = {J},
  dblp = {journals/corr/abs-2604-14209},
  pdf = "research/wang2026jair.pdf",
}
@article{zubair2026jair,
  title = {ModelStar: Reachability Analysis-based Safety Verification of Neural Networks Against Model Perturbations},
  author = {Muhammad Usama Zubair and Taylor T. Johnson and Kanad Basu and Waseem Abbas},
  year = {2026},
  month = apr,
  journal = {Journal of Artificial Intelligence Research},
  volume = {85},
  publisher = {AAAI Press},
  doi = {10.1613/jair.1.18922},
  url = {https://doi.org/10.1613/jair.1.18922},
  publabel = {J32},
  pubtype = {J},
  dblp = {journals/jair/ZubairJBA26},
  pdf = "research/zubair2026jair.pdf",
}
@inproceedings{nguyen2026wacv,
  title = {SUGAR: A Sweeter Spot for Generative Unlearning of Many Identities},
  author = {Dung Thuy Nguyen and Quang Nguyen and Preston K. Robinette and Eli Jiang and Taylor T. Johnson and Kevin Leach},
  year = {2026},
  month = mar,
  booktitle = {IEEE/CVF Winter Conference on Applications of Computer Vision (WACV'26)},
  publabel = {C60},
  pubtype = {C},
  dblp = {conf/wacv/NguyenNRJJL26},
  pdf = "research/nguyen2026wacv.pdf",
}
@inproceedings{robinette2026eacl,
  title = {We Are What We Repeatedly Do: Improving Long Context Instruction Following},
  author = {Preston K. Robinette and Andrew Hard and Swaroop Ramaswamy and Ehsan Amid and Rajiv Mathews and Taylor T. Johnson},
  year = {2026},
  month = apr,
  booktitle = {Findings of the 23rd Conference of the European Chapter of the Association for Computational Linguistics (EACL'26)},
  publabel = {C61},
  pubtype = {C},
  dblp = {conf/eacl/RobinetteHRAMJ26},
}
@inproceedings{an2026iccps,
  title = {LogiEx: Integrating Formal Logic and LLMs for Explainable Transit Planning},
  author = {Ziyan An and Xia Wang and Hendrik Baier and Zirong Chen and Abhishek Dubey and Ayan Mukhopadhyay and Taylor T. Johnson and Jonathan Sprinkle and Meiyi Ma},
  year = {2026},
  month = may,
  booktitle = {17th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS'26)},
  publabel = {C63},
  pubtype = {C},
}
@inproceedings{nguyen2026iccps,
  title = {LOGSAFE: Logic-Guided Verification for Trustworthy Federated Time-Series Learning},
  author = {Dung Thuy Nguyen and Ziyan An and Taylor T. Johnson and Meiyi Ma and Kevin Leach},
  year = {2026},
  month = may,
  booktitle = {17th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS'26)},
  publabel = {C62},
  pubtype = {C},
  pdf = "research/nguyen2026iccps.pdf",
}
@inproceedings{neider2023aisola,
  title = {Track C1: Safety Verification of Deep Neural Networks (DNNs)},
  author = {Daniel Neider and Taylor T. Johnson},
  year = {2023},
  month = oct,
  booktitle = {1st International Conference on Bridging the Gap between AI and Reality (AISoLA'23)},
  pages = {217--224},
  publisher = {Springer},
  doi = {10.1007/978-3-031-46002-9_12},
  keywords = {Formal Verification, Formal Methods, Neural Networks,Safety of Autonomy},
  publabel = {E2},
  pubtype = {E},
  dblp = {conf/vecos/NeiderJ23},
  s2id = {266845072},
  pdf = "research/neider2023aisola.pdf",
}
@inproceedings{hashemi2025neurips,
  title = {Scaling Data-Driven Probabilistic Robustness Analysis for Semantic Segmentation Neural Networks},
  author = {Navid Hashemi and Samuel Sasaki and Ipek Oguz and Meiyi Ma and Taylor T. Johnson},
  year = {2025},
  month = dec,
  booktitle = {39th Annual Conference on Neural Information Processing Systems (NeurIPS'25)},
  publabel = {C59},
  pubtype = {C},
  pdf = "research/hashemi2025neurips.pdf",
}
@inproceedings{robinette2025esorics,
  title = {Trigger-Based Fragile Model Watermarking for Image Transformation Networks},
  author = {Preston K. Robinette and Dung Thuy Nguyen and Samuel Sasaki and Taylor T. Johnson},
  year = {2025},
  month = sep,
  booktitle = {30th European Symposium on Research in Computer Security (ESORICS'25)},
  pages = {346--365},
  publisher = {Springer},
  doi = {10.1007/978-3-032-07884-1_18},
  publabel = {C58},
  pubtype = {C},
  dblp = {conf/esorics/RobinetteNSJ25},
  s2id = {282594823},
  pdf = "research/robinette2025esorics.pdf",
}
@inproceedings{potteiger2025neus,
  title = {Real-Time Reachability for Neurosymbolic Reinforcement Learning based Safe Autonomous Navigation},
  author = {Nicholas Potteiger and Diego Manzanas Lopez and Taylor T. Johnson and Xenofon Koutsoukos},
  year = {2025},
  month = may,
  booktitle = {2nd International Conference on Neuro-symbolic Systems (NeuS'25)},
  publisher = {PMLR},
  keywords = {reinforcement learning, real-time reachability, neurosymbolic learning},
  publabel = {C56},
  pubtype = {C},
  pdf = "research/potteiger2025neus.pdf",
}
@inproceedings{sasaki2025neus,
  title = {Neurosymbolic Finite and Pushdown Automata: Improved Multimodal Reasoning versus Vision Language Models (VLMs)},
  author = {Samuel Sasaki and Diego Manzanas Lopez and Taylor T. Johnson},
  year = {2025},
  month = may,
  booktitle = {2nd International Conference on Neuro-symbolic Systems (NeuS'25)},
  publisher = {PMLR},
  keywords = {neurosymbolic artificial intelligence, automata, multimodal reasoning},
  publabel = {C55},
  pubtype = {C},
  pdf = "research/sasaki2025neus.pdf",
}
@inproceedings{serbinowska2025neus,
  title = {Neuro-Symbolic Behavior Trees and Their Verification},
  author = {Serena Serbinowska and Diego Manzanas Lopez and Dung Thuy Nguyen and Taylor T. Johnson},
  year = {2025},
  month = may,
  booktitle = {2nd International Conference on Neuro-symbolic Systems (NeuS'25)},
  publisher = {PMLR},
  keywords = {behavior trees, neurosymbolic systems, verification},
  publabel = {C54},
  pubtype = {C},
  pdf = "research/serbinowska2025neus.pdf",
}
@inproceedings{nguyen2025icdcs,
  title = {PARDON: Privacy-Aware and Robust Federated Domain Generalization},
  author = {Dung Thuy Nguyen and Taylor T. Johnson and Kevin Leach},
  year = {2025},
  month = jul,
  booktitle = {45th IEEE International Conference on Distributed Computing Systems (ICDCS'25)},
  pages = {703--713},
  publisher = {IEEE},
  doi = {10.1109/icdcs63083.2025.00074},
  keywords = {machine learning, federated learning, privacy},
  publabel = {C57},
  pubtype = {C},
  dblp = {conf/icdcs/NguyenJL25},
  pdf = "research/nguyen2025icdcs.pdf",
}
@inproceedings{bao2025iccps,
  title = {Uncertainty Quantification for Physics-Informed Traffic Graph Networks},
  author = {Tianshu Bao and Xiaoou Liu and Meiyi Ma and Taylor T. Johnson and Hua Wei},
  year = {2025},
  month = may,
  booktitle = {16th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS'25)},
  pages = {1--10},
  publisher = {ACM/IEEE},
  doi = {10.1145/3716550.3722023},
  keywords = {uncertainty quantification, physics-based machine learning, traffic forecasting},
  publabel = {C53},
  pubtype = {C},
  dblp = {conf/iccps/BaoLMJ025},
  pdf = "research/bao2025iccps.pdf",
}
@inproceedings{yang2025mai,
  title = {Metacognition with Neural Network Verification and Repair using Veritex},
  author = {Xiaodong Yang and Tomoya Yamaguchi and Bardh Hoxha and Danil Prokhorov and Taylor T. Johnson},
  year = {2025},
  month = feb,
  booktitle = {Metacognitive Artificial Intelligence},
  pages = {212--228},
  publisher = {Cambridge University Press},
  doi = {10.1017/9781009522472.019},
  keywords = {neural network verification, neural network repair, metacognitive AI},
  publabel = {BC2},
  pubtype = {BC},
}
@inproceedings{sasaki2025formalise,
  title = {Robustness Verification of Video Classification Neural Networks},
  author = {Samuel Sasaki and Preston K. Robinette and Diego Manzanas Lopez and Taylor T. Johnson},
  year = {2025},
  month = may,
  booktitle = {13th International Conference on Formal Methods in Software Engineering (FormaliSE'25)},
  pages = {22--33},
  publisher = {ACM},
  doi = {10.1109/FormaliSE66629.2025.00009},
  keywords = {neural network verification, video classification, formal verification},
  publabel = {C52},
  pubtype = {C},
  dblp = {conf/icse-formalise/SasakiLRJ25},
  pdf = "research/sasaki2025formalise.pdf",
}
@inproceedings{cordeiro2025esop,
  title = {Neural Network Verification is a Programming Language Challenge (Fresh Perspectives)},
  author = {Lucas Cordeiro and Matthew Daggitt and Julien Girard-Satabin and Omri Isac and Taylor T. Johnson and Guy Katz and Ekaterina Komendantskaya and Augustin Lemesle and Edoardo Manino and Artjoms Sinkarovs and Haoze Wu},
  year = {2025},
  month = may,
  booktitle = {34th European Symposium on Programming (ESOP'25)},
  pages = {206--235},
  publisher = {Springer},
  doi = {10.1007/978-3-031-91118-7_9},
  keywords = {programming languages, formal verification, neural networks},
  publabel = {C51},
  pubtype = {C},
  pdf = "research/cordeiro2025esop.pdf",
}
@misc{andreasen2024sc_poster,
  title = {Parallel Verification of Neural Networks Applied to Medical Imaging (Research Poster)},
  author = {Jonathan Andreasen and Diego Manzanas Lopez and Taylor T. Johnson and Yatis Dodia},
  year = {2024},
  month = nov,
  howpublished = {36th International Conference for High Performance Computing, Networking, Storage, and Analysis / Supercomputing Conference (SC'24)},
  note = {36th International Conference for High Performance Computing, Networking, Storage, and Analysis / Supercomputing Conference (SC'24)},
  publisher = {ACM},
  keywords = {medical imaging, neural network verification, high-performance computing},
  publabel = {D12},
  pubtype = {D},
}
@inproceedings{nguyen2025ndss,
  title = {PBP: Post-training Backdoor Purification for Malware Classifiers},
  author = {Dung Thuy Nguyen and Ngoc N. Tran and Taylor T. Johnson and Kevin Leach},
  year = {2025},
  month = feb,
  booktitle = {32nd Network and Distributed System Security Symposium (NDSS'25)},
  publisher = {Internet Society},
  doi = {10.14722/ndss.2025.240603},
  keywords = {malware, purification, machine learning},
  publabel = {C50},
  pubtype = {C},
  dblp = {conf/ndss/NguyenTJL25},
  pdf = "research/nguyen2025ndss.pdf",
}
@inproceedings{abate2024toolympics,
  title = {The ARCH-COMP Friendly Verification Competition for Continuous and Hybrid Systems},
  author = {Alessandro Abate and Matthias Althoff and Lei Bu and Gidon Ernst and Goran Frehse and Luca Geretti and Taylor T. Johnson and Claudio Menghi and Stefan Mitsch and Stefan Schupp and Sadegh Soudjani},
  year = {2024},
  month = oct,
  booktitle = {TOOLympics Challenge 2023 and TOOLympics 2024},
  volume = {14550},
  pages = {1--37},
  publisher = {Springer},
  doi = {10.1007/978-3-031-67695-6_1},
  keywords = {formal verification, hybrid systems, competition},
  publabel = {OC18},
  pubtype = {OC},
  dblp = {conf/toolympics/AbateABEFGJMMSS23},
  s2id = {278668440},
  pdf = "research/abate2024toolympics.pdf",
}
@inproceedings{serbinowska2024fmas_rv,
  title = {Verification of Behavior Trees with Contingency Monitors},
  author = {Serena S. Serbinowska and Nicholas Potteiger and Anne M. Tumlin and Taylor T. Johnson},
  year = {2024},
  month = nov,
  booktitle = {6th International Workshop on Formal Methods for Autonomous Systems (FMAS'24)},
  volume = {411},
  pages = {56--72},
  publisher = {EPTCS},
  doi = {10.4204/EPTCS.411.4},
  keywords = {runtime verification, behavior trees, formal verification},
  publabel = {W30},
  pubtype = {W},
  arxiv = {2411.14162},
  dblp = {journals/corr/abs-2411-14162},
  s2id = {274165812},
  pdf = "research/serbinowska2024fmas_rv.pdf",
}
@inproceedings{serbinowska2024fmas_sbt,
  title = {Formalizing Stateful Behavior Trees},
  author = {Serena S. Serbinowska and Preston K. Robinette and Gabor Karsai and Taylor T. Johnson},
  year = {2024},
  month = nov,
  booktitle = {6th International Workshop on Formal Methods for Autonomous Systems (FMAS'24)},
  volume = {411},
  pages = {201--218},
  publisher = {EPTCS},
  doi = {10.4204/EPTCS.411.14},
  keywords = {behavior trees, syntax and semantics, formal verification},
  publabel = {W31},
  pubtype = {W},
  arxiv = {2411.14165},
  dblp = {journals/corr/abs-2411-14165},
  s2id = {274165889},
  pdf = "research/serbinowska2024fmas_sbt.pdf",
}
@inproceedings{tumlin2024icaif,
  title = {FairNNV: The Neural Network Verification Tool For Certifying Fairness},
  author = {Anne M. Tumlin and Diego Manzanas Lopez and Preston K. Robinette and Yuying Zhao and Tyler Derr and Taylor T. Johnson},
  year = {2024},
  month = nov,
  booktitle = {5th ACM International Conference on AI in Finance (ICAIF'24)},
  pages = {36--44},
  publisher = {ACM},
  doi = {10.1145/3677052.3698677},
  keywords = {Fairness, Formal Verification, Neural Networks},
  publabel = {C49},
  pubtype = {C},
  dblp = {conf/icaif/TumlinLRZDJ24},
  s2id = {274072185},
  pdf = "research/tumlin2024icaif.pdf",
}
@inproceedings{robinette2024ecai,
  title = {Sanitizing Hidden Information with Diffusion Models},
  author = {Preston K. Robinette and Daniel Moyer and Taylor T. Johnson},
  year = {2024},
  month = oct,
  booktitle = {27th European Conference on Artificial Intelligence (ECAI'24)},
  publisher = {IOS Press},
  doi = {10.3233/FAIA240562},
  keywords = {machine learning, diffusion models, security},
  publabel = {C48},
  pubtype = {C},
  dblp = {conf/ecai/RobinetteMJ24},
  s2id = {273589573},
  pdf = "research/robinette2024ecai.pdf",
}
@inproceedings{bao2024ecml_pkdd,
  title = {Spatial-Temporal PDE Networks for Traffic Flow Forecasting},
  author = {Tianshu Bao and Hua Wei and Junyi Ji and Daniel Work and Taylor T. Johnson},
  year = {2024},
  month = sep,
  booktitle = {European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases (ECML-PKDD'24), Applied Data Science Track},
  pages = {166--182},
  publisher = {Springer},
  doi = {10.1007/978-3-031-70381-2_11},
  keywords = {physics-based machine learning},
  publabel = {C47},
  pubtype = {C},
  dblp = {conf/pkdd/BaoWJWJ24},
  s2id = {272554741},
  pdf = "research/bao2024ecml_pkdd.pdf",
}
@inproceedings{lopez2024archcomp_ainncs,
  title = {ARCH-COMP24 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants},
  author = {Diego Manzanas Lopez and Matthias Althoff and Luis Benet and Clemens Blab and Marcelo Forets and Yuhao Jia and Taylor T. Johnson and Manuel Kranzl and Tobias Ladner and Lukas Linauer and Philipp Neubauer and Sophie Neubauer and Christian Schilling and Huan Zhang and Xiangru Zhong},
  year = {2024},
  month = oct,
  booktitle = {EPiC Series in Computing 103, 11th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH'24)},
  volume = {103},
  pages = {64--121},
  publisher = {EasyChair},
  doi = {10.29007/mxld},
  keywords = {formal verification, Neural Network Control Systems, Neural Network Verification, neural networks, verification},
  publabel = {OW14},
  pubtype = {OW},
}
@inproceedings{bao2024ijcai,
  title = {Transfer Learning Using Inaccurate Physics Rule for Streamflow Prediction},
  author = {Tianshu Bao and Taylor T. Johnson and Xiaowei Jia},
  year = {2024},
  month = aug,
  booktitle = {33rd International Joint Conference on Artificial Intelligence (IJCAI'24), AI for Good Track},
  pages = {7170--7178},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  doi = {10.24963/ijcai.2024/793},
  keywords = {physics-based machine learning},
  publabel = {C46},
  pubtype = {C},
  dblp = {conf/ijcai/BaoJJ24},
  pdf = "research/bao2024ijcai.pdf",
}
@inproceedings{johnson2024dsn_tutorial,
  title = {Tutorial: Safe, Secure, and Trustworthy Artificial Intelligence (AI) via Formal Verification of Neural Networks and Autonomous Cyber-Physical Systems (CPS) with NNV},
  author = {Taylor T. Johnson and Hoang-Dung Tran and Diego Manzanas Lopez},
  year = {2024},
  month = jun,
  booktitle = {54th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN'24)},
  pages = {65--66},
  publisher = {IEEE/IFIP},
  doi = {10.1109/DSN-S60304.2024.00027},
  keywords = {tutorial,trustworthy AI,verification},
  publabel = {D11},
  pubtype = {D},
  dblp = {conf/dsn/JohnsonLT24},
  s2id = {272219746},
  pdf = "research/johnson2024dsn_tutorial.pdf",
}
@inproceedings{an2024aaai,
  title = {Formal Logic Enabled Personalized Federated Learning Through Property Inference},
  author = {Ziyan An and Taylor T. Johnson and Meiyi Ma},
  year = {2024},
  month = feb,
  booktitle = {38th AAAI Conference on Artificial Intelligence (AAAI'24)},
  volume = {38},
  pages = {10882--10890},
  publisher = {AAAI},
  doi = {10.1609/aaai.v38i10.28962},
  keywords = {federated learning,neurosymbolic learning,temporal logic},
  publabel = {C44},
  pubtype = {C},
  dblp = {conf/aaai/AnJM24},
  pdf = "research/an2024aaai.pdf",
}
@inproceedings{robinette2024formalise,
  title = {Case Study: Neural Network Malware Detection Verification for Feature and Image Datasets},
  author = {Preston K. Robinette and Diego Manzanas Lopez and Serena Serbinowska and Kevin Leach and Taylor T. Johnson},
  year = {2024},
  month = apr,
  booktitle = {12th International Conference on Formal Methods in Software Engineering (FormaliSE'24)},
  pages = {127--137},
  publisher = {ACM},
  doi = {10.1145/3644033.3644372},
  keywords = {machine learning, security, neural network verification},
  publabel = {C45},
  pubtype = {C},
  dblp = {conf/icse-formalise/RobinetteLSLJ24},
  pdf = "research/robinette2024formalise.pdf",
}
@inproceedings{lopez2023archcomp_ainncs,
  title = {ARCH-COMP23 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants},
  author = {Diego Manzanas Lopez and Matthias Althoff and Marcelo Forets and Taylor T. Johnson and Tobias Ladner and Christian Schilling},
  year = {2023},
  month = oct,
  booktitle = {EPiC Series in Computing 96, 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH'23)},
  volume = {96},
  pages = {89--51},
  publisher = {EasyChair},
  doi = {10.29007/x38n},
  keywords = {formal verification, Neural Network Control Systems, Neural Network Verification, neural networks, verification},
  publabel = {OW13},
  pubtype = {OW},
  dblp = {conf/arch/LopezAFJL023},
  pdf = "research/lopez2023archcomp_ainncs.pdf",
}
@inproceedings{johnson2023archcomp,
  title = {ARCH-COMP23 Repeatability Evaluation Report},
  author = {Taylor T. Johnson},
  year = {2023},
  month = oct,
  booktitle = {EPiC Series in Computing 96, 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH'23)},
  volume = {96},
  pages = {189--181},
  publisher = {EasyChair},
  doi = {10.29007/q313},
  keywords = {Artifact Evaluation, formal methods, hybrid systems, Repeatability Evaluation, verification},
  publabel = {OW12},
  pubtype = {OW},
  dblp = {conf/arch/Johnson23},
  s2id = {264318865},
  pdf = "research/johnson2023archcomp.pdf",
}
@inproceedings{bogomolov2023fmas,
  title = {Online Reachability Analysis and Space Convexification for Autonomous Racing},
  author = {Sergiy Bogomolov and Taylor T. Johnson and Diego Manzanas Lopez and Patrick Musau and Paulius Stankaitis},
  year = {2023},
  month = nov,
  booktitle = {5th International Workshop on Formal Methods for Autonomous Systems (FMAS'23)},
  volume = {395},
  pages = {95--112},
  publisher = {EPTCS},
  doi = {10.4204/EPTCS.395.7},
  keywords = {reachability, verification},
  publabel = {W28},
  pubtype = {W},
  arxiv = {2311.09781},
  dblp = {journals/corr/abs-2311-09781},
  s2id = {265220701},
  pdf = "research/bogomolov2023fmas.pdf",
}
@inproceedings{pal2023fmas,
  title = {Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach},
  author = {Neelanjana Pal and Taylor T. Johnson},
  year = {2023},
  month = nov,
  booktitle = {5th International Workshop on Formal Methods for Autonomous Systems (FMAS'23)},
  volume = {395},
  pages = {162--179},
  publisher = {EPTCS},
  doi = {10.4204/EPTCS.395.12},
  keywords = {formal verification,lstm,robustness},
  publabel = {W29},
  pubtype = {W},
  arxiv = {2311.12130},
  dblp = {journals/corr/abs-2311-12130},
  s2id = {265249004},
  pdf = "research/pal2023fmas.pdf",
}
@inproceedings{robinette2023aisola,
  title = {Benchmark: neural network malware classification},
  author = {Preston K. Robinette and Diego Manzanas Lopez and Taylor T. Johnson},
  year = {2023},
  month = oct,
  booktitle = {1st International Conference on Bridging the Gap between AI and Reality (AISoLA'23)},
  pages = {291--298},
  publisher = {Springer},
  doi = {10.1007/978-3-031-46002-9_17},
  keywords = {malware,verification,benchmark},
  publabel = {OC16},
  pubtype = {OC},
  dblp = {conf/vecos/RobinetteLJ23},
  s2id = {266845222},
  pdf = "research/robinette2023aisola.pdf",
}
@inproceedings{pal2023aisola,
  title = {Benchmark: formal verification of semantic segmentation neural networks},
  author = {Neelanjana Pal and Seojin Lee and Taylor T. Johnson},
  year = {2023},
  month = oct,
  booktitle = {1st International Conference on Bridging the Gap between AI and Reality (AISoLA'23)},
  pages = {311--330},
  publisher = {Springer},
  doi = {10.1007/978-3-031-46002-9_20},
  keywords = {Semantic Segmentation,Adversarial Attack,Benchmark,Reachability,Robustness},
  publabel = {OC17},
  pubtype = {OC},
  dblp = {conf/vecos/PalLJ23},
  pdf = "research/pal2023aisola.pdf",
}
@inproceedings{lopez2023aisola,
  title = {Empirical analysis of benchmark generation for the verification of neural network image classifiers},
  author = {Diego Manzanas Lopez and Taylor T. Johnson},
  year = {2023},
  month = oct,
  booktitle = {1st International Conference on Bridging the Gap between AI and Reality (AISoLA'23)},
  pages = {331--347},
  publisher = {Springer},
  doi = {10.1007/978-3-031-46002-9_21},
  keywords = {Formal Verification,Medical Imaging,Deep Learning,Reachability Analysis},
  publabel = {OC15},
  pubtype = {OC},
  dblp = {conf/vecos/LopezJ23},
  pdf = "research/lopez2023aisola.pdf",
}
@inproceedings{an2023rv,
  title = {Runtime Monitoring of Accidents in Driving Recordings with Multi-Type Logic in Empirical Models},
  author = {Ziyan An and Xia Wang and Taylor T. Johnson and Jonathan Sprinkle and Meiyi Ma},
  year = {2023},
  month = oct,
  booktitle = {23rd International Conference on Runtime Verification (RV'23)},
  pages = {376--388},
  publisher = {Springer},
  doi = {10.1007/978-3-031-44267-4_21},
  keywords = {runtime verification, cyber-physical systems},
  publabel = {C43},
  pubtype = {C},
  dblp = {conf/rv/AnWJSM23},
  pdf = "research/an2023rv.pdf",
}
@inproceedings{tran2023iavvc_tutorial,
  title = {Tutorial: Verification and Validation of Neural Networks in Automated Vehicles using the Neural Network Verification (NNV) Tool},
  author = {Hoang-Dung Tran and Diego Manzanas Lopez and Taylor T. Johnson},
  year = {2023},
  month = oct,
  booktitle = {IEEE International Automated Vehicle Validation Conference (IAVVC'23)},
  publisher = {IEEE},
  publabel = {D10},
  pubtype = {D},
}
@inproceedings{robinette2023ecai,
  title = {SUDS: Sanitizing Universal and Dependent Steganography},
  author = {Preston K. Robinette and Taylor T. Johnson and David Wang and Nishan Shehadeh and Daniel C. Moyer},
  year = {2023},
  month = oct,
  booktitle = {26th European Conference on Artificial Intelligence (ECAI'23)},
  publisher = {IOS Press},
  doi = {10.3233/FAIA230489},
  keywords = {steganography,neural networks,sanitization},
  publabel = {C42},
  pubtype = {C},
  dblp = {conf/ecai/RobinetteWSMJ23},
  pdf = "research/robinette2023ecai.pdf",
}
@inproceedings{pal2023fmics,
  title = {Robustness verification of deep neural networks using star-based reachability analysis with variable-length time series input},
  author = {Neelanjana Pal and Diego Manzanas Lopez and Taylor T. Johnson},
  year = {2023},
  month = sep,
  booktitle = {ERCIM Working Group 28th International Conference on Formal Methods for Industrial Critical Systems (FMICS'23)},
  pages = {170--188},
  publisher = {Springer},
  doi = {10.1007/978-3-031-43681-9_10},
  keywords = {predictive maintenance,neural network verification,time-series},
  publabel = {C41},
  pubtype = {C},
  dblp = {conf/fmics/PalLJ23},
  pdf = "research/pal2023fmics.pdf",
}
@inproceedings{tran2023emsoft_tutorial,
  title = {Tutorial: Neural Network and Autonomous Cyber-Physical Systems Formal Verification for Trustworthy AI and Safe Autonomy},
  author = {Hoang-Dung Tran and Diego Manzanas Lopez and Taylor T. Johnson},
  year = {2023},
  month = sep,
  booktitle = {International Conference on Embedded Software (EMSOFT'23)},
  pages = {1--2},
  publisher = {ACM},
  doi = {10.1145/3607890.3608454},
  keywords = {tutorial,trustworthy AI,verification},
  publabel = {D9},
  pubtype = {D},
  dblp = {conf/emsoft/TranLJ23},
  pdf = "research/tran2023emsoft_tutorial.pdf",
}
@inproceedings{lopez2023cav,
  title = {NNV 2.0: The Neural Network Verification Tool},
  author = {Diego Manzanas Lopez and Sung Woo Choi and Hoang-Dung Tran and Taylor T. Johnson},
  year = {2023},
  month = jul,
  booktitle = {35th International Conference on Computer Aided Verification (CAV'23)},
  publisher = {Springer},
  doi = {10.1007/978-3-031-37703-7_19},
  keywords = {neural networks, cyber-physical systems,verification,tool},
  publabel = {C40},
  pubtype = {C},
  dblp = {conf/cav/LopezCTJ23},
  pdf = "research/lopez2023cav.pdf",
}
@inproceedings{hamilton2023smcit,
  title = {Ablation Study of How Run Time Assurance Impacts the Training and Performance of Reinforcement Learning Agents},
  author = {Nathaniel Hamilton and Kyle Dunlap and Taylor T. Johnson and Kerianne L. Hobbs},
  year = {2023},
  month = jul,
  booktitle = {IEEE 9th International Conference on Space Mission Challenges for Information Technology (SMC-IT'23)},
  publisher = {IEEE},
  doi = {10.1109/smc-it56444.2023.00014},
  publabel = {C39},
  pubtype = {C},
  arxiv = {2207.04117},
  dblp = {journals/corr/abs-2207-04117},
  s2id = {250425880},
  pdf = "research/hamilton2023smcit.pdf",
}
@inproceedings{robinette2023iccps,
  title = {Self-Preserving Genetic Algorithms for Safe Learning in Discrete Action Spaces},
  author = {Preston K. Robinette and Nathaniel Hamilton and Taylor T. Johnson},
  year = {2023},
  month = may,
  booktitle = {14th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS'23)},
  publisher = {ACM/IEEE},
  doi = {10.1145/3576841.3585936},
  publabel = {C38},
  pubtype = {C},
  dblp = {conf/iccps/RobinetteHJ23},
  pdf = "research/robinette2023iccps.pdf",
}
@article{nguyen2023tcns,
  title = {Decentralized Safe Control for Distributed Cyber-Physical Systems using Real-time Reachability Analysis},
  author = {Luan Viet Nguyen and Hoang-Dung Tran and Taylor T. Johnson and Vijay Gupta},
  year = {2023},
  month = jan,
  journal = {IEEE Transactions on Control of Network Systems (TCNS)},
  volume = {10},
  pages = {1234--1244},
  publisher = {IEEE},
  doi = {10.1109/TCNS.2023.3239562},
  publabel = {J29},
  pubtype = {J},
  dblp = {journals/tcns/NguyenTJG23},
  s2id = {256254052},
  pdf = "research/nguyen2023tcns.pdf",
}
@article{lopez2023jat,
  title = {Evaluation of Neural Network Verification Methods for Air-to-Air Collision Avoidance},
  author = {Diego Manzanas Lopez and Taylor T. Johnson and Stanley Bak and Hoang-Dung Tran and Kerianne L. Hobbs},
  year = {2023},
  month = oct,
  journal = {AIAA Journal of Air Transportation (JAT)},
  volume = {31},
  pages = {1--17},
  publisher = {AIAA},
  doi = {10.2514/1.D0255},
  publabel = {J30},
  pubtype = {J},
  pdf = "research/lopez2023jat.pdf",
}
@article{brix2023sttt,
  title = {First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)},
  author = {Christopher Brix and Mark Niklas Müller and Stanley Bak and Taylor T. Johnson and Changliu Liu},
  year = {2023},
  month = jan,
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  publisher = {Springer},
  doi = {10.1007/s10009-023-00703-4},
  publabel = {J28},
  pubtype = {J},
  arxiv = {2301.05815},
  dblp = {journals/corr/abs-2301-05815},
  s2id = {255942627},
  pdf = "research/brix2023sttt.pdf",
}
@inproceedings{muller2023vnncomp,
  title = {The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results},
  author = {Mark Niklas Müller and Christopher Brix and Stanley Bak and Changliu Liu and Taylor T. Johnson},
  year = {2022},
  publabel = {R11},
  pubtype = {R},
  dblp = {journals/corr/abs-2212-10376},
}
@inproceedings{lopez2022archcomp_ainncs,
  title = {ARCH-COMP22 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants},
  author = {Diego Manzanas Lopez and Matthias Althoff and Luis Benet and Xin Chen and Jiameng Fan and Marcelo Forets and Chao Huang and Taylor T. Johnson and Tobias Ladner and Wenchao Li and Christian Schilling and Qi Zhu},
  year = {2022},
  month = sep,
  booktitle = {EPiC Series in Computing 90, 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22)},
  volume = {90},
  pages = {142--98},
  publisher = {EasyChair},
  doi = {10.29007/wfgr},
  publabel = {OW11},
  pubtype = {OW},
  dblp = {conf/arch/LopezABCFFHJLL022},
  s2id = {195464916},
  pdf = "research/lopez2022archcomp_ainncs.pdf",
}
@inproceedings{johnson2022archcomp,
  title = {ARCH-COMP22 Repeatability Evaluation Report},
  author = {Taylor T. Johnson},
  year = {2022},
  month = sep,
  booktitle = {EPiC Series in Computing 90, 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22)},
  volume = {90},
  pages = {222--212},
  publisher = {EasyChair},
  doi = {10.29007/djqx},
  publabel = {OW10},
  pubtype = {OW},
  dblp = {conf/arch/Johnson22},
  pdf = "research/johnson2022archcomp.pdf",
}
@inproceedings{hamilton2022sefm,
  title = {Training Agents to Satisfy Timed and Untimed Signal Temporal Logic Specifications with Reinforcement Learning},
  author = {Nathaniel Hamilton and Preston K. Robinette and Taylor T. Johnson},
  year = {2022},
  month = sep,
  booktitle = {20th International Conference on Software Engineering and Formal Methods (SEFM'22)},
  pages = {190--206},
  publisher = {Springer},
  doi = {10.1007/978-3-031-17108-6_12},
  publabel = {C37},
  pubtype = {C},
  dblp = {conf/sefm/HamiltonRJ22},
  pdf = "research/hamilton2022sefm.pdf",
}
@inproceedings{serbinowska2022sefm,
  title = {BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees},
  author = {Serena Serbinowska and Taylor T. Johnson},
  year = {2022},
  month = sep,
  booktitle = {20th International Conference on Software Engineering and Formal Methods (SEFM'22)},
  pages = {307--323},
  publisher = {Springer},
  doi = {10.1007/978-3-031-17108-6_19},
  publabel = {C36},
  pubtype = {C},
  dblp = {conf/sefm/SerbinowskiJ22},
  pdf = "research/serbinowska2022sefm.pdf",
}
@inproceedings{lopez2022formats,
  title = {Reachability Analysis of a General Class of Neural Ordinary Differential Equations},
  author = {Diego Manzanas Lopez and Patrick Musau and Nathaniel Hamilton and Taylor T. Johnson},
  year = {2022},
  month = sep,
  booktitle = {20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'22)},
  pages = {258--277},
  publisher = {Springer},
  doi = {10.1007/978-3-031-15839-1_15},
  publabel = {C35},
  pubtype = {C},
  dblp = {conf/formats/LopezMHJ22},
  pdf = "research/lopez2022formats.pdf",
}
@inproceedings{yang2022formats,
  title = {Neural Network Repair with Reachability Analysis},
  author = {Xiaodong Yang and Tom Yamaguchi and Hoang-Dung Tran and Taylor T. Johnson and Danil Prokhorov},
  year = {2022},
  month = sep,
  booktitle = {20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'22)},
  pages = {221--236},
  publisher = {Springer},
  doi = {10.1007/978-3-031-15839-1_13},
  publabel = {C34},
  pubtype = {C},
  dblp = {conf/formats/YangYTHJP22},
  pdf = "research/yang2022formats.pdf",
}
@inproceedings{bao2022uai,
  title = {Physics Guided Neural Networks for Spatio-temporal Super-resolution of Turbulent Flows},
  author = {Tianshu Bao and Shengyu Chen and Taylor T. Johnson and Peyman Givi and Shervin Sammak and Xiaowei Jia},
  year = {2022},
  month = aug,
  booktitle = {38th Conference on Uncertainty in Artificial Intelligence (UAI'22)},
  volume = {180},
  pages = {118--128},
  publisher = {Proceedings of Machine Learning Research (PMLR)},
  publabel = {C33},
  pubtype = {C},
  dblp = {conf/uai/BaoCJGSJ22},
  pdf = "research/bao2022uai.pdf",
}
@article{tran2022lites,
  title = {Real-Time Verification for Distributed Cyber-Physical Systems},
  author = {Hoang-Dung Tran and Luan Viet Nguyen and Patrick Musau and Weiming Xiang and Taylor T. Johnson},
  year = {2022},
  month = feb,
  journal = {Leibniz Transactions on Embedded Systems (LITES)},
  publisher = {Dagstuhl},
  doi = {10.4230/LITES.8.2.7},
  publabel = {J25},
  pubtype = {J},
  dblp = {journals/lites/TranNMXJ22},
}
@inproceedings{robinette2022aerospace,
  title = {Reinforcement Learning Heuristics for Aerospace Control Systems},
  author = {Preston K. Robinette and Benjamin Heiner and Umberto Ravaioli and Nathaniel Hamilton and Taylor T. Johnson and Kerianne Hobbs},
  year = {2022},
  month = mar,
  booktitle = {IEEE Aerospace Conference},
  pages = {1--12},
  publisher = {IEEE},
  doi = {10.1109/AERO53065.2022.9843224},
  publabel = {OC14},
  pubtype = {OC},
  s2id = {251473019},
  pdf = "research/robinette2022aerospace.pdf",
}
@inproceedings{hamilton2022icaa,
  title = {Zero-Shot Policy Transfer in Autonomous Racing: Reinforcement Learning versus Imitation Learning},
  author = {Nathaniel Hamilton and Patrick Musau and Diego Manzanas Lopez and Taylor T. Johnson},
  year = {2022},
  month = mar,
  booktitle = {IEEE International Conference on Assured Autonomy (ICAA'22)},
  pages = {11--20},
  publisher = {IEEE},
  doi = {10.1109/ICAA52185.2022.00011},
  publabel = {OC13},
  pubtype = {OC},
  dblp = {conf/icaa2/HamiltonMLJ22},
  s2id = {248435373},
  pdf = "research/hamilton2022icaa.pdf",
}
@inproceedings{musau2022icaa,
  title = {On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers},
  author = {Patrick Musau and Nathaniel Hamilton and Diego Manzanas Lopez and Preston K. Robinette and Taylor T. Johnson},
  year = {2022},
  month = mar,
  booktitle = {IEEE International Conference on Assured Autonomy (ICAA'22)},
  pages = {1--10},
  publisher = {IEEE},
  doi = {10.1109/ICAA52185.2022.00010},
  publabel = {OC12},
  pubtype = {OC},
  dblp = {conf/icaa2/MusauHLRJ22},
  s2id = {248435263},
  pdf = "research/musau2022icaa.pdf",
}
@inproceedings{bao2021icdm,
  title = {Partial Differential Equation Driven Dynamic Graph Networks for Predicting Stream Water Temperature},
  author = {Tianshu Bao and Xiaowei Jia and Jacob Zwart and Jeffrey Sadler and Alison Appling and Samantha Oliver and Taylor T. Johnson},
  year = {2021},
  month = dec,
  booktitle = {21st IEEE International Conference on Data Mining (ICDM'21)},
  pages = {11--20},
  publisher = {IEEE},
  doi = {10.1109/ICDM51629.2021.00011},
  publabel = {C32},
  pubtype = {C},
  dblp = {conf/icdm/BaoJZSAOJ21},
  s2id = {246290850},
  pdf = "research/bao2021icdm.pdf",
}
@inproceedings{johnson2021archcomp_ainncs,
  title = {ARCH-COMP21 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants},
  author = {Taylor T. Johnson and Diego Manzanas Lopez and Luis Benet and Marcelo Forets and Sebastián Guadalupe and Christian Schilling and Radoslav Ivanov and Taylor J. Carpenter and James Weimer and Insup Lee},
  year = {2021},
  month = dec,
  booktitle = {EPiC Series in Computing 80, 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)},
  volume = {80},
  pages = {90--119},
  publisher = {EasyChair},
  doi = {10.29007/kfk9},
  publabel = {OW9},
  pubtype = {OW},
  dblp = {conf/arch/JohnsonLBFG0ICW21},
  s2id = {263873983},
  pdf = "research/johnson2021archcomp_ainncs.pdf",
}
@inproceedings{johnson2021archcomp,
  title = {ARCH-COMP21 Repeatability Evaluation Report},
  author = {Taylor T. Johnson},
  year = {2021},
  month = dec,
  booktitle = {EPiC Series in Computing 80, 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)},
  volume = {80},
  pages = {153--160},
  publisher = {EasyChair},
  doi = {10.29007/zqdx},
  publabel = {OW8},
  pubtype = {OW},
  dblp = {conf/arch/Johnson21},
  pdf = "research/johnson2021archcomp.pdf",
}
@inproceedings{pal2021snr,
  title = {Safety and Robustness Verification of Autoencoder based Regression Model using NNV Tool},
  author = {Neelanjana Pal and Taylor T. Johnson},
  year = {2021},
  month = aug,
  booktitle = {7th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR'21)},
  publabel = {OW15},
  pubtype = {OW},
  pdf = "research/pal2021snr.pdf",
}
@article{rosenfeld2021jns,
  title = {Dynamic Mode Decomposition for Continuous Time Systems with the Liouville Operator},
  author = {Joel A. Rosenfeld and Rushikesh Kamalapurkar and L. Forest Gruss and Taylor T. Johnson},
  year = {2022},
  month = oct,
  journal = {Journal of Nonlinear Science},
  publisher = {Springer},
  doi = {10.1007/s00332-021-09746-w},
  publabel = {J27},
  pubtype = {J},
  dblp = {journals/jns/RosenfeldKGJ22},
}
@article{yang2021tcps,
  title = {A Framework for Identification and Validation of Affine Hybrid Automata from Input-Output Traces},
  author = {Xiaodong Yang and Omar Beg and Matthew Kenigsberg and Taylor T. Johnson},
  year = {2022},
  month = aug,
  journal = {ACM Transactions on Cyber-Physical Systems (TCPS)},
  publisher = {ACM},
  doi = {10.1145/3470455},
  publabel = {J26},
  pubtype = {J},
  dblp = {journals/tcps/YangBKJ22},
  s2id = {246751128},
  pdf = "research/yang2021tcps.pdf",
}
@article{tran2021faoc,
  title = {Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter},
  author = {Hoang-Dung Tran and Neelanjana Pal and Diego Manzanas Lopez and Patrick Musau and Xiaodong Yang and Luan Viet Nguyen and Weiming Xiang and Stanley Bak and Taylor T. Johnson},
  year = {2021},
  month = aug,
  journal = {Formal Aspects of Computing},
  volume = {33},
  pages = {519--545},
  publisher = {Springer},
  doi = {10.1007/s00165-021-00553-4},
  publabel = {J23},
  pubtype = {J},
  dblp = {journals/fac/TranPLMYNXBJ21},
  pdf = "research/tran2021faoc.pdf",
}
@inproceedings{tran2021cav,
  title = {Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability},
  author = {Hoang-Dung Tran and Neelanjana Pal and Patrick Musau and Diego Manzanas Lopez and Nathaniel Hamilton and Xiaodong Yang and Stanley Bak and Taylor T. Johnson},
  year = {2021},
  month = jul,
  booktitle = {33rd International Conference on Computer-Aided Verification (CAV'21)},
  volume = {12759},
  pages = {263--283},
  publisher = {Springer},
  doi = {10.1007/978-3-030-81685-8_12},
  publabel = {C31},
  pubtype = {C},
  dblp = {conf/cav/TranPMLHYBJ21},
  s2id = {235602343},
  pdf = "research/tran2021cav.pdf",
}
@inproceedings{yang2021hscc,
  title = {Reachability Analysis of Deep ReLU Neural Networks using Facet-Vertex Incidence},
  author = {Xiaodong Yang and Tomoya Yamaguchi and Hoang-Dung Tran and Bardh Hoxha and Taylor T. Johnson and Danil Prokhorov},
  year = {2021},
  month = may,
  booktitle = {24th ACM International Conference on Hybrid Systems (HSCC'21)},
  pages = {18:1--7},
  publisher = {ACM},
  doi = {10.1145/3447928.3456650},
  publabel = {C30},
  pubtype = {C},
  dblp = {conf/hybrid/YangJT0HP21},
  s2id = {233486434},
  pdf = "research/yang2021hscc.pdf",
}
@inproceedings{rosenfeld2021acc,
  title = {On Occupation Kernels, Liouville Operators, and Dynamic Mode Decomposition},
  author = {Joel A. Rosenfeld and Rushikesh Kamalapurkar and L. Forest Gruss and Taylor T. Johnson},
  year = {2021},
  month = may,
  booktitle = {2021 American Control Conference (ACC)},
  pages = {3957--3962},
  publisher = {IEEE},
  doi = {10.23919/ACC50511.2021.9483121},
  publabel = {OC11},
  pubtype = {OC},
  dblp = {conf/amcc/RosenfeldKGJ21},
}
@article{beg2021access,
  title = {Cyber-Physical Anomaly Detection in Microgrids Using Time-Frequency Logic Formalism},
  author = {Omar Ali Beg and Luan Viet Nguyen and Taylor T. Johnson and Ali Davoudi},
  year = {2021},
  month = jan,
  journal = {IEEE Access},
  volume = {9},
  pages = {20012--20021},
  publisher = {IEEE},
  doi = {10.1109/ACCESS.2021.3055229},
  publabel = {J21},
  pubtype = {J},
  dblp = {journals/access/BegNJD21},
}
@inproceedings{muvva2021scitech,
  title = {Assuring Learning-Enabled Components in Small Unmanned Aircraft Systems},
  author = {Krishna Muvva and Justin M. Bradley and Marilyn Wolf and and Taylor T. Johnson},
  year = {2021},
  month = jan,
  booktitle = {AIAA Scitech 2021 Forum},
  publisher = {AIAA},
  doi = {10.2514/6.2021-0994},
  publabel = {LC9},
  pubtype = {LC},
  pdf = "research/muvva2021scitech.pdf",
}
@inproceedings{lopez2021scitech,
  title = {Verification of Neural Network Compression of ACAS Xu Lookup Tables with Star Set Reachability},
  author = {Diego Manzanas Lopez and Taylor T. Johnson and Hoang-Dung Tran and Stanley Bak and Xin Chen and and Kerianne L. Hobbs},
  year = {2021},
  month = jan,
  booktitle = {AIAA Scitech 2021 Forum},
  publisher = {AIAA},
  doi = {10.2514/6.2021-0995},
  publabel = {LC8},
  pubtype = {LC},
  s2id = {234246989},
  pdf = "research/lopez2021scitech.pdf",
}
@inproceedings{beg2020rw,
  title = {Formal Online Resiliency Monitoring in Microgrids},
  author = {Omar Ali Beg and Ajay P. Yadav and Taylor T. Johnson and Ali Davoudi},
  year = {2020},
  month = oct,
  booktitle = {IEEE 2020 Resilience Week (RWS)},
  pages = {99--105},
  publisher = {IEEE},
  doi = {10.1109/RWS50334.2020.9241272},
  publabel = {OC10},
  pubtype = {OC},
}
@inproceedings{johnson2020archcomp_ainncs,
  title = {ARCH-COMP20 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants},
  author = {Taylor T. Johnson and Diego Manzanas Lopez and Patrick Musau and Hoang-Dung Tran and Elena Botoeva and Francesco Leofante and Amir Maleki and Chelsea Sidrane and Jiameng Fan and Chao Huang},
  year = {2020},
  month = sep,
  booktitle = {EPiC Series in Computing 74, 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH'20)},
  volume = {74},
  pages = {107--139},
  publisher = {EasyChair},
  doi = {10.29007/9xgv},
  publabel = {OW7},
  pubtype = {OW},
  dblp = {conf/arch/JohnsonLMTBLMSF20},
  pdf = "research/johnson2020archcomp_ainncs.pdf",
}
@inproceedings{johnson2020archcomp,
  title = {ARCH-COMP20 Repeatability Evaluation Report},
  author = {Taylor T. Johnson},
  year = {2020},
  month = sep,
  booktitle = {EPiC Series in Computing 74, 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH'20)},
  volume = {74},
  pages = {175--183},
  publisher = {EasyChair},
  doi = {10.29007/8dp4},
  publabel = {OW6},
  pubtype = {OW},
  dblp = {conf/arch/Johnson20},
  pdf = "research/johnson2020archcomp.pdf",
}
@inproceedings{tran2022dt,
  title = {Verification Approaches for Learning-Enabled Autonomous Cyber-Physical Systems},
  author = {Hoang-Dung Tran and Weiming Xiang and Taylor T. Johnson},
  year = {2022},
  month = feb,
  booktitle = {IEEE Design and Test (D\&T)},
  volume = {39},
  pages = {24--34},
  publisher = {IEEE},
  doi = {10.1109/MDAT.2020.3015712},
  publabel = {J24},
  pubtype = {J},
  dblp = {journals/dt/TranXJ22},
  s2id = {226648636},
  pdf = "research/tran2022dt.pdf",
}
@article{xiang2020tnnls,
  title = {Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach},
  author = {Weiming Xiang and Hoang-Dung Tran and Taylor T. Johnson},
  year = {2021},
  month = may,
  journal = {IEEE Transactions on Neural Networks and Learning Systems (TNNLS)},
  volume = {32},
  pages = {1821--1830},
  publisher = {IEEE},
  doi = {10.1109/TNNLS.2020.2991090},
  publabel = {J22},
  pubtype = {J},
  arxiv = {2004.12273},
  dblp = {journals/tnn/XiangTYJ21},
  s2id = {216553342},
  pmid = {32452771},
  pdf = "research/xiang2020tnnls.pdf",
}
@inproceedings{bak2020cav,
  title = {Improved Geometric Path Enumeration for Verifying ReLU Neural Networks},
  author = {Stanley Bak and Hoang-Dung Tran and Kerianne Hobbs and Taylor T. Johnson},
  year = {2020},
  month = jul,
  booktitle = {32nd International Conference on Computer-Aided Verification (CAV'20)},
  volume = {12224},
  pages = {66--96},
  publisher = {Springer},
  doi = {10.1007/978-3-030-53288-8_4},
  publabel = {C28},
  pubtype = {C},
  dblp = {conf/cav/BakTHJ20},
  s2id = {220548064},
  pdf = "research/bak2020cav.pdf",
}
@inproceedings{tran2020cav,
  title = {Verification of Deep Convolutional Neural Networks Using ImageStars},
  author = {Hoang-Dung Tran and Stanley Bak and Weiming Xiang and Taylor T. Johnson},
  year = {2020},
  month = jul,
  booktitle = {32nd International Conference on Computer-Aided Verification (CAV'20)},
  volume = {12224},
  pages = {18--42},
  publisher = {Springer},
  doi = {10.1007/978-3-030-53288-8_2},
  publabel = {C29},
  pubtype = {C},
  dblp = {conf/cav/TranBXJ20},
  pdf = "research/tran2020cav.pdf",
}
@inproceedings{tran2020cav_tool,
  title = {NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems},
  author = {Hoang-Dung Tran and Xiaodong Yang and Diego Manzanas Lopez and Patrick Musau and Luan Viet Nguyen and Weiming Xiang and Stanley Bak and Taylor T. Johnson},
  year = {2020},
  month = jul,
  booktitle = {32nd International Conference on Computer-Aided Verification (CAV'20)},
  volume = {12224},
  pages = {3--17},
  publisher = {Springer},
  doi = {10.1007/978-3-030-53288-8_1},
  publabel = {C27},
  pubtype = {C},
  arxiv = {2004.05519},
  dblp = {journals/corr/abs-2004-05519},
  s2id = {215744954},
  pdf = "research/tran2020cav_tool.pdf",
}
@inproceedings{chowdhury2020icse_demo,
  title = {Demo: SLEMI: Finding Simulink Compiler Bugs through Equivalence Modulo Input (EMI)},
  author = {Shafiul Azam Chowdhury and Sohil Lal Shrestha and Taylor T. Johnson and Christoph Csallner},
  year = {2020},
  month = jun,
  booktitle = {42nd International Conference on Software Engineering (ICSE'20)},
  pages = {1--4},
  publisher = {ACM},
  doi = {10.1145/3377812.3382147},
  publabel = {D8},
  pubtype = {D},
  pdf = "research/chowdhury2020icse_demo.pdf",
}
@inproceedings{chowdhury2020icse,
  title = {SLEMI: Equivalence Modulo Input (EMI) Based Mutation of CPS Models for Finding Compiler Bugs in Simulink},
  author = {Shafiul Azam Chowdhury and Sohil Lal Shrestha and Taylor T. Johnson and Christoph Csallner},
  year = {2020},
  month = jun,
  booktitle = {42nd International Conference on Software Engineering (ICSE'20)},
  pages = {335--346},
  publisher = {ACM},
  doi = {10.1145/3377811.3380381},
  publabel = {C26},
  pubtype = {C},
  dblp = {conf/icse/ChowdhurySJC20},
  s2id = {211103257},
  pdf = "research/chowdhury2020icse.pdf",
}
@inproceedings{hamilton2020spie,
  title = {Sonic to knuckles: evaluations on transfer reinforcement learning},
  author = {Nathaniel Hamilton and Lena Schlemmer and Christopher Menart and Chad Waddington and Todd Jenkins and Taylor T. Johnson},
  year = {2020},
  month = apr,
  booktitle = {SPIE Defense + Commercial Sensing - Unmanned Systems Technology XXII},
  volume = {11425},
  pages = {20},
  publisher = {SPIE},
  doi = {10.1117/12.2559546},
  publabel = {LC7},
  pubtype = {LC},
  s2id = {219048377},
}
@inproceedings{tran2020destion,
  title = {NNV Demo: A Neural Network Verification Tool},
  author = {Hoang-Dung Tran and Diego Manzanas Lopez and Xiaodong Yang and Patrick Musau and Luan Viet Nguyen and Weiming Xiang and Stanley Bak and Taylor T. Johnson},
  year = {2020},
  month = apr,
  booktitle = {2nd IEEE Workshop on Design Automation for CPS and IoT (DESTION'20), Co-located with IEEE/ACM CPS-IoT Week 2020},
  pages = {21--22},
  publisher = {IEEE},
  doi = {10.1109/DESTION50928.2020.00010},
  publabel = {D7},
  pubtype = {D},
  s2id = {220606300},
  pdf = "research/tran2020destion.pdf",
}
@inproceedings{lopez2020waas,
  title = {Case Study: Safety Verification of an Unmanned Underwater Vehicle},
  author = {Diego Manzanas Lopez and Patrick Musau and Nathaniel Hamilton and Hoang-Dung Tran and Taylor T. Johnson},
  year = {2020},
  booktitle = {IEEE Workshop on Assured Autonomous Systems (WAAS'20), Co-located with the 41st IEEE Symposium on Security and Privacy (Oakland)},
  publabel = {W27},
  pubtype = {W},
  dblp = {conf/sp/LopezMHTJ20},
  pdf = "research/lopez2020waas.pdf",
}
@inproceedings{hartsell2019rsp,
  title = {CPS Design with Learning-Enabled Components: A Case Study},
  author = {Charles Hartsell and Nagabhushan Mahadevan and Shreyas Ramakrishna and Abhishek Dubey and Theodore Bapty and Taylor T. Johnson and Xenofon Koutsoukos and Janos Sztipanovits and Gabor Karsai},
  year = {2019},
  month = oct,
  booktitle = {30th International Workshop on Rapid System Prototyping (RSP'19)},
  pages = {57--63},
  publisher = {ACM},
  doi = {10.1145/3339985.3358491},
  publabel = {W26},
  pubtype = {W},
  dblp = {conf/rsp/HartsellMRDBJKS19},
}
@techreport{rosenfeld2019arxivDDD,
  title = {Dynamic Mode Decomposition for Continuous Time Systems with the Liouville Operator},
  author = {JA Rosenfeld and R Kamalapurkar and L Gruss and Taylor T. Johnson},
  year = {2019},
  institution = {arXiv preprint arXiv:1910.03977},
  publabel = {R10},
  pubtype = {R},
  dblp = {journals/jns/RosenfeldKGJ22},
}
@inproceedings{rosenfeld2019cdc,
  title = {Occupation Kernels and Densely Defined Liouville Operators for System Identification},
  author = {J. A. Rosenfeld and R. Kamalapurkar and B. Russo and Taylor T. Johnson},
  year = {2019},
  month = dec,
  booktitle = {IEEE 58th Conference on Decision and Control (CDC'19)},
  pages = {6455--6460},
  publisher = {IEEE},
  doi = {10.1109/CDC40024.2019.9029337},
  publabel = {OC9},
  pubtype = {OC},
  arxiv = {1909.11792},
  dblp = {journals/siamco/RosenfeldRKJ24},
  s2id = {202888498},
  pdf = "research/rosenfeld2019cdc.pdf",
}
@article{tran2019emsoft,
  title = {Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control},
  author = {HD Tran and F Cai and Diego Manzanas Lopez and P Musau and Taylor T. Johnson and X Koutsoukos},
  year = {2019},
  month = oct,
  journal = {ACM Transactions on Embedded Computing Systems (TECS), Special Issue from EMSOFT'19},
  volume = {18},
  number = {5s},
  pages = {105:1--105:22},
  publisher = {ACM},
  doi = {10.1145/3358230},
  publabel = {J19},
  pubtype = {J},
  dblp = {journals/tecs/TranCLMJK19},
  pdf = "research/tran2019emsoft.pdf",
}
@inproceedings{tran2019fm,
  title = {Star-Based Reachability Analysis of Deep Neural Networks},
  author = {HD Tran and DM Lopez and P Musau and X Yang and LV Nguyen and W Xiang and Taylor T. Johnson},
  year = {2019},
  month = sep,
  booktitle = {23rd International Symposium on Formal Methods (FM'19)},
  volume = {11800},
  pages = {670--686},
  publisher = {Springer},
  doi = {10.1007/978-3-030-30942-8_39},
  publabel = {C25},
  pubtype = {C},
  dblp = {conf/fm/TranLMYNXJ19},
  pdf = "research/tran2019fm.pdf",
}
@article{rosenfeld2024sicon,
  title = {The Occupation Kernel Method for Nonlinear System Identification},
  author = {JA Rosenfeld and B Russo and R Kamalapurkar and Taylor T. Johnson},
  year = {2024},
  journal = {SIAM Journal on Control and Optimization},
  volume = {62 (3)},
  pages = {1643--1668},
  publisher = {SIAM},
  doi = {10.1137/19M127029X},
  keywords = {reproducing kernel Hilbert spaces,nonlinear system identification,occupation kernels,Liouville operators,inner products,dynamical systems},
  publabel = {J31},
  pubtype = {J},
  dblp = {journals/siamco/RosenfeldRKJ24},
  pdf = "research/rosenfeld2024sicon.pdf",
}
@techreport{tran2019forte_extended,
  title = {Real-Time Verification for Distributed Cyber-Physical Systems},
  author = {HD Tran and LV Nguyen and P Musau and W Xiang and Taylor T. Johnson},
  year = {2019},
  institution = {arXiv preprint arXiv:1909.09087},
  publabel = {R9},
  pubtype = {R},
  dblp = {journals/lites/TranNMXJ22},
}
@inproceedings{tran2019formats,
  title = {Reachability Analysis for High-Index Linear Differential Algebraic Equations},
  author = {HD Tran and LV Nguyen and N Hamilton and W Xiang and Taylor T. Johnson},
  year = {2019},
  month = aug,
  booktitle = {17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'19)},
  volume = {11750},
  pages = {160--177},
  publisher = {Springer},
  doi = {10.1007/978-3-030-29662-9_10},
  publabel = {C24},
  pubtype = {C},
  dblp = {conf/formats/TranNHXJ19},
  s2id = {201107002},
  pdf = "research/tran2019formats.pdf",
}
@inproceedings{tran2019forte,
  title = {Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems},
  author = {HD Tran and LV Nguyen and P Musau and W Xiang and Taylor T. Johnson},
  year = {2019},
  month = jun,
  booktitle = {39th International Conference on Formal Techniques for Distributed Objects (FORTE'19)},
  volume = {11535},
  pages = {261--277},
  publisher = {Springer},
  doi = {10.1007/978-3-030-21759-4_15},
  publabel = {C23},
  pubtype = {C},
  dblp = {conf/forte/TranNMXJ19},
  s2id = {173992249},
  pdf = "research/tran2019forte.pdf",
}
@inproceedings{tran2019formalise,
  title = {Parallelizable reachability analysis algorithms for feed-forward neural networks},
  author = {HD Tran and P Musau and DM Lopez and X Yang and LV Nguyen and W Xiang and Taylor T. Johnson},
  year = {2019},
  month = may,
  booktitle = {7th IEEE/ACM International Conference on Formal Methods in Software Engineering (FormalISE'19)},
  pages = {31--40},
  publisher = {IEEE/ACM},
  doi = {10.1109/FormaliSE.2019.00012},
  publabel = {W23},
  pubtype = {W},
  dblp = {conf/icse/TranMLYNXJ19},
  s2id = {174803577},
  pdf = "research/tran2019formalise.pdf",
}
@inproceedings{tran2019dhs,
  title = {Decentralized real-time safety verification for distributed cyber-physical systems},
  author = {Hoang-Dung Tran and Luan Viet Nguyen and Patrick Musau and Weiming Xiang and Taylor T. Johnson},
  year = {2019},
  booktitle = {3rd International Workshop on Methods and Tools for Distributed Hybrid Systems (DHS'19)},
  publabel = {W25},
  pubtype = {W},
  dblp = {conf/forte/TranNMXJ19},
}
@inproceedings{tran2019fomlas,
  title = {Safety Verification in Reinforcement Learning Control},
  author = {Hoang-Dung Tran and Feiyang Cai and Diego Manzanas Lopez and Patrick Musau and Taylor T. Johnson and Xenofon Koutsoukos},
  year = {2019},
  booktitle = {2nd Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS'19)},
  publabel = {W24},
  pubtype = {W},
  pdf = "research/tran2019fomlas.pdf",
}
@inproceedings{lopez2019archcomp,
  title = {ARCH-COMP19 Category Report: Artificial Intelligence/Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants},
  author = {Diego Manzanas Lopez and Patrick Musau and Hoang-Dung Tran and Souradeep Dutta and Taylor J. Carpenter and Radoslav Ivanov and Taylor T. Johnson},
  year = {2019},
  month = may,
  booktitle = {EPiC Series in Computing 61, 6th Applied Verification for Continuous and Hybrid Systems (ARCH'19)},
  volume = {61},
  pages = {103--119},
  publisher = {EasyChair},
  doi = {10.29007/rgv8},
  publabel = {OW5},
  pubtype = {OW},
  dblp = {conf/cpsweek/LopezMTDCIJ19},
  s2id = {263861068},
  pdf = "research/lopez2019archcomp.pdf",
}
@inproceedings{lopez2019arch,
  title = {Verification of closed-loop systems with neural network controllers},
  author = {DM Lopez and P Musau and HD Tran and Taylor T. Johnson},
  year = {2019},
  month = may,
  booktitle = {EPiC Series in Computing 61, 6th Applied Verification for Continuous and Hybrid Systems (ARCH'19)},
  volume = {61},
  pages = {201--210},
  publisher = {EasyChair},
  doi = {10.29007/btv1},
  publabel = {W22},
  pubtype = {W},
  dblp = {conf/cpsweek/LopezMTJ19},
  pdf = "research/lopez2019arch.pdf",
}
@inproceedings{johnson2019archcomp,
  title = {ARCH-COMP19 Repeatability Evaluation Report},
  author = {Taylor T. Johnson},
  year = {2019},
  month = may,
  booktitle = {EPiC Series in Computing 61, 6th Applied Verification for Continuous and Hybrid Systems (ARCH'19)},
  volume = {61},
  pages = {162--169},
  publisher = {EasyChair},
  doi = {10.29007/wbl3},
  publabel = {OW4},
  pubtype = {OW},
  dblp = {conf/cpsweek/Johnson19},
  pdf = "research/johnson2019archcomp.pdf",
}
@inproceedings{rees2019iccps,
  title = {Cyber-physical systems virtual organization: Active resources: enabling reproducibility, improving accessibility, and lowering the barrier to entry},
  author = {SA Rees and T Kecskes and P Meijer and Taylor T. Johnson and K Dey and P Tabuada and M Lucas},
  year = {2019},
  booktitle = {10th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS'19)},
  pages = {340--341},
  publisher = {ACM/IEEE},
  doi = {10.1145/3302509.3313331},
  publabel = {D6},
  pubtype = {D},
  dblp = {conf/iccps/ReesKMJDTL19},
  s2id = {102347897},
}
@inproceedings{bak2019hscc,
  title = {Numerical verification of affine systems with up to a billion dimensions},
  author = {S Bak and HD Tran and Taylor T. Johnson},
  year = {2019},
  month = apr,
  booktitle = {22nd ACM International Conference on Hybrid Systems (HSCC'19)},
  pages = {23--32},
  publisher = {ACM},
  doi = {10.1145/3302504.3311792},
  publabel = {C22},
  pubtype = {C},
  arxiv = {1804.01583},
  dblp = {journals/corr/abs-1804-01583},
  s2id = {4602804},
  pdf = "research/bak2019hscc.pdf",
}
@inproceedings{kecskes2019destion,
  title = {Demo: A Design Studio for Verification Tools},
  author = {T Kecskes and P Meijer and Taylor T. Johnson and M Lucas},
  year = {2019},
  month = apr,
  booktitle = {1st Workshop on Design Automation for CPS and IoT (DESTION'19)},
  pages = {60--61},
  publisher = {ACM},
  doi = {10.1145/3313151.3314057},
  publabel = {W21},
  pubtype = {W},
  dblp = {conf/cpsweek/KecskesMJL19},
  s2id = {239333144},
}
@inproceedings{hartsell2019destion,
  title = {Model-based design for CPS with learning-enabled components},
  author = {Charles Hartsell and Nagabhushan Mahadevan and Shreyas Ramakrishna and Abhishek Dubey and Theodore Bapty and Taylor T. Johnson and Xenofon Koutsoukos and Janos Sztipanovits and Gabor Karsai},
  year = {2019},
  month = apr,
  booktitle = {1st Workshop on Design Automation for CPS and IoT (DESTION'19)},
  pages = {1--9},
  publisher = {ACM},
  doi = {10.1145/3313151.3313166},
  publabel = {W20},
  pubtype = {W},
  dblp = {conf/cpsweek/HartsellMRDBJKS19},
  s2id = {85519087},
  pdf = "research/hartsell2019destion.pdf",
}
@article{bak2019sttt,
  title = {Hybrid automata: from verification to implementation},
  author = {S Bak and OA Beg and S Bogomolov and Taylor T. Johnson and LV Nguyen and C Schilling},
  year = {2019},
  month = feb,
  journal = {International Journal on Software Tools for Technology Transfer (STTT), Springer},
  volume = {21 (1)},
  pages = {87--104},
  doi = {10.1007/s10009-017-0458-1},
  publabel = {J15},
  pubtype = {J},
  dblp = {journals/sttt/BakBBJNS19},
  pdf = "research/bak2019sttt.pdf",
}
@incollection{xiang2019ust,
  title = {Reachable Set Estimation and Verification for Neural Network Models of Nonlinear Dynamic Systems},
  author = {W Xiang and DM Lopez and P Musau and Taylor T. Johnson},
  year = {2019},
  booktitle = {Safe, Autonomous and Intelligent Vehicles, Series on Unmanned Systems Technologies, Springer},
  pages = {123--144},
  doi = {10.1007/978-3-319-97301-2_7},
  publabel = {BC1},
  pubtype = {BC},
  arxiv = {1802.03557},
  dblp = {journals/corr/abs-1802-03557},
  s2id = {3640186},
  pdf = "research/xiang2019ust.pdf",
}
@inproceedings{xiang2019vnn,
  title = {Specification-Guided Safety Verification for Feedforward Neural Networks},
  author = {W Xiang and HD Tran and Taylor T. Johnson},
  year = {2019},
  booktitle = {2nd Verification of Neural Networks (VNN'19), AAAI 2019 Spring Symposium},
  publabel = {W19},
  pubtype = {W},
  dblp = {journals/corr/abs-1812-06161},
  pdf = "research/xiang2019vnn.pdf",
}
@inproceedings{xiang2019vnn_nncs,
  title = {Reachability Analysis and Safety Verification for Neural Network Control Systems},
  author = {W Xiang and Xiaodong Yang and HD Tran and Taylor T. Johnson},
  year = {2019},
  booktitle = {2nd Verification of Neural Networks (VNN'19), AAAI 2019 Spring Symposium},
  publabel = {W18},
  pubtype = {W},
  dblp = {journals/corr/abs-1805-09944},
  pdf = "research/xiang2019vnn_nncs.pdf",
}
@inproceedings{rahman2019aap,
  title = {Using crowd sourcing to locate and characterize conflicts for vulnerable modes},
  author = {Ziaur Rahman and Stephen P. Mattingly and Rahul Kawadgave and Dian Nostikasari and Nicole Roeglin and Colleen Casey and Taylor T. Johnson},
  year = {2019},
  month = jul,
  booktitle = {Accident Analysis and Prevention},
  volume = {128},
  pages = {23--39},
  publisher = {Elsevier},
  doi = {10.1016/j.aap.2019.03.014},
  publabel = {J17},
  pubtype = {J},
  s2id = {102349640},
  pmid = {30954784},
  pdf = "research/rahman2019aap.pdf",
}
@techreport{xiang2018survey,
  title = {Verification for Machine Learning, Autonomy, and Neural Networks Survey},
  author = {W Xiang and P Musau and AA Wild and DM Lopez and N Hamilton and X Yang and J Rosenfeld and Taylor T. Johnson},
  year = {2018},
  institution = {arXiv preprint arXiv:1810.01989},
  publabel = {R7},
  pubtype = {R},
  pdf = "research/xiang2018survey.pdf",
}
@inproceedings{nguyen2018adhs,
  title = {Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS},
  author = {LV Nguyen and B Hoxha and Taylor T. Johnson and G Fainekos},
  year = {2018},
  month = jul,
  booktitle = {6th IFAC Analysis and Design of Hybrid Systems (ADHS'18)},
  volume = {51},
  number = {16},
  pages = {67--72},
  publisher = {IFAC/Elsevier},
  doi = {10.1016/j.ifacol.2018.08.012},
  publabel = {OC8},
  pubtype = {OC},
  dblp = {conf/adhs/NguyenHJF18},
  s2id = {52953695},
  pdf = "research/nguyen2018adhs.pdf",
}
@inproceedings{tran2018adhs,
  title = {Reachability Analysis for One Dimensional Linear Parabolic Equations},
  author = {HD Tran and W Xiang and S Bak and Taylor T. Johnson},
  year = {2018},
  month = jul,
  booktitle = {6th IFAC Analysis and Design of Hybrid Systems (ADHS'18)},
  volume = {51},
  number = {16},
  pages = {133--138},
  publisher = {IFAC/Elsevier},
  doi = {10.1016/j.ifacol.2018.08.023},
  publabel = {OC7},
  pubtype = {OC},
  dblp = {conf/adhs/TranXBJ18},
  s2id = {51991984},
  pdf = "research/tran2018adhs.pdf",
}
@techreport{xiang2018nncs,
  title = {Reachability Analysis and Safety Verification for Neural Network Control Systems},
  author = {W Xiang and Taylor T. Johnson},
  year = {2018},
  institution = {arXiv preprint arXiv:1805.09944},
  publabel = {R6},
  pubtype = {R},
  pdf = "research/xiang2018nncs.pdf",
}
@article{beg2018tsg,
  title = {Signal Temporal Logic-based Attack Detection in DC Microgrids},
  author = {OA Beg and LV Nguyen and Taylor T. Johnson and A Davoudi},
  year = {2019},
  month = jul,
  journal = {IEEE Transactions on Smart Grid (TSG)},
  volume = {10},
  number = {4},
  pages = {3585--3595},
  publisher = {IEEE},
  doi = {10.1109/TSG.2018.2832544},
  publabel = {J16},
  pubtype = {J},
  pdf = "research/beg2018tsg.pdf",
}
@inproceedings{chowdhury2018icse,
  title = {Automatically Finding Bugs in a Commercial Cyber-Physical System Development Tool Chain With SLforge},
  author = {SA Chowdhury and S Mohian and S Mehra and Taylor T. Johnson and C Csallner},
  year = {2018},
  month = may,
  booktitle = {40th International Conference on Software Engineering (ICSE'18)},
  pages = {981--992},
  publisher = {ACM},
  doi = {10.1145/3180155.3180231},
  publabel = {C21},
  pubtype = {C},
  dblp = {conf/icse/ChowdhuryMMGJC18},
  s2id = {47019892},
  pdf = "research/chowdhury2018icse.pdf",
}
@article{xiang2018tac_a,
  title = {Robust exponential stability and disturbance attenuation for discrete-time switched systems under arbitrary switching},
  author = {W Xiang and HD Tran and Taylor T. Johnson},
  year = {2018},
  month = may,
  journal = {IEEE Transactions on Automatic Control (TAC)},
  volume = {63},
  number = {5},
  pages = {1450--1456},
  publisher = {IEEE},
  doi = {10.1109/TAC.2017.2748918},
  publabel = {J13},
  pubtype = {J},
  dblp = {journals/tac/XiangTJ18},
  pdf = "research/xiang2018tac_a.pdf",
}
@techreport{tran2018dae,
  title = {Simulation-Based Reachability Analysis for High-Index Large Linear Differential Algebraic Equations},
  author = {HD Tran and W Xiang and N Hamilton and Taylor T. Johnson},
  year = {2018},
  institution = {arXiv preprint arXiv:1804.03227},
  publabel = {R5},
  pubtype = {R},
  dblp = {journals/corr/abs-1804-03227},
}
@inproceedings{musau2018arch_dae,
  title = {Differential Algebraic Equations (DAEs) with Varying Index (Benchmark Proposal)},
  author = {Patrick Musau and Diego Manzanas Lopez and Hoang-Dung Tran and Taylor T. Johnson},
  year = {2018},
  month = sep,
  booktitle = {5th International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'18)},
  volume = {54},
  pages = {174--184},
  publisher = {EasyChair},
  doi = {10.29007/4gj7},
  publabel = {W17},
  pubtype = {W},
}
@inproceedings{musau2018arch_ctrnn,
  title = {Continuous-Time Recurrent Neural Networks (CTRNNs) (Benchmark Proposal)},
  author = {Patrick Musau and Taylor T. Johnson},
  year = {2018},
  month = sep,
  booktitle = {5th International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'18)},
  volume = {54},
  pages = {196--207},
  publisher = {EasyChair},
  doi = {10.29007/6czp},
  publabel = {W16},
  pubtype = {W},
}
@inproceedings{tran2018arch,
  title = {Discrete-Space Analysis of Partial Differential Equations (PDEs) (Benchmark Proposal)},
  author = {Hoang-Dung Tran and Tianshu Bao and Taylor T. Johnson},
  year = {2018},
  month = sep,
  booktitle = {5th International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'18)},
  volume = {54},
  pages = {185--195},
  publisher = {EasyChair},
  doi = {10.29007/fvpp},
  publabel = {W15},
  pubtype = {W},
}
@inproceedings{johnson2018archcomp,
  title = {ARCH-COMP18 Repeatability Evaluation Report},
  author = {Taylor T. Johnson},
  year = {2018},
  month = sep,
  booktitle = {5th International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'18)},
  volume = {54},
  pages = {128--134},
  publisher = {EasyChair},
  doi = {10.29007/n9t3},
  publabel = {OW3},
  pubtype = {OW},
  dblp = {conf/adhs/Johnson18},
}
@techreport{bak2019hscc_arxiv,
  title = {Numerical Verification of Affine Systems with up to a Billion Dimensions},
  author = {S Bak and HD Tran and Taylor T. Johnson},
  year = {2019},
  institution = {arXiv preprint arXiv:1804.01583},
  publabel = {R8},
  pubtype = {R},
  dblp = {conf/hybrid/BakTJ19},
}
@article{xiang2018tnnls,
  title = {Output reachable set estimation and verification for multilayer neural networks},
  author = {W Xiang and HD Tran and Taylor T. Johnson},
  year = {2018},
  month = mar,
  journal = {IEEE Transactions on Neural Networks and Learning Systems (TNNLS)},
  volume = {29},
  number = {11},
  pages = {5777--5783},
  publisher = {IEEE},
  doi = {10.1109/TNNLS.2018.2808470},
  publabel = {J12},
  pubtype = {J},
  dblp = {journals/tnn/XiangTJ18},
  pdf = "research/xiang2018tnnls.pdf",
}
@techreport{johnson2018afrltr,
  title = {Formal Modeling, Monitoring, and Control of Emergence in Distributed Cyber-Physical Systems},
  author = {Taylor T. Johnson},
  year = {2018},
  institution = {University of Texas at Arlington Arlington United States},
  publabel = {R4},
  pubtype = {R},
}
@inproceedings{xiang2018acc,
  title = {Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers},
  author = {W Xiang and HD Tran and JA Rosenfeld and Taylor T. Johnson},
  year = {2018},
  month = jun,
  booktitle = {American Control Conference (ACC'18)},
  pages = {1574--1579},
  publisher = {IEEE},
  doi = {10.23919/ACC.2018.8431048},
  publabel = {OC6},
  pubtype = {OC},
  arxiv = {1802.06981},
  dblp = {journals/corr/abs-1802-06981},
  s2id = {3385941},
  pdf = "research/xiang2018acc.pdf",
}
@article{sogokon2019jar,
  title = {Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants},
  author = {A Sogokon and PB Jackson and Taylor T. Johnson},
  year = {2019},
  month = dec,
  journal = {Journal of Automated Reasoning (JAR), Springer},
  volume = {63},
  number = {4},
  pages = {1005--1029},
  doi = {10.1007/s10817-018-9497-x},
  publabel = {J20},
  pubtype = {J},
  dblp = {journals/jar/SogokonJJ19},
  pdf = "research/sogokon2019jar.pdf",
}
@article{xiang2018tac_b,
  title = {Nonconservative Lifted Convex Conditions for Stability of Discrete-Time Switched Systems under Minimum Dwell-Time Constraint},
  author = {W Xiang and HD Tran and Taylor T. Johnson},
  year = {2019},
  month = aug,
  journal = {IEEE Transactions on Automatic Control (TAC)},
  volume = {64},
  number = {8},
  pages = {3407--3414},
  publisher = {IEEE},
  doi = {10.1109/TAC.2018.2879585},
  publabel = {J18},
  pubtype = {J},
  dblp = {journals/tac/XiangTJ19},
  pdf = "research/xiang2018tac_b.pdf",
}
@inproceedings{chowdhury2018sescps,
  title = {A Curated Corpus of Simulink Models for Model-based Empirical Studies},
  author = {SA Chowdhury and LS Varghese and S Mohian and Taylor T. Johnson and C Csallner},
  year = {2018},
  month = may,
  booktitle = {4th International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS '18)},
  pages = {45--48},
  publisher = {ACM},
  doi = {10.1145/3196478.3196484},
  publabel = {W14},
  pubtype = {W},
  dblp = {conf/icse/ChowdhuryVMJC18},
  s2id = {49866368},
}
@article{nguyen2018tcps,
  title = {Cyber-Physical Specification Mismatches},
  author = {LV Nguyen and KA Hoque and S Bak and S Drager and Taylor T. Johnson},
  year = {2018},
  month = jul,
  journal = {ACM Transactions on Cyber-Physical Systems (TCPS)},
  volume = {2},
  number = {4},
  pages = {23:1--23:26},
  publisher = {ACM},
  doi = {10.1145/3170500},
  publabel = {J14},
  pubtype = {J},
  arxiv = {1806.09224},
  dblp = {journals/tcps/NguyenHBDJ18},
  s2id = {49420245},
  pdf = "research/nguyen2018tcps.pdf",
}
@techreport{xiang2018tcyb,
  title = {Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations},
  author = {W Xiang and HD Tran and Taylor T. Johnson},
  year = {2017},
  institution = {arXiv preprint arXiv:1712.08163},
  publabel = {R3},
  pubtype = {R},
  dblp = {journals/corr/abs-1712-08163},
  pdf = "research/xiang2018tcyb.pdf",
}
@article{sogokon2017emsoft_tecs,
  title = {Operational Models for Piecewise-Smooth Systems},
  author = {A Sogokon and K Ghorbal and Taylor T. Johnson},
  year = {2017},
  month = oct,
  journal = {ACM Transactions on Embedded Computing Systems (TECS), Special Issue from EMSOFT'17},
  volume = {16},
  number = {5s},
  pages = {185:1--185:19},
  publisher = {ACM},
  doi = {10.1145/3126506},
  publabel = {J11},
  pubtype = {J},
  dblp = {journals/tecs/SogokonGJ17},
}
@article{xiang2017tac,
  title = {Output Reachable Set Estimation for Switched Linear Systems and Its Application in Safety Verification},
  author = {W Xiang and HD Tran and Taylor T. Johnson},
  year = {2017},
  month = oct,
  journal = {IEEE Transactions on Automatic Control (TAC)},
  volume = {62},
  number = {10},
  pages = {5380--5387},
  publisher = {IEEE},
  doi = {10.1109/TAC.2017.2692100},
  publabel = {J10},
  pubtype = {J},
  dblp = {journals/tac/XiangTJ17},
  pdf = "research/xiang2017tac.pdf",
}
@article{beg2017tii,
  title = {Detection of false-data injection attacks in cyber-physical DC microgrids},
  author = {OA Beg and Taylor T. Johnson and A Davoudi},
  year = {2017},
  month = oct,
  journal = {IEEE Transactions on Industrial Informatics (TII)},
  volume = {13},
  number = {5},
  pages = {2693--2703},
  publisher = {IEEE},
  doi = {10.1109/TII.2017.2656905},
  publabel = {J9},
  pubtype = {J},
  dblp = {journals/tii/BegJD17},
  pdf = "research/beg2017tii.pdf",
}
@inproceedings{nguyen2017memocode,
  title = {Hyperproperties of real-valued signals},
  author = {LV Nguyen and J Kapinski and X Jin and JV Deshmukh and Taylor T. Johnson},
  year = {2017},
  month = sep,
  booktitle = {15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'17)},
  pages = {104--113},
  publisher = {ACM},
  doi = {10.1145/3127041.3127058},
  publabel = {C20},
  pubtype = {C},
  dblp = {conf/memocode/NguyenKJDJ17},
  s2id = {28305918},
  pdf = "research/nguyen2017memocode.pdf",
}
@article{beg2017tie,
  title = {Model Validation of PWM DC-DC Converters},
  author = {OA Beg and H Abbas and Taylor T. Johnson and A Davoudi},
  year = {2017},
  month = sep,
  journal = {IEEE Transactions on Industrial Electronics (TIE)},
  volume = {64},
  number = {9},
  pages = {7049--7059},
  publisher = {IEEE},
  doi = {10.1109/TIE.2017.2688961},
  publabel = {J8},
  pubtype = {J},
  dblp = {journals/tie/BegAJD17},
  s2id = {28256105},
  pdf = "research/beg2017tie.pdf",
}
@inproceedings{beg2017fac,
  title = {Computer-Aided Formal Verification of Power Electronics Circuits},
  author = {OA Beg and L Nguyen and A Davoudi and Taylor T. Johnson},
  year = {2017},
  month = jul,
  booktitle = {VDE Frontiers in Analog Computer Aided Design (FAC'17)},
  pages = {21--26},
  publisher = {VDE},
  publabel = {OC5},
  pubtype = {OC},
  pdf = "research/beg2017fac.pdf",
}
@inproceedings{johnson2017archcomp,
  title = {ARCH-COMP17 Repeatability Evaluation Report},
  author = {Taylor T. Johnson},
  year = {2017},
  month = jun,
  booktitle = {4th International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'17)},
  volume = {48},
  pages = {175--180},
  publisher = {EasyChair},
  doi = {10.29007/7hvk},
  publabel = {OW2},
  pubtype = {OW},
  dblp = {conf/cpsweek/Johnson17},
  pdf = "research/johnson2017archcomp.pdf",
}
@inproceedings{beg2017arch,
  title = {Reachability Analysis of Transformer-Isolated DC-DC Converters (Benchmark Proposal)},
  author = {OA Beg and A Davoudi and Taylor T. Johnson},
  year = {2017},
  month = jun,
  booktitle = {4th International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'17)},
  volume = {48},
  pages = {52--64},
  publisher = {EasyChair},
  doi = {10.29007/8xk7},
  publabel = {W11},
  pubtype = {W},
  dblp = {conf/cpsweek/BegDJ17},
  s2id = {11391289},
  pdf = "research/beg2017arch.pdf",
}
@inproceedings{tran2017arch,
  title = {Distributed Autonomous Systems (Benchmark Proposal)},
  author = {HD Tran and LV Nguyen and W Xiang and Taylor T. Johnson},
  year = {2017},
  month = jun,
  booktitle = {4th International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'17)},
  volume = {48},
  pages = {33--43},
  publisher = {EasyChair},
  doi = {10.29007/slz2},
  publabel = {W12},
  pubtype = {W},
  dblp = {conf/cpsweek/TranNXJ17},
  s2id = {13461803},
  pdf = "research/tran2017arch.pdf",
}
@article{tran2017deds,
  title = {Order-reduction abstractions for safety verification of high-dimensional linear systems},
  author = {HD Tran and LV Nguyen and W Xiang and Taylor T. Johnson},
  year = {2017},
  month = apr,
  journal = {Discrete Event Dynamic Systems (DEDS), Springer},
  volume = {27},
  number = {2},
  pages = {443--461},
  doi = {10.1007/s10626-017-0244-y},
  publabel = {J6},
  pubtype = {J},
  dblp = {journals/deds/TranNXJ17},
  pdf = "research/tran2017deds.pdf",
}
@inproceedings{xiang2017acc,
  title = {On reachable set estimation for discrete-time switched linear systems under arbitrary switching},
  author = {W Xiang and HD Tran and Taylor T. Johnson},
  year = {2017},
  month = may,
  booktitle = {American Control Conference (ACC'17)},
  pages = {4534--4539},
  publisher = {IEEE},
  doi = {10.23919/ACC.2017.7963654},
  publabel = {OC4},
  pubtype = {OC},
  dblp = {conf/amcc/XiangTJ17},
  pdf = "research/xiang2017acc.pdf",
}
@inproceedings{johnson2017fever,
  title = {Reusable and Understandable Formal Verification for Cyber-Physical Systems},
  author = {Taylor T. Johnson},
  year = {2017},
  booktitle = {1st International Workshop on Formal Approaches to Explainable VERification (FEVER'17)},
  publabel = {W13},
  pubtype = {W},
  pdf = "research/johnson2017fever.pdf",
}
@inproceedings{sogokon2017nfm,
  title = {Verifying safety and persistence properties of hybrid systems using flowpipes and continuous invariants},
  author = {A Sogokon and PB Jackson and Taylor T. Johnson},
  year = {2017},
  month = may,
  booktitle = {9th NASA Formal Methods Symposium (NFM'17)},
  volume = {10227},
  pages = {194--211},
  publisher = {Springer},
  doi = {10.1007/978-3-319-57288-8_14},
  publabel = {C19},
  pubtype = {C},
  dblp = {conf/nfm/SogokonJJ17},
  pdf = "research/sogokon2017nfm.pdf",
}
@inproceedings{nguyen2017hscc,
  title = {Abnormal data classification using time-frequency temporal logic},
  author = {LV Nguyen and J Kapinski and X Jin and JV Deshmukh and K Butts and Taylor T. Johnson},
  year = {2017},
  month = apr,
  booktitle = {20th International Conference on Hybrid Systems: Computation and Control (HSCC'17)},
  pages = {237--242},
  publisher = {ACM},
  doi = {10.1145/3049797.3049809},
  publabel = {C18},
  pubtype = {C},
  dblp = {conf/hybrid/NguyenKJDBJ17},
  pdf = "research/nguyen2017hscc.pdf",
}
@inproceedings{siddique2017date,
  title = {Formal Specification and Dependability Analysis of Optical Communication Networks},
  author = {U Siddique and KA Hoque and Taylor T. Johnson},
  year = {2017},
  month = mar,
  booktitle = {Design, Automation, and Test in Europe (DATE'17)},
  pages = {1564--1569},
  publisher = {IEEE},
  doi = {10.23919/DATE.2017.7927239},
  publabel = {C17},
  pubtype = {C},
  dblp = {conf/date/SiddiqueHJ17},
  s2id = {39616374},
}
@article{xiang2017cta,
  title = {Event-triggered control for continuous-time switched linear systems},
  author = {W Xiang and Taylor T. Johnson},
  year = {2017},
  month = jul,
  journal = {IET Control Theory and Applications (CTA)},
  volume = {11},
  number = {11},
  pages = {1694--1703},
  publisher = {IET},
  doi = {10.1049/iet-cta.2016.0672},
  publabel = {J7},
  pubtype = {J},
  s2id = {33237358},
  pdf = "research/xiang2017cta.pdf",
}
@inproceedings{chowdhury2017hscc_demo,
  title = {Fuzzing Cyber-Physical System Development Environments With CyFuzz},
  author = {Taylor T. Johnson and C Csallner},
  year = {2017},
  booktitle = {20th International Conference on Hybrid Systems: Computation and Control (HSCC'17)},
  publabel = {TALK6},
  pubtype = {TALK},
}
@inproceedings{xiang2016cdc,
  title = {Reachable set estimation and control for switched linear systems with dwell-time restriction},
  author = {W Xiang and HD Tran and Taylor T. Johnson},
  year = {2016},
  month = dec,
  booktitle = {55th IEEE Conference on Decision and Control (CDC'16)},
  pages = {7246--7251},
  publisher = {IEEE},
  doi = {10.1109/CDC.2016.7799387},
  publabel = {OC3},
  pubtype = {OC},
  gsid = {14666544104064248628},
  dblp = {conf/cdc/XiangTJ16},
  s2id = {25831340},
  pdf = "research/xiang2016cdc.pdf",
}
@inproceedings{sogokon2016fm,
  title = {Decoupling Abstractions of Non-linear Ordinary Differential Equations},
  author = {A Sogokon and K Ghorbal and Taylor T. Johnson},
  year = {2016},
  month = nov,
  booktitle = {International Symposium on Formal Methods (FM'16)},
  volume = {9995},
  pages = {628--644},
  publisher = {Springer},
  doi = {10.1007/978-3-319-48989-6_38},
  publabel = {C16},
  pubtype = {C},
  gsid = {6661230319939383532},
  dblp = {conf/fm/SogokonGJ16},
  s2id = {17823282},
  pdf = "research/sogokon2016fm.pdf",
}
@inproceedings{duggirala2016msc,
  title = {Tutorial: software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP},
  author = {Parasara Sridhar Duggirala and Chuchu Fan and Matthew Potok and Bolun Qi and Sayan Mitra and Mahesh Viswanathan and Stanley Bak and Sergiy Bogomolov and Taylor T. Johnson and Luan Viet Nguyen and Christian Schilling and Andrew Sogokon and Hoang-Dung Tran and Weiming Xiang},
  year = {2016},
  month = sep,
  booktitle = {IEEE Conference on Control Applications (CCA'16)},
  pages = {1024--1029},
  publisher = {IEEE},
  doi = {10.1109/CCA.2016.7587948},
  publabel = {OC2},
  pubtype = {OC},
  gsid = {14666544104064248628},
  dblp = {conf/IEEEcca/DuggiralaFPQM0B16},
  pdf = "research/duggirala2016msc.pdf",
}
@article{bogomolov2016sttt,
  title = {Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions},
  author = {Sergiy Bogomolov and Alexandre Donzé and Goran Frehse and Radu Grosu and Taylor T. Johnson and Hamed Ladan and Andreas Podelski and Martin Wehrle},
  year = {2016},
  month = aug,
  journal = {International Journal on Software Tools for Technology Transfer (STTT), Springer},
  volume = {18},
  number = {4},
  pages = {449--467},
  doi = {10.1007/s10009-015-0393-y},
  publabel = {J5},
  pubtype = {J},
  gsid = {4980588848043524788},
  dblp = {journals/sttt/BogomolovDFGJLP16},
  s2id = {5823735},
  pmid = {27445640},
  pdf = "research/bogomolov2016sttt.pdf",
}
@inproceedings{sardar2016nfm,
  title = {Probabilistic formal verification of the SATS concept of operation},
  author = {MU Sardar and N Afaq and KA Hoque and Taylor T. Johnson and O Hasan},
  year = {2016},
  month = jun,
  booktitle = {8th NASA Formal Methods Symposium (NFM'16)},
  volume = {9690},
  pages = {191--205},
  publisher = {Springer},
  doi = {10.1007/978-3-319-40648-0_15},
  publabel = {C15},
  pubtype = {C},
  dblp = {conf/nfm/SardarAHJH16},
  s2id = {13366343},
  pdf = "research/sardar2016nfm.pdf",
}
@article{johnson2016tecs,
  title = {Real-time reachability for verified simplex design},
  author = {Taylor T. Johnson and S Bak and M Caccamo and L Sha},
  year = {2016},
  month = feb,
  journal = {ACM Transactions on Embedded Computing Systems (TECS)},
  volume = {15},
  number = {2},
  pages = {26:1--26:27},
  publisher = {ACM},
  doi = {10.1145/2723871},
  publabel = {J4},
  pubtype = {J},
  dblp = {journals/tecs/JohnsonBCS16},
  pdf = "research/johnson2016tecs.pdf",
}
@inproceedings{beg2016arch,
  title = {Charge Pump Phase-Locked Loops and Full Wave Rectifiers for Reachability Analysis (Benchmark Proposal)},
  author = {OA Beg and A Davoudi and Taylor T. Johnson},
  year = {2016},
  booktitle = {3rd International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'16)},
  volume = {43},
  pages = {27--35},
  publisher = {EasyChair},
  doi = {10.29007/x211},
  publabel = {W7},
  pubtype = {W},
  pdf = "research/beg2016arch.pdf",
}
@inproceedings{tran2016arch,
  title = {Large-Scale Linear Systems from Order-Reduction (Benchmark Proposal)},
  author = {HD Tran and LV Nguyen and Taylor T. Johnson},
  year = {2016},
  booktitle = {3rd International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'16)},
  volume = {43},
  pages = {60--67},
  publisher = {EasyChair},
  doi = {10.29007/xk7x},
  publabel = {W9},
  pubtype = {W},
  dblp = {conf/cpsweek/TranNJ16},
  s2id = {32070788},
  pdf = "research/tran2016arch.pdf",
}
@inproceedings{sogokon2016arch,
  title = {Non-linear Continuous Systems for Safety Verification (Benchmark Proposal)},
  author = {A Sogokon and K Ghorbal and Taylor T. Johnson},
  year = {2016},
  booktitle = {3rd International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'16)},
  volume = {43},
  pages = {42--51},
  publisher = {EasyChair},
  doi = {10.29007/w94n},
  publabel = {W8},
  pubtype = {W},
  pdf = "research/sogokon2016arch.pdf",
}
@inproceedings{bak2016hscc_demo,
  title = {Demo: Hybrid Systems Model Transformations with HyST},
  author = {S Bak and S Bogomolov and Taylor T. Johnson},
  year = {2016},
  booktitle = {19th ACM International Conference on Hybrid Systems: Computation and Control (HSCC'16)},
  publisher = {ACM},
  publabel = {TALK5},
  pubtype = {TALK},
}
@inproceedings{bak2016hscc,
  title = {Scalable Static Hybridization Methods for Analysis of Nonlinear Systems},
  author = {S Bak and S Bogomolov and TA Henzinger and Taylor T. Johnson and P Prakash},
  year = {2016},
  month = apr,
  booktitle = {19th ACM International Conference on Hybrid Systems: Computation and Control (HSCC'16)},
  pages = {155--164},
  publisher = {ACM},
  doi = {10.1145/2883817.2883837},
  publabel = {C14},
  pubtype = {C},
  dblp = {conf/hybrid/BakBHJP16},
  pdf = "research/bak2016hscc.pdf",
}
@inproceedings{chowdhury2016cyphy,
  title = {CyFuzz: A Differential Testing Framework for Cyber-Physical Systems Development Environments},
  author = {SA Chowdhury and Taylor T. Johnson and C Csallner},
  year = {2016},
  month = oct,
  booktitle = {6th Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy'16)},
  volume = {10107},
  pages = {46--60},
  publisher = {Springer},
  doi = {10.1007/978-3-319-51738-4_4},
  publabel = {W10},
  pubtype = {W},
  dblp = {conf/cyphy/ChowdhuryJC16},
  pdf = "research/chowdhury2016cyphy.pdf",
}
@inproceedings{bak2015hscc_demo,
  title = {HYST: A Source-to-Source Transformation Framework for Hybrid Automata},
  author = {S Bak and S Bogomolov and Taylor T. Johnson},
  year = {2015},
  booktitle = {18th International Conference on Hybrid Systems: Computation and Control (HSCC'15)},
  publabel = {TALK4},
  pubtype = {TALK},
}
@misc{hoefel2015patent,
  title = {Control of a Component of a Downhole Tool},
  author = {A Hoefel and F Bernard and KD Harms and S Ramshaw and S Darayan and Taylor T. Johnson},
  year = {2015},
  howpublished = {US Patent 9,222,352},
  note = {US Patent 9,222,352},
  publabel = {P1},
  pubtype = {P},
  pdf = "research/hoefel2015patent.pdf",
}
@inproceedings{bak2015rtss,
  title = {Periodically-Scheduled Controller Analysis using Hybrid Systems Reachability and Continuization},
  author = {S Bak and Taylor T. Johnson},
  year = {2015},
  month = dec,
  booktitle = {36th IEEE Real-Time Systems Symposium (RTSS'15)},
  pages = {195--205},
  publisher = {IEEE},
  doi = {10.1109/RTSS.2015.26},
  publabel = {C13},
  pubtype = {C},
  dblp = {conf/rtss/BakJ15},
  pdf = "research/bak2015rtss.pdf",
}
@inproceedings{nguyen2015cfv,
  title = {Quantified Bounded Model Checking for Rectangular Hybrid Automata},
  author = {LV Nguyen and D Maksimovic and Taylor T. Johnson and A Veneris},
  year = {2015},
  booktitle = {9th International Workshop on Constraints in Formal Verification (CFV'15)},
  publabel = {W6},
  pubtype = {W},
  pdf = "research/nguyen2015cfv.pdf",
}
@inproceedings{nguyen2015rv,
  title = {Runtime Verification for Hybrid Analysis Tools},
  author = {LV Nguyen and C Schilling and S Bogomolov and Taylor T. Johnson},
  year = {2015},
  month = nov,
  booktitle = {15th International Conference on Runtime Verification (RV'15)},
  volume = {9333},
  pages = {281--286},
  publisher = {Springer},
  doi = {10.1007/978-3-319-23820-3_19},
  publabel = {C12},
  pubtype = {C},
  dblp = {conf/rv/NguyenSBJ15},
  pdf = "research/nguyen2015rv.pdf",
}
@article{johnson2015tcs,
  title = {Safe and stabilizing distributed multi-path cellular flows},
  author = {Taylor T. Johnson and S Mitra},
  year = {2015},
  month = may,
  journal = {Theoretical Computer Science (TCS), Elsevier},
  volume = {579},
  pages = {9--32},
  doi = {10.1016/j.tcs.2015.01.023},
  publabel = {J3},
  pubtype = {J},
  arxiv = {1209.2058},
  dblp = {journals/corr/abs-1209-2058},
  s2id = {16612804},
  pdf = "research/johnson2015tcs.pdf",
}
@inproceedings{tran2015arch,
  title = {Benchmark: A Nonlinear Reachability Analysis Test Set from Numerical Analysis},
  author = {HD Tran and LV Nguyen and Taylor T. Johnson},
  year = {2015},
  booktitle = {2nd International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'15)},
  volume = {34},
  pages = {89--97},
  publisher = {EasyChair},
  doi = {10.29007/6dcf},
  publabel = {W4},
  pubtype = {W},
  dblp = {conf/cpsweek/TranNJ15},
  s2id = {28848801},
  pdf = "research/tran2015arch.pdf",
}
@inproceedings{bak2015arch,
  title = {Benchmark: Stratified Controllers of Tank Networks},
  author = {S Bak and S Bogomolov and M Greitschus and Taylor T. Johnson},
  year = {2015},
  booktitle = {2nd International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'15)},
  volume = {34},
  pages = {73--79},
  publisher = {EasyChair},
  doi = {10.29007/2ljt},
  publabel = {W3},
  pubtype = {W},
  dblp = {conf/cpsweek/BakBGJ15},
  s2id = {38753702},
  pdf = "research/bak2015arch.pdf",
}
@inproceedings{bak2015snr,
  title = {HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models},
  author = {S Bak and S Bogomolov and Taylor T. Johnson},
  year = {2015},
  booktitle = {1st International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR'15)},
  publabel = {W5},
  pubtype = {W},
  dblp = {conf/hybrid/BakBJ15},
  pdf = "research/bak2015snr.pdf",
}
@inproceedings{johnson2015iccps,
  title = {Cyber-Physical Specification Mismatch Identification with Dynamic Analysis},
  author = {Taylor T. Johnson and S Bak and S Drager},
  year = {2015},
  month = apr,
  booktitle = {ACM/IEEE 6th International Conference on Cyber-Physical Systems (ICCPS'15)},
  pages = {208--217},
  publisher = {ACM},
  doi = {10.1145/2735960.2735979},
  publabel = {C11},
  pubtype = {C},
  dblp = {conf/iccps/JohnsonBD15},
  s2id = {8263150},
  pdf = "research/johnson2015iccps.pdf",
}
@inproceedings{bak2015hscc,
  title = {HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models},
  author = {S Bak and S Bogomolov and Taylor T. Johnson},
  year = {2015},
  month = apr,
  booktitle = {18th International Conference on Hybrid Systems: Computation and Control (HSCC'15)},
  pages = {128--133},
  publisher = {ACM},
  doi = {10.1145/2728606.2728630},
  publabel = {C10},
  pubtype = {C},
  dblp = {conf/hybrid/BakBJ15},
  s2id = {2394876},
  pdf = "research/bak2015hscc.pdf",
}
@misc{nguyen2015hscc_poster,
  title = {Poster: HyRG: A Random Generation Tool for Affine Hybrid Automata},
  author = {LV Nguyen and C Schilling and S Bogomolov and Taylor T. Johnson},
  year = {2015},
  howpublished = {18th International Conference on Hybrid Systems: Computation and Control (HSCC'15)},
  note = {18th International Conference on Hybrid Systems: Computation and Control (HSCC'15)},
  pages = {289--290},
  publisher = {ACM},
  doi = {10.1145/2728606.2728650},
  publabel = {D2},
  pubtype = {D},
}
@inproceedings{johnson2015esv,
  title = {A survey of electrical and electronic (e/e) notifications for motor vehicles},
  author = {Taylor T. Johnson and R Gannamaraju and S Fischmeister},
  year = {2015},
  booktitle = {24th International Technical Conference on the Enhanced Safety of Vehicles (ESV'15)},
  pages = {1--15},
  publisher = {NHTSA},
  publabel = {LC6},
  pubtype = {LC},
  pdf = "research/johnson2015esv.pdf",
}
@inproceedings{bobadilla2015scitech,
  title = {Verified Planar Formation Control Algorithms by Composition of Primitives},
  author = {L Bobadilla and Taylor T. Johnson and A LaViers and U Huzaifa},
  year = {2015},
  month = jan,
  booktitle = {AIAA Science and Technology Forum and Exposition (SciTech'15)},
  publisher = {AIAA},
  doi = {10.2514/6.2015-1541},
  publabel = {LC5},
  pubtype = {LC},
  s2id = {62764404},
  pdf = "research/bobadilla2015scitech.pdf",
}
@inproceedings{bak2014rtss,
  title = {Real-Time Reachability for Verified Simplex Design},
  author = {S Bak and Taylor T. Johnson and M Caccamo and L Sha},
  year = {2014},
  month = dec,
  booktitle = {35th IEEE Real-Time Systems Symposium (RTSS'14)},
  pages = {138--148},
  publisher = {IEEE},
  doi = {10.1109/RTSS.2014.21},
  publabel = {C9},
  pubtype = {C},
  dblp = {journals/tecs/JohnsonBCS16},
  pdf = "research/bak2014rtss.pdf",
}
@inproceedings{johnson2014formats,
  title = {Anonymized Reachability of Hybrid Automata Networks},
  author = {Taylor T. Johnson and S Mitra},
  year = {2014},
  month = sep,
  booktitle = {12th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'14)},
  volume = {8711},
  pages = {130--145},
  publisher = {Springer},
  doi = {10.1007/978-3-319-10512-3_10},
  publabel = {C8},
  pubtype = {C},
  dblp = {conf/formats/JohnsonM14},
  pdf = "research/johnson2014formats.pdf",
}
@inproceedings{nguyen2014cyphy,
  title = {Model-based design and analysis of a reconfigurable continuous-culture bioreactor},
  author = {Luan Viet Nguyen and Eric J. Nelson and Amol Vengurlekar and Ruoshi Zhang and Kristopher I. White and Victor Salinas and Taylor T. Johnson},
  year = {2014},
  month = apr,
  booktitle = {4th ACM SIGBED International Workshop on Design, Modeling, and Evaluation of Cyber-Physical Systems (CyPhy'14)},
  pages = {48--51},
  publisher = {ACM},
  doi = {10.1145/2593458.2593469},
  publabel = {W2},
  pubtype = {W},
  dblp = {conf/cyphy/NguyenNVZWSJ14},
  pdf = "research/nguyen2014cyphy.pdf",
}
@inproceedings{nguyen2014arch,
  title = {Benchmark: DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters).},
  author = {LV Nguyen and Taylor T. Johnson},
  year = {2014},
  booktitle = {1st International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'14)},
  volume = {34},
  pages = {19--24},
  publisher = {EasyChair},
  doi = {10.29007/23pm},
  publabel = {W1},
  pubtype = {W},
  dblp = {conf/cpsweek/NguyenJ14},
  s2id = {12114321},
  pdf = "research/nguyen2014arch.pdf",
}
@article{nguyen2014tec,
  title = {Virtual Prototyping for Distributed Control of a Fault-Tolerant Modular Multilevel Inverter for Photovoltaics},
  author = {LV Nguyen and H Tran and Taylor T. Johnson},
  year = {2014},
  month = dec,
  journal = {IEEE Transactions on Energy Conversion (TEC)},
  volume = {29},
  number = {4},
  pages = {841--850},
  publisher = {IEEE},
  doi = {10.1109/TEC.2014.2362716},
  publabel = {J2},
  pubtype = {J},
  pdf = "research/nguyen2014tec.pdf",
}
@phdthesis{johnson2013phdthesis,
  title = {Uniform verification of safety for parameterized networks of hybrid automata},
  author = {Taylor T. Johnson},
  year = {2013},
  school = {University of Illinois at Urbana-Champaign},
  publabel = {TH2},
  pubtype = {TH},
  dblp = {phd/us/Johnson13d},
  pdf = "research/johnson2013phdthesis.pdf",
}
@inproceedings{johnson2013infotech,
  title = {Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Applications to Aerospace Systems},
  author = {Taylor T. Johnson and S Mitra},
  year = {2013},
  month = aug,
  booktitle = {AIAA Infotech at Aerospace},
  pages = {1--16},
  publisher = {AIAA},
  doi = {10.2514/6.2013-4811},
  publabel = {LC4},
  pubtype = {LC},
  s2id = {16939484},
  pdf = "research/johnson2013infotech.pdf",
}
@inproceedings{bogomolov2013spin,
  title = {Abstraction-based guided search for hybrid systems},
  author = {Sergiy Bogomolov and Alexandre Donzé and Goran Frehse and Radu Grosu and Taylor T. Johnson and Hamed Ladan and Andreas Podelski and Martin Wehrle},
  year = {2013},
  booktitle = {20th International SPIN Symposium on Model Checking of Software (SPIN'13)},
  pages = {117--134},
  publisher = {Springer},
  doi = {10.1007/978-3-642-39176-7_8},
  publabel = {C7},
  pubtype = {C},
  gsid = {9142077756418010202},
  dblp = {conf/spin/BogomolovDFGJLPW13},
  pdf = "research/bogomolov2013spin.pdf",
}
@inproceedings{johnson2013hscc_demo,
  title = {Demo: The Passel Verification Tool for Hybrid Automata Networks},
  author = {Taylor T. Johnson and S Mitra},
  year = {2013},
  booktitle = {16th International Conference on Hybrid Systems: Computation and Control (HSCC'13)},
  publabel = {TALK3},
  pubtype = {TALK},
  pdf = "research/johnson2013hscc_demo.pdf",
}
@inproceedings{hossain2013peci,
  title = {Reachability Analysis of Closed Loop Switching Power Converters},
  author = {S Hossain and Taylor T. Johnson and S Dhople},
  year = {2013},
  month = feb,
  booktitle = {IEEE Power and Energy Conference at Illinois (PECI'13)},
  pages = {130--134},
  publisher = {IEEE},
  doi = {10.1109/PECI.2013.6506047},
  publabel = {LC3},
  pubtype = {LC},
  gsid = {8886180814224184900},
  s2id = {31246255},
  pdf = "research/hossain2013peci.pdf",
}
@inproceedings{duggirala2012rtss,
  title = {Static and dynamic analysis of timed distributed traces},
  author = {PS Duggirala and Taylor T. Johnson and A Zimmerman and S Mitra},
  year = {2012},
  month = dec,
  booktitle = {33rd IEEE Real-Time Systems Symposium (RTSS'12)},
  pages = {173--182},
  publisher = {IEEE},
  doi = {10.1109/RTSS.2012.69},
  publabel = {C6},
  pubtype = {C},
  gsid = {7478096960006514961},
  dblp = {conf/rtss/DuggiralaJZM12},
  pdf = "research/duggirala2012rtss.pdf",
}
@inproceedings{johnson2012fm,
  title = {Satellite rendezvous and conjunction avoidance: Case studies in verification of nonlinear hybrid systems},
  author = {Taylor T. Johnson and J Green and S Mitra and R Dudley and RS Erwin},
  year = {2012},
  month = aug,
  booktitle = {International Symposium on Formal Methods (FM'12)},
  volume = {7436},
  pages = {252--266},
  publisher = {Springer},
  doi = {10.1007/978-3-642-32759-9_22},
  publabel = {C5},
  pubtype = {C},
  gsid = {6661230319939383532},
  dblp = {conf/fm/JohnsonGMDE12},
  s2id = {12530299},
  pdf = "research/johnson2012fm.pdf",
}
@inproceedings{johnson2012iccps,
  title = {Parameterized verification of distributed cyber-physical systems: An aircraft landing protocol case study},
  author = {Taylor T. Johnson and S Mitra},
  year = {2012},
  month = apr,
  booktitle = {3rd ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS'12)},
  pages = {161--170},
  publisher = {IEEE},
  doi = {10.1109/ICCPS.2012.24},
  publabel = {C3},
  pubtype = {C},
  gsid = {11740586308134469378},
  pdf = "research/johnson2012iccps.pdf",
}
@inproceedings{johnson2012peci,
  title = {Design Verification Methods for Switching Power Converters},
  author = {Taylor T. Johnson and Z Hong and A Kapoor},
  year = {2012},
  month = feb,
  booktitle = {IEEE Power and Energy Conference at Illinois (PECI'12)},
  pages = {1--6},
  publisher = {IEEE},
  doi = {10.1109/PECI.2012.6184587},
  publabel = {LC2},
  pubtype = {LC},
  gsid = {17399493867618088222},
  pdf = "research/johnson2012peci.pdf",
}
@inproceedings{johnson2012forte,
  title = {A small model theorem for rectangular hybrid automata networks},
  author = {Taylor T. Johnson and S Mitra},
  year = {2012},
  month = jun,
  booktitle = {IFIP International Conference on Formal Techniques for Distributed Systems: Joint International Conference of 14th Formal Methods for Open Object-Based Distributed Systems and 32nd Formal Techniques for Networked and Distributed Systems (FORTE/FMOODS'12)},
  volume = {7273},
  pages = {18--34},
  publisher = {Springer},
  doi = {10.1007/978-3-642-30793-5_2},
  publabel = {C4},
  pubtype = {C},
  gsid = {4606381030313410526},
  dblp = {conf/forte/JohnsonM12},
  s2id = {278853},
  pdf = "research/johnson2012forte.pdf",
}
@inproceedings{johnson2011peci,
  title = {Turbo-alternator stalling protection using available-power estimate},
  author = {Taylor T. Johnson and AE Hoefel},
  year = {2011},
  month = feb,
  booktitle = {IEEE Power and Energy Conference at Illinois (PECI'11)},
  pages = {1--6},
  publisher = {IEEE},
  doi = {10.1109/PECI.2011.5740501},
  publabel = {LC1},
  pubtype = {LC},
  gsid = {14808654063079790680},
  s2id = {24370179},
  pdf = "research/johnson2011peci.pdf",
}
@article{johnson2011jnsa,
  title = {Safe Flocking in Spite of Actuator Faults using Directional Failure Detectors},
  author = {Taylor T. Johnson and S Mitra},
  year = {2011},
  journal = {Journal of Nonlinear Systems and Applications, Watam Press},
  volume = {2},
  number = {1-2},
  pages = {73--95},
  publabel = {J1},
  pubtype = {J},
  gsid = {17168942288498640040},
  pdf = "research/johnson2011jnsa.pdf",
}
@inproceedings{johnson2011cdc,
  title = {Stability of Digitally Interconnected Linear Systems},
  author = {Taylor T. Johnson and S Mitra and C Langbort},
  year = {2011},
  month = dec,
  booktitle = {50th IEEE Conference on Decision and Control (CDC'11)},
  pages = {2687--2692},
  publisher = {IEEE},
  doi = {10.1109/CDC.2011.6161264},
  publabel = {OC1},
  pubtype = {OC},
  gsid = {14666544104064248628},
  dblp = {conf/cdc/JohnsonML11},
  s2id = {2453216},
  pdf = "research/johnson2011cdc.pdf",
}
@misc{johnson2011poster,
  title = {Verification of Distributed Cyber-Physical Systems: Stability of Digitally Interconnected Linear Systems},
  author = {Taylor T. Johnson and S Mitra and C Langbort},
  year = {2011},
  publabel = {TALK2},
  pubtype = {TALK},
}
@inproceedings{johnson2010icdcs,
  title = {Safe and stabilizing distributed cellular flows},
  author = {Taylor T. Johnson and S Mitra and K Manamcheri},
  year = {2010},
  month = jun,
  booktitle = {30th IEEE International Distributed Computing Systems (ICDCS'10)},
  pages = {577--586},
  publisher = {IEEE},
  doi = {10.1109/ICDCS.2010.49},
  publabel = {C1},
  pubtype = {C},
  gsid = {12377696546842138389},
  dblp = {conf/icdcs/JohnsonMM10},
  pdf = "research/johnson2010icdcs.pdf",
}
@mastersthesis{johnson2010msthesis,
  title = {Fault-tolerant distributed cyber-physical systems: Two case studies},
  author = {Taylor T. Johnson},
  year = {2010},
  school = {University of Illinois at Urbana-Champaign},
  publabel = {TH1},
  pubtype = {TH},
  gsid = {9683503763763426403},
  pdf = "research/johnson2010msthesis.pdf",
}
@techreport{johnson2010tr,
  title = {Safe and stabilizing distributed flocking in spite of actuator faults},
  author = {Taylor T. Johnson and S Mitra},
  year = {2010},
  institution = {Coordinated Science Laboratory Report no. UILU-ENG-10-2204},
  publabel = {R2},
  pubtype = {R},
  pdf = "research/johnson2010tr.pdf",
}
@inproceedings{johnson2010sss,
  title = {Safe flocking in spite of actuator faults},
  author = {Taylor T. Johnson and S Mitra},
  year = {2010},
  month = sep,
  booktitle = {Stabilization, Safety, and Security of Distributed Systems (SSS'10)},
  volume = {6366},
  pages = {588--602},
  publisher = {Springer},
  doi = {10.1007/978-3-642-16023-3_45},
  publabel = {C2},
  pubtype = {C},
  gsid = {14477781552252082549},
  dblp = {conf/sss/JohnsonM10},
  s2id = {17948270},
  pdf = "research/johnson2010sss.pdf",
}
@inproceedings{johnson2009rtss,
  title = {Handling Failures in Cyber-Physical Systems: Potential Directions},
  author = {Taylor T. Johnson and S Mitra},
  year = {2009},
  booktitle = {Real-Time Systems Symposium (RTSS'09)},
  publabel = {E1},
  pubtype = {E},
  gsid = {18127665186175310638},
  pdf = "research/johnson2009rtss.pdf",
}
@inproceedings{johnson2009rtas,
  title = {Poster Abstract: Power Usage of Time and Event-Triggered Paradigms: A Case Study},
  author = {Taylor T. Johnson and S Mitra},
  year = {2009},
  booktitle = {Real-Time and Embedded Technology and Applications Symposium (RTAS'09)},
  publabel = {TALK1},
  pubtype = {TALK},
  gsid = {1931943751823825557},
  pdf = "research/johnson2009rtas.pdf",
}
@techreport{johnson2008tr,
  title = {Stability Analysis of Simplex Architecture Controlled Inverted Pendulum},
  author = {Taylor T. Johnson},
  year = {2008},
  institution = {Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign},
  publabel = {R1},
  pubtype = {R},
}
@inproceedings{johnson2025allerton,
  title = {Is Neural Network Verification Useful and What Is Next?},
  author = {Taylor T. Johnson},
  year = {2025},
  month = sep,
  booktitle = {61st Allerton Conference on Communication, Control, and Computing},
  url = {https://hdl.handle.net/2142/130315},
  publabel = {LC10},
  pubtype = {LC},
  pdf = "research/johnson2025allerton.pdf",
}
@inproceedings{wang2025ficc,
  title = {Robustness Verification for Knowledge-Based Logic of Risky Driving Scenes},
  author = {Xia Wang and Anda Liang and Jonathan Sprinkle and Taylor T. Johnson},
  year = {2025},
  booktitle = {Future of Information and Communication Conference (FICC 2025)},
  pages = {572--585},
  doi = {10.1007/978-3-031-84460-7_36},
  publabel = {OC22},
  pubtype = {OC},
  dblp = {conf/ficc/WangLSJ25},
}
@inproceedings{zubair2025cai,
  title = {Verification of Neural Network Robustness Against Weight Perturbations Using Star Sets},
  author = {Muhammad Usama Zubair and Taylor T. Johnson and Kanad Basu and Waseem Abbas},
  year = {2025},
  booktitle = {IEEE Conference on Artificial Intelligence (CAI 2025)},
  pages = {637--642},
  doi = {10.1109/CAI64502.2025.00117},
  publabel = {OC21},
  pubtype = {OC},
  dblp = {conf/ieeecai/ZubairJBA25},
  s2id = {279986902},
}
@inproceedings{an2025aamas,
  title = {Combining LLMs with a Logic-Based Framework to Explain MCTS},
  author = {Ziyan An and Xia Wang and Hendrik Baier and Zirong Chen and Abhishek Dubey and Jonathan Sprinkle and Ayan Mukhopadhyay and Meiyi Ma and Taylor T. Johnson},
  year = {2025},
  booktitle = {24th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2025)},
  pages = {2405--2407},
  doi = {10.65109/jwwj9232},
  publabel = {OC20},
  pubtype = {OC},
  dblp = {conf/ifaamas/AnWBCDJSMM25},
}
@inproceedings{an2025rv,
  title = {ISL: Monitoring Image Segmentation Logic in Medical Imaging Analysis},
  author = {Ziyan An and Daniel Moyer and Ipek Oguz and Meiyi Ma and Taylor T. Johnson},
  year = {2025},
  booktitle = {25th International Conference on Runtime Verification (RV 2025)},
  pages = {477--496},
  doi = {10.1007/978-3-032-05435-7_26},
  publabel = {OC19},
  pubtype = {OC},
  dblp = {conf/rv/AnMOJM25},
  pdf = "research/an2025rv.pdf",
}
@inproceedings{lopez2025saiv,
  title = {NNV: A Star Set Reachability Approach (Competition Contribution)},
  author = {Diego Manzanas Lopez and Samuel Sasaki and Taylor T. Johnson},
  year = {2025},
  booktitle = {2nd International Symposium on AI Verification (SAIV 2025)},
  pages = {260--265},
  doi = {10.1007/978-3-031-99991-8_15},
  publabel = {W33},
  pubtype = {W},
  dblp = {conf/saiv/LopezSJ25},
}
@inproceedings{kaulen2025vnncomp,
  title = {The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results},
  author = {Konstantin Kaulen and Tobias Ladner and Stanley Bak and Christopher Brix and Hai Duong and Thomas Flinkow and Taylor T. Johnson and Lukas Koller and Edoardo Manino and ThanhVu H. Nguyen and Haoze Wu},
  year = {2025},
  booktitle = {2nd International Symposium on AI Verification (SAIV 2025)},
  publabel = {W32},
  pubtype = {W},
  dblp = {journals/corr/abs-2512-19007},
  pdf = "research/kaulen2025vnncomp.pdf",
}
@inproceedings{nguyen2015hscc,
  title = {HyRG: a random generation tool for affine hybrid automata},
  author = {Luan Viet Nguyen and Christian Schilling and Sergiy Bogomolov and Taylor T. Johnson},
  year = {2015},
  month = apr,
  booktitle = {18th International Conference on Hybrid Systems: Computation and Control (HSCC'15)},
  pages = {289--290},
  doi = {10.1145/2728606.2728650},
  publabel = {OW1},
  pubtype = {OW},
  gsid = {15770939070662677354},
  pdf = "research/nguyen2015hscc.pdf",
}