Research

VeriVITAL People: Collaborators and Students

Research Interests

• Cyber-physical systems: real-time, networked embedded control systems and software
• Software engineering, formal methods, and formal verification
• Safe autonomy: from sensing and perception through planning and control, encompassing computer vision reliability and neural network control systems (NNCS)
• Safe and trustworthy artificial intelligence (AI): robust machine learning (ML), adversarial machine learning, symbolic (e.g., automata) learning, requirements and specifications in AI/ML (robustness, safety, security, etc.)
• Hybrid systems and switched systems: hybrid automata, dynamics models (ODEs, DAEs, PDEs, etc.), reachability
• Reliability and fault-tolerance
• Application domains including transportation systems (aerospace and automotive), robotics, power and energy systems

Curriculum Vitae (CV) / Resume [pdf]

Research Support

We gratefully acknowledge the support of our ongoing/past research by AFOSR, AFRL, ARO, DARPA, MathWorks, NSA, NSF (CISE CCF/SHF, CNS/CPS, FMitF; ENG ECCS/EPCN), NVIDIA, ONR, Toyota Technical Center, and USDOT. More details on the projects are available in my CV.

Active & Ongoing Research Projects

• “PRISMATIC: Pathways and Resources for Interdisciplinary Student Majors — AI, Technology, and Inclusive Computing”, Northeastern University (NEU), Center for Inclusive Computing, Role: PI with Julie L. Johnson (Co-PI), 2026–2028.
• “VSEC Seed Project (AI safety/verification with legal and control collaborators)”, Vanderbilt University (VU), VSEC Seed Project Fund, Role: PI with Meiyi Ma, Ahmad Taha, Mark Williams, 2026–2028.
• “Workshops on Safe, Secure, and Trustworthy Generative Artificial Intelligence”, Vanderbilt University (VU), Vanderbilt-Liverpool Joint Research Seed Grant, Role: PI with Xiaowei Huang (University of Liverpool), 2025–.
• “Dependable AI for National Security (DAINS)”, Department of Energy (DOE), Role: Co-PI with Gabor Karsai (PI), Jonathan Sprinkle (Co-PI), 2025–2028.
• “Assured Neuro Symbolic Components and Systems (ANSCS)”, Defense Advanced Research Projects Agency (DARPA), Assured Neuro Symbolic Learning and Reasoning, Role: Co-PI with Gabor Karsai (PI), Xenofon Koutsoukos (Co-PI), Abhishek Dubey (Co-PI), Janos Sztipanovits, 2023–2027.
• “Improving Malware Classifiers with Plausible Novel Samples”, National Security Agency (NSA), Science of Security, Role: Co-PI with Kevin Leach (PI), 2023–2026.
• “FMitF: Track I: Generative Neural Network Verification in Medical Imaging Analysis”, National Science Foundation (NSF), Formal Methods in the Field (FMitF), Directorate for Computer and Information Science and Engineering, Role: PI with Ipek Oguz (Co-PI), Meiyi Ma (Co-PI), 2022–2026. Award Number: 2220401.

Past & Completed Research Projects

• “Verification of Autonomous Systems through Hyperproperties and Machine Learning”, Air Force Office of Scientific Research (AFOSR), Role: PI, 2023–2024. Award Number: FA9550-23-1-0135.
• “High-Performance Computing for Neural Network Verification”, National Security Agency (NSA), Georgia Tech Research Institute, Role: PI, 2023–2024.
• “Collaborative Research: FMitF: Track II: Enhancing the Neural Network Verification (NNV) Tool for Industrial Applications”, National Science Foundation (NSF), Formal Methods in the Field (FMitF), Directorate for Computer and Information Science and Engineering, Role: PI with Hoang-Dung Tran (PI, UNL), 2022–2025. Award Number: 2220426.
• “NSF Workshop on Safety and Trust in Artificial Intelligence Enabled Systems”, National Science Foundation (NSF), Software and Hardware Foundations, Division of Computing and Communication Foundations, Directorate for Computer and Information Science and Engineering, Role: PI with Jerry Zhu, Kate Saenko, 2022–2023. Award Number: 2231543.
• “Verification of Autonomous Systems: Hyperproperties in Machine Learning”, Air Force Office of Scientific Research (AFOSR), Trusted AI Challenge, Role: Sole PI, 2021–2023.
• “Hyperproperties for Generative AI Models”, Semiconductor Research Corporation (SRC), Artificial Intelligence Hardware, Role: Sole PI, 2021–2023.
• “Collaborative Research: Operator Theoretic Methods for Identification and Verification of Dynamical Systems”, National Science Foundation (NSF), Energy, Power, Control, and Networks Program, Division of Electrical, Communications and Cyber Systems, Directorate for Engineering, Role: PI with Joel Rosenfeld (PI), Rushikesh Kamalapurkar (PI), 2020–2024.
• “SHF: Small: Collaborative Research: Fuzzing Cyber-Physical System Development Tool Chains with Deep Learning (DeepFuzz-CPS)”, National Science Foundation (NSF), Software and Hardware Foundations, Division of Computing and Communication Foundations, Directorate for Computer and Information Science and Engineering, Role: PI with Christoph Csallner (PI), 2019–2022.
• “FMitF: Track II: Hybrid and Dynamical Systems Verification on the CPS-VO”, National Science Foundation (NSF), Formal Methods in the Field (FMitF), Directorate for Computer and Information Science and Engineering, Role: PI with Joel Rosenfeld (Co-PI), 2019–2021.
• “Equivalence Modulo Input (EMI)-Based Validation of CPS Tool Chains”, The MathWorks, Development Collaboration Research Grant, Role: Co-PI with Christoph Csallner (PI), 2018–2019.
• “Scalable Formal Verification of Resilient Converter-dominated MVDC Networks”, Office of Naval Research (ONR), Sea and Warfare Weapons, Role: Co-PI with Ali Davoudi (PI, UT-Arlington), 2018–2021. Award Number: N00014-18-1-2184.
• “Understandable and Reusable Formal Verification for Cyber-Physical Systems”, Air Force Office of Scientific Research (AFOSR), Young Investigator Research Program, Role: Sole PI, 2018–2021. Award Number: FA9550-18-1-0122.
• “Assurance-Based Learning-Enabled Cyber-Physical Systems (ALC)”, Defense Advanced Research Projects Agency (DARPA), Assured Autonomy, Role: Co-PI with Gabor Karsai, Xenofon Koutsoukos (Co-PI), Ted Bapty (Co-PI), Janos Sztipanovits (Oversight), 2018–2023.
• “Cyber-Physical Systems Specification Mismatch and Safe Upgrades”, Air Force Office of Scientific Research (AFOSR), Systems and Software Program, Role: Sole PI, 2016–2018.
• “Safely and Securely Controlling Large Swarms of Unmanned Aerial Vehicles (UAVs) with the STAbilizing Robot Language (StarL)”, Air Force Research Laboratory (AFRL), Summer of Innovation, Role: Sole PI, 2017. Award Number: FA8650-12-3-7255.
• “Formal Modeling of Emergence in Distributed Cyber-Physical Systems”, Air Force Research Laboratory (AFRL), Trusted Autonomy and Verification and Validation (VV), Integrated Command and Control, Role: Sole PI, 2016–2017.
• “Faculty Travel Program”, Southeastern Conference (SEC), Role: Sole PI, 2017–2018.
• “Improving Participation of Female Computer Science Majors and Professionals through Digital Learning with Groups of Mobile Robots Controlled by Android Apps”, Vanderbilt Institute for Digital Learning (VIDL), MacroGrant, Role: PI with Gautam Biswas (Co-PI), Clare McCabe (Co-PI), Julie Johnson (Co-PI), 2017–2018.
• “Science of Security for Cyber-Physical Systems Lablet”, Department of Defense (DoD), Science of Security Lablet, Role: Co-PI with Xenofon Koutsoukos (PI), Janos Sztipanovits (Vanderbilt/EECS), Gabor Karsai (Vanderbilt/EECS), Aniruddha Gokhale (Vanderbilt/EECS), Yevgeniy Vorobeychik (Vanderbilt/EECS), Abhishek Dubey (Vanderbilt/EECS), Maithilee Kunda (Vanderbilt/EECS), Peter Volgyesi (Vanderbilt/EECS), Jennifer Trueblood (Vanderbilt/Psychology), S. Shankar Sastry (Berkeley/EECS), Claire Tomlin (Berkeley/EECS), Anthony Joseph (Berkeley/EECS), Saurabh Amin (MIT/CEE), Nazli Choucri (MIT/Political Science), Alvaro Cardenas (UT Dallas/CS), Bhavani Thuraisingham (UT Dallas/CS), 2017–2022.
• “Realizing Resilient Self-Organizing Microgrids”, Army Research Office (ARO), Department of Defense (DoD) Research and Education Program for Historically Black Colleges and Universities and Minority-Serving Institutions (HBCU/MI), Role: Co-PI with Ali Davoudi (PI, UT-Arlington), Frank Lewis (Co-PI, UT-Arlington), Hamidreza Modares (Co-PI, UT-Arlington), 2016–2017. Award Number: W911NF-16-1-0534.
• “Testbed Acquisition for Resilient Self-Organizing Microgrids”, Office of Naval Research (ONR), Defense University Research Instrumentation Program, Role: Co-PI with Ali Davoudi (PI, UT-Arlington), Frank Lewis (Co-PI, UT-Arlington), Hamidreza Modares (Co-PI, UT-Arlington), 2016–2017. Award Number: N0014-16-1-3180.
• “Reusable Formal Verification for Cyber-Physical Systems”, Air Force Office of Scientific Research (AFOSR), Young Investigator Research Program, Role: Sole PI, 2016–2019. Award Number: FA9550-16-1-0246.
• “Real-time Ab Initio Modeling of Electric Machines”, National Science Foundation (NSF), Energy, Power, Control, and Networks Program, Division of Electrical, Communications and Cyber Systems, Directorate for Engineering, Role: Co-PI with Ali Davoudi (PI), David Levine (Senior Personnel), 2015–2021. Award Number: 1509804.
• “Cyber-Physical Systems Specification Mismatch and Safe Upgrades”, Air Force Office of Scientific Research (AFOSR), Systems and Software Program, Role: Sole PI, 2015–2018. Award Number: FA9550-15-1-0258.
• “Detecting and Mitigating Cyber-Physical Attacks with Invariant Inference and Runtime Assurance”, Air Force Office of Scientific Research (AFOSR), Summer Faculty Fellowship Program, Role: Sole PI, 2015.
• “Formal Modeling of Emergence in Distributed Cyber-Physical Systems”, Air Force Research Laboratory (AFRL), Trusted Autonomy and Verification and Validation (VV), Integrated Command and Control, Role: Sole PI, 2015–2017. Award Number: FA8750-15-1-0105.
• “CRII: CPS: Safe Cyber-Physical Systems Upgrades”, National Science Foundation (NSF), CISE Research Initiation Initiative, Cyber-Physical Systems Program, Division of Computer and Network Systems, Directorate for Computer and Information Science and Engineering, Role: Sole PI, 2015–2017. Award Number: 1713253, 1464311.
• “SHF: Small: Automating Improvement of Development Environments for Cyber-Physical Systems (AIDE-CPS)”, National Science Foundation (NSF), Software and Hardware Foundations, Division of Computing and Communication Foundations, Directorate for Computer and Information Science and Engineering, Role: PI with Christoph Csallner (Co-PI), 2015–2019. Award Number: 1736323, 1527398.
• “Real-time Ab Initio Modeling of Electric Machines”, NVIDIA, Hardware Donation Program, Role: PI with Ali Davoudi (Co-PI), David Levine (Senior Personnel), 2014.
• “App-Based Crowd Sourcing of Bicycle and Pedestrian Conflict Data”, United States Department of Transportation (USDOT), University Transportation Center for Livable Communities, Role: Co-PI with Stephen Mattingly (PI), Colleen Casey (Co-PI), 2015–2016. Award Number: DTRT13-G-UTC60.
• “Inferring Physical System Specifications from Embedded Software Tests”, Air Force Research Laboratory (AFRL), Visiting Faculty Research Program, Role: Sole PI, 2014. Award Number: FA8750-13-2-0115.

Research Software and Artifacts

Talks and tool demonstrations are on our YouTube channel.

We develop verification software tool prototypes, some peer-reviewed through software repeatability evaluations. Source is maintained at github.com/verivital and github.com/ttj.

• STLGym (2022–present)
  A safe reinforcement learning tool for learning control policies that satisfy timed and untimed specifications written in signal temporal logic (STL)..
  1 related paper

  • Training Agents to Satisfy Timed and Untimed Signal Temporal Logic Specifications with Reinforcement Learning (2022)
• Veritex (2021–present)
  A tool for verification and repair of neural networks, written in Python. It implements different data structures and approaches compared to NNV, and supports repairing a network that fails its specification rather than only reporting the failure..
  2 related papers

  • Metacognition with Neural Network Verification and Repair using Veritex (2025)
  • Reachability Analysis of Deep ReLU Neural Networks using Facet-Vertex Incidence (2021)
• Behavior Tree Verification Tool (BehaVerify) (2020–present)
  This software tool implements methods to formally verify behavior trees.
  3 related papers

  • Formalizing Stateful Behavior Trees (2024)
  • Verification of Behavior Trees with Contingency Monitors (2024)
  • BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees (2022)
• AbLECPS and the ALC Toolchain (2018–present)
  Assurance-based Learning-enabled Cyber-Physical Systems (AbLECPS) and the Assurance-based Learning-enabled CPS (ALC) toolchain. Integrates our DARPA Assured Autonomy verification tools, such as NNV and BehaVerify, with design tools for learning-enabled CPS. Built on WebGME..
  2 related papers

  • Assuring Learning-Enabled Components in Small Unmanned Aircraft Systems (2021)
  • CPS Design with Learning-Enabled Components: A Case Study (2019)
• Hybrid Automata Learning Toolkit (HAutLearn) (2018–present)
  This software tool implements methods to infer hybrid automaton models from time-series data.
  1 related paper

  • A Framework for Identification and Validation of Affine Hybrid Automata from Input-Output Traces (2022)
• NNV and nnmt (2018–present)
  Neural network verification and neural network model transformation tools. These software tools implement methods for formally verifying properties of systems incorporating neural networks, as well as for interchange with other neural network verification tools and related software, such as ONNX, PyTorch, Keras, Tensorflow, etc.
  15 related papers

  • Robustness Verification of Video Classification Neural Networks (2025)
  • FairNNV: The Neural Network Verification Tool For Certifying Fairness (2024)
  • NNV 2.0: The Neural Network Verification Tool (2023)
  • Reachability Analysis of a General Class of Neural Ordinary Differential Equations (2022)
  • Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability (2021)
  • Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach (2021)
  • NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems (2020)
  • Verification of Deep Convolutional Neural Networks Using ImageStars (2020)
  • Case Study: Safety Verification of an Unmanned Underwater Vehicle (2020)
  • Star-Based Reachability Analysis of Deep Neural Networks (2019)
  • Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control (2019)
  • Parallelizable reachability analysis algorithms for feed-forward neural networks (2019)
  • Verification of closed-loop systems with neural network controllers (2019)
  • ARCH-COMP19 Category Report: Artificial Intelligence/Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants (2019)
  • Output reachable set estimation and verification for multilayer neural networks (2018)
• daev (2017–present)
  Differential algebraic equation (DAE) verification tool. This software tool implements methods to formally verify safety properties of systems incorporating DAEs, specifically targeted for DAEs with index greater than one, for which it is impossible to represent as classical hybrid automata without model transformations.
  1 related paper

  • Reachability Analysis for High-Index Linear Differential Algebraic Equations (2019)
• pdev (2017–present)
  Partial differential equation (PDE) verification tool. This software tool implements numerical reachability analysis methods for systems incorporating PDEs.
  1 related paper

  • Reachability Analysis for One Dimensional Linear Parabolic Equations (2018)
• SLForge and CyFuzz (2015–present)
  Random differential testing for CPS Development Toolchains. This software tool randomly generates CPS model artifacts, currently targeting the MathWorks' Simulink/Stateflow (SLSF).
  3 related papers

  • SLEMI: Equivalence Modulo Input (EMI) Based Mutation of CPS Models for Finding Compiler Bugs in Simulink (2020)
  • Automatically Finding Bugs in a Commercial Cyber-Physical System Development Tool Chain With SLforge (2018)
  • CyFuzz: A Differential Testing Framework for Cyber-Physical Systems Development Environments (2016)
• ha2slsf (2015–present)
  A converter of hybrid automata to Simulink/Stateflow models. Takes hybrid automaton models and generates semantically equivalent Simulink/Stateflow models; being merged into HyST..
  2 related papers

  • Hybrid automata: from verification to implementation (2019)
  • HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models (2015)
• HyST (2014–present)
  Hybrid Source Transformer. This software tool takes hybrid automaton models in the SpaceEx XML or Compositional Interchange Format (CIF) formats and translates them to other popular hybrid systems verification and reachability analysis tools, including Flow*, dReach, HyComp, HyCreate, and development tools including MathWorks' Simulink/Stateflow (SLSF). Best repeatability evaluation award.
  6 related papers

  • NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems (2020)
  • Hybrid automata: from verification to implementation (2019)
  • Scalable Static Hybridization Methods for Analysis of Nonlinear Systems (2016)
  • Periodically-Scheduled Controller Analysis using Hybrid Systems Reachability and Continuization (2015)
  • Runtime Verification for Hybrid Analysis Tools (2015)
  • HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models (2015)
• Hynger (2014–present)
  Hybrid iNvariant GEneratoR: This software tool takes MathWorks' Simulink/Stateflow (SLSF) models, instruments them, and produces traces for dynamic analysis in tools like Daikon.
  4 related papers

  • Signal Temporal Logic-based Attack Detection in DC Microgrids (2019)
  • Cyber-Physical Specification Mismatches (2018)
  • Detection of false-data injection attacks in cyber-physical DC microgrids (2017)
  • Cyber-Physical Specification Mismatch Identification with Dynamic Analysis (2015)
• rtreach (2014–present)
  Real-time reachability algorithms for hybrid systems with linear and nonlinear dynamics: This software implements reachability analysis algorithms based on face-lifting that have worst-case execution time (WCET) guarantees.
  3 related papers

  • Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems (2019)
  • Real-time reachability for verified simplex design (2016)
  • Real-Time Reachability for Verified Simplex Design (2014)
• HyRG (2014–2016)
  Hybrid Random Generator. This software tool randomly generates hybrid automaton models, and is integrated within HyST to generate models in output formats compatible with several different formal verification tools for hybrid systems.
  1 related paper

  • Runtime Verification for Hybrid Analysis Tools (2015)
• Passel (2011–2014)
  This software tool is used for parameterized verification (sometimes known as uniform verification) of parameterized networks of hybrid automata, and has been used to verify safety specifications in several distributed cyber-physical systems such as proving safe separation in air traffic control protocols.
  4 related papers

  • Anonymized Reachability of Hybrid Automata Networks (2014)
  • Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Applications to Aerospace Systems (2013)
  • A small model theorem for rectangular hybrid automata networks (2012)
  • Parameterized verification of distributed cyber-physical systems: An aircraft landing protocol case study (2012)

Research Links

• VeriVITAL Research Group Webpage
• VeriVITAL Research Group Google Photos
• VeriVITAL Research Group Youtube Page
• ACM Author Page
• Web of Science Reviewer Profile (formerly Publons)
• DBLP
• Google Scholar Profile
• Vanderbilt University Faculty Profile
• ORCID
• ResearcherID
• ResearchGate
• Former Research Group Wiki (at Illinois)
• Microsoft Academic Search Profile

Publications

The entire BiBteX file is available here.

Copyright Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.