People

Principal Investigator

• 
  Taylor T. Johnson

  Formal verification of neural networks and cyber-physical systems, hybrid and switched systems, and safe, trustworthy autonomy

  WebsiteLinkedInGitHubGoogle ScholarX (Twitter)Stack OverflowORCIDDBLPResearchGate

  223 papers, 38 first-author

  • Control Barrier Function Synthesis for Differential-Algebraic Systems (2026)
  • Safe Control of Semi-Explicit Differential-Algebraic Systems: Control Barrier Functions with SO... (2026)
  • Safe Autonomous Takeover for Unknown Descriptor Systems (2026)
  • NNV3: Expanding Neural Network Verification to New Architectures and Domains (2026)
  • Indelible Backdoors: On the Limits of Post-Training Defenses (2026)
  • MetaMoE: Formal Verification of Compositional Robustness and Scalability of Mixture-of-Experts ... (2026)
  • A Self-correcting Neuro-symbolic AI Reasoning Framework (2026)
  • Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features (2026)
  • Modeling Spectral Energy Shifts in Spatio-Temporal Graph Anomaly Detection (2026)
  • MorphoMod: Visible Watermark Removal with Morphological Dilation (2026)
  • Reward Shaping and Action Masking for Compositional Tasks using Behavior Trees and LLMs (2026)
  • k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics (2026)
  • +211 more

Postdoctoral Research Associates and Research Scientists

• 
  Ben Wooding

  Postdoctoral researcher · Fall 2025 – Present

  Develops barrier certificates and abstraction-based controller synthesis for formal safety guarantees on unknown, stochastic dynamics

  WebsiteLinkedInGitHubGoogle ScholarORCIDDBLP

  8 papers, 3 first-author

  • Control Barrier Function Synthesis for Differential-Algebraic Systems (2026)
  • Safe Control of Semi-Explicit Differential-Algebraic Systems: Control Barrier Functions with SO... (2026)
  • Safe Autonomous Takeover for Unknown Descriptor Systems (2026)
  • NNV3: Expanding Neural Network Verification to New Architectures and Domains (2026)
  • MetaMoE: Formal Verification of Compositional Robustness and Scalability of Mixture-of-Experts ... (2026)
  • A Self-correcting Neuro-symbolic AI Reasoning Framework (2026)
  • Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features (2026)
  • k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics (2026)
• 
  Hongchao Zhang

  Postdoctoral researcher · Fall 2025 – Present

  co-advised with Prof. Ahmad Taha and Prof. Meiyi Ma; Learning and Verification for Differential Algebraic Equations (DAEs); Verifies and synthesizes neural control barrier functions for safe cyber-physical systems under faults and attacks

  WebsiteLinkedInGitHubGoogle ScholarORCID

  7 papers, 1 first-author

  • Control Barrier Function Synthesis for Differential-Algebraic Systems (2026)
  • Safe Control of Semi-Explicit Differential-Algebraic Systems: Control Barrier Functions with SO... (2026)
  • Safe Autonomous Takeover for Unknown Descriptor Systems (2026)
  • NNV3: Expanding Neural Network Verification to New Architectures and Domains (2026)
  • A Self-correcting Neuro-symbolic AI Reasoning Framework (2026)
  • Modeling Spectral Energy Shifts in Spatio-Temporal Graph Anomaly Detection (2026)
  • k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics (2026)

PhD Students

• KG
  Kendra Givens

  PhD student · Summer 2026 – Present

  co-advised with Bryan Ward

  LinkedInDBLP
• LN
  Luke Nam

  PhD student · Spring 2026 – Present

  Works on formal verification of neural network architectures, including robustness verification of mixture-of-experts models

  WebsiteLinkedInDBLP

  1 paper

  • MetaMoE: Formal Verification of Compositional Robustness and Scalability of Mixture-of-Experts ... (2026)
• 
  Michaela Winfree

  PhD student · Fall 2025 – Present

  co-advised with Prof. Gautam Biswas

  Google ScholarDBLP
• 
  Thuy Dung (Judy) Nguyen

  PhD student · Fall 2023 – Present

  co-advised with Prof. Kevin Leach; Robust federated and adversarial machine learning; Studies backdoor attacks, purification defenses, and generative unlearning in federated and adversarial machine learning

  WebsiteLinkedInGitHubGoogle ScholarORCIDDBLP

  7 papers, 4 first-author

  • Indelible Backdoors: On the Limits of Post-Training Defenses (2026)
  • SUGAR: A Sweeter Spot for Generative Unlearning of Many Identities (2026)
  • LOGSAFE: Logic-Guided Verification for Trustworthy Federated Time-Series Learning (2026)
  • Trigger-Based Fragile Model Watermarking for Image Transformation Networks (2025)
  • Neuro-Symbolic Behavior Trees and Their Verification (2025)
  • PARDON: Privacy-Aware and Robust Federated Domain Generalization (2025)
  • PBP: Post-training Backdoor Purification for Malware Classifiers (2025)
• 
  Samuel Sasaki

  PhD student · Fall 2023 – Present

  Verifies robustness of video classification and segmentation neural networks, and builds neurosymbolic automata for multimodal reasoning

  WebsiteGitHubDBLP

  7 papers, 2 first-author

  • NNV3: Expanding Neural Network Verification to New Architectures and Domains (2026)
  • MetaMoE: Formal Verification of Compositional Robustness and Scalability of Mixture-of-Experts ... (2026)
  • Scaling Data-Driven Probabilistic Robustness Analysis for Semantic Segmentation Neural Networks (2025)
  • Trigger-Based Fragile Model Watermarking for Image Transformation Networks (2025)
  • Neurosymbolic Finite and Pushdown Automata: Improved Multimodal Reasoning versus Vision Languag... (2025)
  • Robustness Verification of Video Classification Neural Networks (2025)
  • NNV: A Star Set Reachability Approach (Competition Contribution) (2025)
• 
  Anne Tumlin

  PhD student · Fall 2023 – Present

  co-advised with Prof. Tyler Derr; Fairness verification in graph neural networks; Applies formal verification to graph neural networks in power systems and certifies fairness properties of machine learning models

  WebsiteLinkedInGitHubORCIDDBLP

  5 papers, 3 first-author

  • NNV3: Expanding Neural Network Verification to New Architectures and Domains (2026)
  • A Self-correcting Neuro-symbolic AI Reasoning Framework (2026)
  • Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features (2026)
  • Verification of Behavior Trees with Contingency Monitors (2024)
  • FairNNV: The Neural Network Verification Tool For Certifying Fairness (2024)

Undergraduate Researchers

• CC
  Caleb Ching

  Undergraduate researcher · Summer 2026 – Present
• JF
  Jamie Fong

  Undergraduate researcher · Summer 2026 – Present
• ZZ
  Zichen Zhu

  Undergraduate researcher · Summer 2026 – Present

  Spiking neural network (SNN) verification

Postdoctoral Research Associate Alumni

• NH
  Navid Hashemi

  Postdoctoral researcher · Spring 2025 – Fall 2025

  Neural network verification and neuro-symbolic AI; neural, scaling data, driven probabilistic, robustness analysis, semantic segmentation, networks

  LinkedInGoogle ScholarDBLP

  2 papers, 1 first-author

  • NNV3: Expanding Neural Network Verification to New Architectures and Domains (2026)
  • Scaling Data-Driven Probabilistic Robustness Analysis for Semantic Segmentation Neural Networks (2025)
• 
  Tianshu Bao

  Postdoctoral researcher · Fall 2023 – Fall 2025

  Builds physics-informed and PDE-driven neural networks for traffic forecasting, streamflow prediction, and turbulent-flow reconstruction

  WebsiteLinkedInGitHubGoogle ScholarORCIDDBLP

  6 papers, 5 first-author

  • Uncertainty Quantification for Physics-Informed Traffic Graph Networks (2025)
  • Spatial-Temporal PDE Networks for Traffic Flow Forecasting (2024)
  • Transfer Learning Using Inaccurate Physics Rule for Streamflow Prediction (2024)
  • Physics Guided Neural Networks for Spatio-temporal Super-resolution of Turbulent Flows (2022)
  • Partial Differential Equation Driven Dynamic Graph Networks for Predicting Stream Water Tempera... (2021)
  • Discrete-Space Analysis of Partial Differential Equations (PDEs) (Benchmark Proposal) (2018)
• 
  Diego Manzanas Lopez

  Postdoctoral researcher · Fall 2022 – Fall 2025

  Works on formal assurance of AI, applying reachability-based verification to neural networks and learning-enabled cyber-physical systems; now: Applied Scientist, Amazon

  WebsiteLinkedInGitHubGoogle ScholarORCIDDBLP

  45 papers, 13 first-author

  • NNV3: Expanding Neural Network Verification to New Architectures and Domains (2026)
  • Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features (2026)
  • Toward Assured Autonomy Using Neurosymbolic Components and Systems (2026)
  • Towards Verified and Targeted Explanations through Formal Methods (2026)
  • Real-Time Reachability for Neurosymbolic Reinforcement Learning based Safe Autonomous Navigatio... (2025)
  • Neurosymbolic Finite and Pushdown Automata: Improved Multimodal Reasoning versus Vision Languag... (2025)
  • Neuro-Symbolic Behavior Trees and Their Verification (2025)
  • Robustness Verification of Video Classification Neural Networks (2025)
  • NNV: A Star Set Reachability Approach (Competition Contribution) (2025)
  • Parallel Verification of Neural Networks Applied to Medical Imaging (Research Poster) (2024)
  • FairNNV: The Neural Network Verification Tool For Certifying Fairness (2024)
  • ARCH-COMP24 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS... (2024)
  • +33 more
• 
  Joel Rosenfeld

  Postdoctoral researcher · 8/2017 – 8/2019

  Optimization-Based Verification for Cyber-Physical Systems; Develops occupation kernel and Liouville operator methods in RKHSs for nonlinear system identification and dynamic mode decomposition; next: Assistant Professor, Mathematics and Statistics, University of South Florida; now: Associate Professor, Department of Mathematics and Statistics, University of South Florida

  WebsiteGoogle ScholarORCIDDBLP

  4 papers, 3 first-author

  • Dynamic Mode Decomposition for Continuous Time Systems with the Liouville Operator (2022)
  • On Occupation Kernels, Liouville Operators, and Dynamic Mode Decomposition (2021)
  • Occupation Kernels and Densely Defined Liouville Operators for System Identification (2019)
  • Verification for Machine Learning, Autonomy, and Neural Networks Survey (2018)
• 
  Khaza Anuarul Hoque

  Postdoctoral researcher · 3/2016 – 8/2016

  Formal Verification for Aerospace CPS; Works on formal methods, hardware security, and dependable edge AI, including DNN fault robustness and trustworthy VR/XR systems; next: Research Fellow at Oxford University; now: Assistant Professor, Electrical Engineering and Computer Science (EECS) at University of Missouri Columbia

  WebsiteLinkedInGoogle ScholarORCIDDBLP

  3 papers

  • Cyber-Physical Specification Mismatches (2018)
  • Formal Specification and Dependability Analysis of Optical Communication Networks (2017)
  • Probabilistic formal verification of the SATS concept of operation (2016)
• 
  Andrew Sogokon

  Postdoctoral researcher · 1/2016 – 5/2017

  Liveness Verification for Hybrid Automata; Formal verification of hybrid and continuous dynamical systems, including continuous invariant generation and safety and liveness proofs; next: Postdoc at Carnegie Mellon University; now: Lecturer at the University of Southampton, UK

  WebsiteGitHubGoogle ScholarORCIDDBLP

  6 papers, 5 first-author

  • Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants (2019)
  • Operational Models for Piecewise-Smooth Systems (2017)
  • Verifying safety and persistence properties of hybrid systems using flowpipes and continuous in... (2017)
  • Decoupling Abstractions of Non-linear Ordinary Differential Equations (2016)
  • Tutorial: software tools for hybrid systems verification, transformation, and synthesis: C2E2, ... (2016)
  • Non-linear Continuous Systems for Safety Verification (Benchmark Proposal) (2016)
• 
  Weiming Xiang

  Postdoctoral researcher · 11/2015 – 8/2019

  Unbounded-Time Reachability Analysis for Switched Systems; Formal verification and reachability analysis for neural networks, switched systems, and learning-enabled cyber-physical systems; next: Assistant Professor, School of Computer and Cyber Sciences, Augusta University; now: Associate Professor, School of Computer and Cyber Sciences, Augusta University

  WebsiteLinkedInGitHubGoogle ScholarX (Twitter)ORCIDDBLP

  32 papers, 15 first-author

  • Real-Time Verification for Distributed Cyber-Physical Systems (2022)
  • Verification Approaches for Learning-Enabled Autonomous Cyber-Physical Systems (2022)
  • Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter (2021)
  • Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach (2021)
  • Verification of Deep Convolutional Neural Networks Using ImageStars (2020)
  • NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-P... (2020)
  • NNV Demo: A Neural Network Verification Tool (2020)
  • Star-Based Reachability Analysis of Deep Neural Networks (2019)
  • Real-Time Verification for Distributed Cyber-Physical Systems (2019)
  • Reachability Analysis for High-Index Linear Differential Algebraic Equations (2019)
  • Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems (2019)
  • Parallelizable reachability analysis algorithms for feed-forward neural networks (2019)
  • +20 more

PhD Alumni

• 
  Preston Robinette

  PhD student · Fall 2020 – May 2025

  Robustness verification in steganography and watermarking neural networks; Studies robustness verification of neural networks for steganography, watermarking, and malware detection; 2021 NDSEG Fellowship ($500k); next: Google DeepMind; now: Google DeepMind

  WebsiteLinkedInGitHubGoogle ScholarORCIDDBLP

  16 papers, 9 first-author

  • MorphoMod: Visible Watermark Removal with Morphological Dilation (2026)
  • Towards Verified and Targeted Explanations through Formal Methods (2026)
  • SUGAR: A Sweeter Spot for Generative Unlearning of Many Identities (2026)
  • We Are What We Repeatedly Do: Improving Long Context Instruction Following (2026)
  • Trigger-Based Fragile Model Watermarking for Image Transformation Networks (2025)
  • Robustness Verification of Video Classification Neural Networks (2025)
  • Formalizing Stateful Behavior Trees (2024)
  • FairNNV: The Neural Network Verification Tool For Certifying Fairness (2024)
  • Sanitizing Hidden Information with Diffusion Models (2024)
  • Case Study: Neural Network Malware Detection Verification for Feature and Image Datasets (2024)
  • Benchmark: neural network malware classification (2023)
  • SUDS: Sanitizing Universal and Dependent Steganography (2023)
  • +4 more
• 
  Neelanjana Pal

  PhD student · Summer 2019 – Fall 2023

  Robustness verification in time-series neural networks; Verifies robustness of time-series, audio, and semantic segmentation neural networks using star-set reachability analysis; now: AI Researcher, Princeton IT Services, Inc

  WebsiteLinkedInGitHubGoogle ScholarORCIDDBLP

  6 papers, 4 first-author

  • Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach (2023)
  • Benchmark: formal verification of semantic segmentation neural networks (2023)
  • Robustness verification of deep neural networks using star-based reachability analysis with var... (2023)
  • Safety and Robustness Verification of Autoencoder based Regression Model using NNV Tool (2021)
  • Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter (2021)
  • Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability (2021)
• 
  Serena Serbinowska

  PhD student · Summer 2019 – Summer 2025

  Hyperproperties in adversarial machine learning and cyber-physical systems; Formally verifies behavior trees for robotic mission planning, building the BehaVerify tool that compiles them to nuXmv models; now: Research Engineer on contract to Toyota

  LinkedInGitHubORCIDDBLP

  6 papers, 4 first-author

  • Toward Assured Autonomy Using Neurosymbolic Components and Systems (2026)
  • Neuro-Symbolic Behavior Trees and Their Verification (2025)
  • Verification of Behavior Trees with Contingency Monitors (2024)
  • Formalizing Stateful Behavior Trees (2024)
  • Case Study: Neural Network Malware Detection Verification for Feature and Image Datasets (2024)
  • BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees (2022)
• TB
  Tianshu Bao

  PhD student · Fall 2017 – Summer 2023

  networks, physics, traffic, graph, temporal, partial differential

  WebsiteLinkedInGoogle ScholarDBLP

  6 papers, 5 first-author

  • Uncertainty Quantification for Physics-Informed Traffic Graph Networks (2025)
  • Spatial-Temporal PDE Networks for Traffic Flow Forecasting (2024)
  • Transfer Learning Using Inaccurate Physics Rule for Streamflow Prediction (2024)
  • Physics Guided Neural Networks for Spatio-temporal Super-resolution of Turbulent Flows (2022)
  • Partial Differential Equation Driven Dynamic Graph Networks for Predicting Stream Water Tempera... (2021)
  • Discrete-Space Analysis of Partial Differential Equations (PDEs) (Benchmark Proposal) (2018)
• 
  Nathaniel (Nate) Hamilton

  PhD student · Summer 2017 – Summer 2022

  Works on safe reinforcement learning and run-time assurance for aircraft and spacecraft control policies; now: Reinforcement Learning Engineer, University of Dayton Research Institute

  WebsiteLinkedInGitHubGoogle ScholarORCIDDBLP

  13 papers, 4 first-author

  • Ablation Study of How Run Time Assurance Impacts the Training and Performance of Reinforcement ... (2023)
  • Self-Preserving Genetic Algorithms for Safe Learning in Discrete Action Spaces (2023)
  • Training Agents to Satisfy Timed and Untimed Signal Temporal Logic Specifications with Reinforc... (2022)
  • Reachability Analysis of a General Class of Neural Ordinary Differential Equations (2022)
  • Reinforcement Learning Heuristics for Aerospace Control Systems (2022)
  • Zero-Shot Policy Transfer in Autonomous Racing: Reinforcement Learning versus Imitation Learnin... (2022)
  • On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers (2022)
  • Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability (2021)
  • Sonic to knuckles: evaluations on transfer reinforcement learning (2020)
  • Case Study: Safety Verification of an Unmanned Underwater Vehicle (2020)
  • Reachability Analysis for High-Index Linear Differential Algebraic Equations (2019)
  • Verification for Machine Learning, Autonomy, and Neural Networks Survey (2018)
  • +1 more
• DM
  Diego Manzanas Lopez

  PhD student · Fall 2017 – Summer 2022

  now: Applied Scientist, Amazon; neural, systems, network, verification, control, artificial intelligence

  WebsiteLinkedInGoogle ScholarDBLP

  45 papers, 13 first-author

  • NNV3: Expanding Neural Network Verification to New Architectures and Domains (2026)
  • Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features (2026)
  • Toward Assured Autonomy Using Neurosymbolic Components and Systems (2026)
  • Towards Verified and Targeted Explanations through Formal Methods (2026)
  • Real-Time Reachability for Neurosymbolic Reinforcement Learning based Safe Autonomous Navigatio... (2025)
  • Neurosymbolic Finite and Pushdown Automata: Improved Multimodal Reasoning versus Vision Languag... (2025)
  • Neuro-Symbolic Behavior Trees and Their Verification (2025)
  • Robustness Verification of Video Classification Neural Networks (2025)
  • NNV: A Star Set Reachability Approach (Competition Contribution) (2025)
  • Parallel Verification of Neural Networks Applied to Medical Imaging (Research Poster) (2024)
  • FairNNV: The Neural Network Verification Tool For Certifying Fairness (2024)
  • ARCH-COMP24 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS... (2024)
  • +33 more
• 
  Patrick Musau

  PhD student · Fall 2017 – Spring 2022

  Works on real-time reachability and runtime safety assurance for autonomous cyber-physical systems and learning-enabled controllers; now: Software Engineer, Google

  WebsiteLinkedInGitHubGoogle ScholarDBLP

  25 papers, 3 first-author

  • Online Reachability Analysis and Space Convexification for Autonomous Racing (2023)
  • Reachability Analysis of a General Class of Neural Ordinary Differential Equations (2022)
  • Real-Time Verification for Distributed Cyber-Physical Systems (2022)
  • Zero-Shot Policy Transfer in Autonomous Racing: Reinforcement Learning versus Imitation Learnin... (2022)
  • On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers (2022)
  • Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter (2021)
  • Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability (2021)
  • ARCH-COMP20 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS... (2020)
  • NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-P... (2020)
  • NNV Demo: A Neural Network Verification Tool (2020)
  • Case Study: Safety Verification of an Unmanned Underwater Vehicle (2020)
  • Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control (2019)
  • +13 more
• 
  Xiaodong Yang

  PhD student · Fall 2017 – Summer 2022

  Verifies and repairs deep neural networks using reachability analysis; author of the Veritex neural network repair tool; now: Visa Research (Trustworthy AI), Visa Inc

  LinkedInGitHubGoogle Scholar

  12 papers, 4 first-author

  • Metacognition with Neural Network Verification and Repair using Veritex (2025)
  • Neural Network Repair with Reachability Analysis (2022)
  • A Framework for Identification and Validation of Affine Hybrid Automata from Input-Output Trace... (2022)
  • Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter (2021)
  • Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability (2021)
  • Reachability Analysis of Deep ReLU Neural Networks using Facet-Vertex Incidence (2021)
  • NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-P... (2020)
  • NNV Demo: A Neural Network Verification Tool (2020)
  • Star-Based Reachability Analysis of Deep Neural Networks (2019)
  • Parallelizable reachability analysis algorithms for feed-forward neural networks (2019)
  • Reachability Analysis and Safety Verification for Neural Network Control Systems (2019)
  • Verification for Machine Learning, Autonomy, and Neural Networks Survey (2018)
• 
  Shafiul Chowdhury

  PhD student · Fall 2015 – Fall 2019

  co-advised with Prof. Christoph Csallner; Randomized Differential Testing for CPS Development Environments; Automated testing of cyber-physical system tool chains; built SLforge and SLEMI to find compiler bugs in MATLAB/Simulink; next: Research Scientist, Facebook; now: AI/ML Research Scientist, Meta

  WebsiteLinkedInGitHubGoogle ScholarORCIDDBLP

  2 papers, 2 first-author

  • Demo: SLEMI: Finding Simulink Compiler Bugs through Equivalence Modulo Input (EMI) (2020)
  • SLEMI: Equivalence Modulo Input (EMI) Based Mutation of CPS Models for Finding Compiler Bugs in... (2020)
• 
  Hoang-Dung Tran

  PhD student · Spring 2015 – Summer 2020

  Formal Verification of Distributed Cyber-Physical Systems; Verifies deep neural networks and learning-enabled cyber-physical systems via star-set reachability; co-created the NNV and StarV tools; next: Assistant Professor, Computer Science and Engineering, University of Nebraska Lincoln; now: Assistant Professor, Computer and Information Science and Engineering, University of Florida

  WebsiteGoogle ScholarORCIDDBLP

  53 papers, 24 first-author

  • Tutorial: Safe, Secure, and Trustworthy Artificial Intelligence (AI) via Formal Verification of... (2024)
  • Tutorial: Verification and Validation of Neural Networks in Automated Vehicles using the Neural... (2023)
  • Tutorial: Neural Network and Autonomous Cyber-Physical Systems Formal Verification for Trustwor... (2023)
  • NNV 2.0: The Neural Network Verification Tool (2023)
  • Decentralized Safe Control for Distributed Cyber-Physical Systems using Real-time Reachability ... (2023)
  • Evaluation of Neural Network Verification Methods for Air-to-Air Collision Avoidance (2023)
  • Neural Network Repair with Reachability Analysis (2022)
  • Real-Time Verification for Distributed Cyber-Physical Systems (2022)
  • Verification Approaches for Learning-Enabled Autonomous Cyber-Physical Systems (2022)
  • Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter (2021)
  • Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability (2021)
  • Reachability Analysis of Deep ReLU Neural Networks using Facet-Vertex Incidence (2021)
  • +41 more
• 
  Omar Beg

  PhD student · Summer 2014 – Summer 2017

  co-advised with Prof. Ali Davoudi; Reachability Analysis of Power Electronics and Systems; Applies formal methods and machine learning to detect cyber attacks and improve resilience in microgrids and power electronic systems; next: Assistant Professor at University of Texas at Permian Basin; now: Associate Professor and Department Chair, University of Texas Permian Basin

  WebsiteLinkedInGitHubGoogle ScholarORCIDDBLP

  3 papers, 2 first-author

  • A Framework for Identification and Validation of Affine Hybrid Automata from Input-Output Trace... (2022)
  • Cyber-Physical Anomaly Detection in Microgrids Using Time-Frequency Logic Formalism (2021)
  • Formal Online Resiliency Monitoring in Microgrids (2020)
• 
  Luan Viet Nguyen

  PhD student · Spring 2014 – Summer 2018

  Specifications for Cyber-Physical Systems; Works on formal verification, logic-guided testing, and specification mining for cyber-physical systems and hyperproperties; next: Postdoc at University of Pennsylvania, then Postdoc at University of Notre Dame; now: Assistant Professor at University of Dayton

  WebsiteLinkedInGitHubGoogle ScholarORCIDDBLP

  31 papers, 12 first-author

  • Decentralized Safe Control for Distributed Cyber-Physical Systems using Real-time Reachability ... (2023)
  • Real-Time Verification for Distributed Cyber-Physical Systems (2022)
  • Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter (2021)
  • Cyber-Physical Anomaly Detection in Microgrids Using Time-Frequency Logic Formalism (2021)
  • NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-P... (2020)
  • NNV Demo: A Neural Network Verification Tool (2020)
  • Star-Based Reachability Analysis of Deep Neural Networks (2019)
  • Real-Time Verification for Distributed Cyber-Physical Systems (2019)
  • Reachability Analysis for High-Index Linear Differential Algebraic Equations (2019)
  • Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems (2019)
  • Parallelizable reachability analysis algorithms for feed-forward neural networks (2019)
  • Decentralized real-time safety verification for distributed cyber-physical systems (2019)
  • +19 more

Other Past Graduate Students

• RH
  Ran Hao

  Graduate researcher · Fall 2017 – Spring 2018

  LinkedIn
• YX
  Yuanqi Xie

  Graduate researcher · Fall 2017 – Fall 2018

  now: Lecturer, Department of Computer Science, University of West Florida

  WebsiteLinkedIn

MSc Thesis Alumni

• CP
  Charlie Perkins

  MS (thesis) · Spring 2025 – Fall 2025

  Cinder: Differential and Symbolic Equivalence Checking for Diffcolic Analysis of LLM-Based C-to-Rust Translation
• UY
  Ulysses Yu

  MS (thesis) · Fall 2019 – Summer 2020

  Combining Reachable Set Computation with Neuron Coverage
• AW
  Ayana Wild

  MS (thesis) · Summer 2017 – Fall 2021

  Examining the Impact of Curricular and Robotic Interventions

  LinkedInDBLP
• RK
  Rahul Kawadgave

  MS (thesis) · Fall 2015 – Summer 2016

  Automatic Conflict Classification for Vulnerable Road Users; now: Engineer, Qualcomm (Qualcomm Technologies); crowd sourcing, locate characterize, conflicts vulnerable, modes

  LinkedInGoogle Scholar

  1 paper

  • Using crowd sourcing to locate and characterize conflicts for vulnerable modes (2019)
• RL
  Randy Long

  MS (thesis) · Fall 2015 – Summer 2016

  Time-Triggered Controller Area Network Design for Formula SAE Racecars and Technique for Measuring CPU Usage on Systems with Nested and Non-Nested Interrupts

  LinkedIn
• SH
  Shweta Hardas

  MS (thesis) · Fall 2014 – Spring 2015

  Virtual and Hardware Prototyping of a Modular Multilevel Inverter for Photovoltaics

  LinkedIn
• NH
  Nathan Hervey

  MS (thesis) · Fall 2014 – Spring 2016

  Distributed Robotics Localization and Control

  LinkedIn
• AV
  Amol Vengurlekar

  MS (thesis) · Fall 2013 – May 2015

  Design of a Real-Time Reconfigurable Bioreactor; model design, analysis reconfigurable, continuous culture, bioreactor

  LinkedInDBLP

  1 paper

  • Model-based design and analysis of a reconfigurable continuous-culture bioreactor (2014)
• RZ
  Ruoshi Zhang

  MS (thesis) · Fall 2013 – Spring 2015

  Model-Based Design and Analysis of Automotive Systems using Time-Triggered Controller Area Networks (TTCAN); now: Senior Research Scientist, Louisville Automation & Robotics Research Institute (LARRI), University of Louisville; model design, analysis reconfigurable, continuous culture, bioreactor

  LinkedInGoogle Scholar

  1 paper

  • Model-based design and analysis of a reconfigurable continuous-culture bioreactor (2014)

Master of Engineering / MSc Project Alumni

• RP
  Ronald Picard

  MS (project) · Fall 2018 – Summer 2019

  Action Schema Neural Networks: Generalized Policies for Stochastic Planning Problems in the Wargaming Domain; "Action Schema Neural Networks: Generalized Policies for Stochastic Planning Problems in the Wargaming Domain"; now: Director of Aircraft Autonomy, EpiSci
• RW
  Ruohan Wang

  MS (project) · Summer 2018 – Fall 2018

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization; "Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization"
• ZB
  Zankar Bapat

  MS (project) · Spring 2014 – Spring 2015

  Robot Localization with Circle Detection; "Robot Localization with Circle Detection"
• SH
  Shamina Hossain

  MS (project) · Fall 2012 – Spring 2013

  reachability analysis, closed loop, switching power, converters

  1 paper, 1 first-author

  • Reachability Analysis of Closed Loop Switching Power Converters (2013)

Undergraduate Research Alumni

• IB
  Ibrahim Boudaoud

  Undergraduate researcher · Summer 2026

  now: Undergraduate (rising senior), Computer Science and Applied Mathematics (accelerated B.S./M.S.), Vanderbilt University
• JH
  Judy Hsu

  Undergraduate researcher · Summer 2026

  now: Undergraduate (second year), Computer Science, College of Computing, Georgia Institute of Technology

  LinkedIn
• BP
  Bishal Panthi

  Undergraduate researcher · Summer 2026

  now: Undergraduate (rising senior), Computer Science, Vanderbilt University
• YQ
  Yutong Qiu

  Undergraduate researcher · Summer 2026

  now: Undergraduate (rising sophomore), Computer Science and Mathematics, Vanderbilt University
• YW
  Yitong Wang

  Undergraduate researcher · Summer 2026

  now: Undergraduate (rising senior), Mathematics and Computer Science, Vanderbilt University
• AA
  Aarij Atiq

  Undergraduate researcher · Summer 2025
• KB
  Kiersten Brennan

  Undergraduate researcher · Summer 2025

  self correcting, neuro symbolic, reasoning framework

  1 paper

  • A Self-correcting Neuro-symbolic AI Reasoning Framework (2026)
• KL
  Kevin L. Chen

  Undergraduate researcher · Summer 2025
• JV
  Jaycie V. Nguyen

  Undergraduate researcher · Summer 2025
• VR
  Vision R. Panta

  Undergraduate researcher · Summer 2025
• GP
  Grant Petrosky

  Undergraduate researcher · Spring 2025

  Autonomous systems development
• ZS
  Zhenxuan Shao

  Undergraduate researcher · Summer 2025

  reachability formal, verification graph, neural networks, node edge, features

  DBLP

  1 paper

  • Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features (2026)
• LC
  Lana Cartailler

  Undergraduate researcher · Summer 2024

  Malware Detection Graph Neural Network Verification; now: Undergraduate student, BS Computer Science (class of 2027), Vanderbilt University
• SL
  Seojin Lee

  Undergraduate researcher · Summer 2023

  Semantic Segmentation Neural Network Verification; benchmark formal, verification semantic, segmentation neural, networks

  WebsiteLinkedInGoogle Scholar

  1 paper

  • Benchmark: formal verification of semantic segmentation neural networks (2023)
• JZ
  Jingyu (Gloria) Zhang

  Undergraduate researcher · Summer 2023

  Semantic Segmentation Neural Network Verification
• AZ
  Amanda Zhou

  Undergraduate researcher · Summer 2022

  Trustworthy Artificial Intelligence (AI)
• YL
  Yi Li

  Undergraduate researcher · Summer 2020

  Neural Network and Machine Learning Verification
• SZ
  Siqi (Christine) Zhao

  Undergraduate researcher · Summer 2020

  Neural Network and Machine Learning Verification
• LB
  Luke Bhan

  Undergraduate researcher · Summer 2019

  Autonomous F1/10 Race Car

  WebsiteGoogle ScholarDBLP
• JH
  Jiuke Huang

  Undergraduate researcher · Summer 2019

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization
• MK
  Matthew Kenigsberg

  Undergraduate researcher · Spring 2019

  Learning Hybrid Automata from Data; framework identification, validation affine, hybrid automata, input output, traces

  DBLP

  1 paper

  • A Framework for Identification and Validation of Affine Hybrid Automata from Input-Output Trace... (2022)
• AR
  Angela R Maliakal

  Undergraduate researcher · Summer 2019

  Controlling Groups of Swarm Robots
• DA
  Diandry A Rutayisire

  Undergraduate researcher · Summer 2019–Spring 2020

  Autonomous F1/10 Race Car; now: Software engineer, Active911

  WebsiteLinkedIn
• JT
  Julie Truong

  Undergraduate researcher · Summer 2019

  Controlling Groups of Swarm Robots
• AT
  Arda Turkmen

  Undergraduate researcher · Spring 2019, Fall 2018

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization
• HV
  Harsha Vankayalapati

  Undergraduate researcher · Spring 2019, Fall 2018

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization
• RW
  Rong Wang

  Undergraduate researcher · Summer 2019

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization
• JB
  Jackson Brewer

  Undergraduate researcher · Summer 2018

  Controlling Groups of Swarm Robots
• DH
  Daniel Hong

  Undergraduate researcher · Summer 2018

  Controlling Groups of Swarm Robots
• SK
  Sally Kwok

  Undergraduate researcher · Summer 2018

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization
• TL
  Teo Lee

  Undergraduate researcher · Fall 2018

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization
• TL
  Teo Lee

  Undergraduate researcher · Summer 2018

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization
• AT
  Arda Turkmen

  Undergraduate researcher · Summer 2018

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization
• JW
  Joshua Wilson

  Undergraduate researcher · Fall 2018

  Controlling Groups of Swarm Robots
• JW
  Joshua Wilson

  Undergraduate researcher · Summer 2018

  Controlling Groups of Swarm Robots
• YY
  Yufei Yan

  Undergraduate researcher · Summer 2018

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization; now: Software Engineer, Microsoft
• XZ
  Xueqing Zhao

  Undergraduate researcher · Summer 2018

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization
• XZ
  Xue Zou

  Undergraduate researcher · Summer 2018

  Auto-Scribing Electronic Health Records (EHRs) with Natural Language Processing (NLP) and Autosummarization
• AA
  Anissa Alexander

  Undergraduate researcher · Summer 2017

  Controlling Groups of Swarm Robots with Android Studio and Microsoft Kinect
• SC
  Stirling Carter

  Undergraduate researcher · Summer 2017

  Controlling Groups of Swarm Robots with Android Studio and Microsoft Kinect

  LinkedIn
• DH
  Daniel Hong

  Undergraduate researcher · Summer 2017

  Controlling Groups of Swarm Robots with Android Studio and Microsoft Kinect
• TL
  Timothy Liang

  Undergraduate researcher · Summer 2017

  Controlling Groups of Swarm Robots with Android Studio and Microsoft Kinect
• CW
  Christina Wang

  Undergraduate researcher · Summer 2017

  Controlling Groups of Swarm Robots with Android Studio and Microsoft Kinect
• AW
  Austin Wilms

  Undergraduate researcher · Summer 2017

  Controlling Groups of Swarm Robots with Android Studio and Microsoft Kinect
• YY
  Yinghui Yang

  Undergraduate researcher · Summer 2017

  Controlling Groups of Swarm Robots with Android Studio and Microsoft Kinect
• ET
  Ewin Tang

  Undergraduate researcher · Summer 2015

  now: Miller Postdoctoral Fellow, University of California, Berkeley; Assistant Professor of Computer Science, Princeton University (appointment begins September 2026)

  WebsiteGoogle ScholarDBLP
• EN
  Eric Nelson

  Undergraduate researcher · Fall 2013–Spring 2014

  model design, analysis reconfigurable, continuous culture, bioreactor

  DBLP

  1 paper

  • Model-based design and analysis of a reconfigurable continuous-culture bioreactor (2014)
• ZZ
  Zhongdong Zhu

  Undergraduate researcher · Fall 2011

NSF REU Alumni

• LB
  Lucas Buccafusca

  NSF REU · Summer 2012

  Safe Distributed Flocking Implemented on the StarL Distributed Robotics Framework; now: Lecturer (teaching faculty), Department of Electrical and Computer Engineering, Johns Hopkins University

  WebsiteGoogle ScholarDBLP
• SG
  Shashank Gupta

  NSF REU · Summer 2009

  Distributed Algorithms for Sensor Networks Implemented on Net-X

PURE Alumni (University of Illinois)

• JK
  Jordan Kravitz

  PURE · Spring 2012
• ZH
  Zhihao (Ted) Hong

  PURE · Spring 2011

  design verification, methods switching, power converters

  1 paper

  • Design Verification Methods for Switching Power Converters (2012)
• AK
  Akash Kapoor

  PURE · Fall 2011

  design verification, methods switching, power converters

  1 paper

  • Design Verification Methods for Switching Power Converters (2012)
• JL
  Jeffrey Lale

  PURE · Spring 2011
• HT
  Hershed Tilak

  PURE · Spring 2011
• HT
  Hershed Tilak

  PURE · Fall 2010
• RB
  Rohan Bali

  PURE · Spring 2009
• PG
  Patrick Gu

  PURE · Spring 2009
• DS
  Dongeek Shin

  PURE · Fall 2009

  now: Principal Engineer, Google DeepMind (Google)

  WebsiteLinkedInDBLP
• JS
  Jerry Sun

  PURE · Fall 2009
• HL
  Haeran Lee

  PURE · Fall 2008

Prospective Students: I am looking for ambitious and motivated graduate and undergraduate students. Research Assistantships (RAs) are available for competitive candidates. If you are a Vanderbilt student looking for an advisor, or if you are interested in applying to Vanderbilt for graduate studies in Electrical Engineering, Computer Science, or Computer Engineering, please email me with your resume/CV if you are interested to do research in formal methods, hybrid systems, embedded systems / cyber-physical systems, software engineering, distributed systems, and related areas. If you do not include your resume/CV, I will definitely not respond. As I receive many such requests, I cannot reply to every email, but do my best to reply to competitive applicants.

Current/Recent Collaborators

• Stanley Bak
• Leonardo Bobadilla
• Sergiy Bogomolov
• Marco Caccamo
• Jyotirmoy V. Deshmukh
• Sebastian Fischmeister
• Amy LaViers
• Sayan Mitra
• Christian Schilling
• Lui Sha
• Andreas Veneris

© 2026 Taylor Johnson, All Rights Reserved.