Welcome to Luan V. Nguyen's Homepage
 |
Luan V. Nguyen, Ph.D. |
Brief Bio: I am currently an Assistant Professor at the Department of Computer Science, University of Dayton. Previously, I was a postdoctoral research associate at the Department of Electrical Engineering, University of Notre Dame (Oct 2019 - July 2020), and at the PRECISE Center, University of Pennsylvania (June 2018 - Sep 2019). I received my B.E. in May 2012 and M.Sc. degree in December 2012 at The Catholic University of America. During my Ph.D., I was a member of the Verivital Lab at The University of Texas at Arlington, under the supervision of Prof. Taylor T. Johnson. My research interest is to develop formal verification techniques and state-of-the-art software tools to enforce safety, reliability, security and resiliency of autonomous cyber-physical systems (CPS), with practical applications across CPS domains such as power and energy systems, medical devices, automotive, aerospace, and robotics.
Prospective students
I am looking for self-motivated graduate and undergraduate students in the areas of cyber-physical systems, model-based design, formal verification, and safe autonomy. Funding support is available for competitive applicants with excellent qualifications. If you are interested, please send me an email with your CV or drop by my office if you are on campus.
What's new
Sep 2024: Papers accepted at ICFEM 2024, NordSec 2024, KSE 2024
Aug 2024: Paper accepted at ECAI 2024
Mar 2024: Received UD Chapter Sigma Xi Early Career Award Recognition for Research
Feb 2024: Received ODHE Third Frontier Innovation Initiatives Grant
Jan 2024: Received Research Council Seed Grant
Sep 2023: Paper accepted at ACM Transactions on Embedded Computing Systems
Aug 2023: Paper accepted at IEEE MEMOCODE 2023
May 2023: Paper accepted at IEEE Robotics and Automation Letters
Mar 2023: Received NSF CRII Grant
Feb 2023: Paper accepted at FORMALISE 2023 with Artifact Evaluation Badge, received UD Research Council Seed Grant and UD/UDRI Research Fellowship
Jan 2023: Paper accepted at IEEE Transactions on Control of Network Systems
Research Interest
Cyber-Physical Systems: Formal Verification, Logic-guided Testing, and Specification Mining
Model-based Repair for Improving Resiliency of Hybrid Systems
Safe Autonomy
Secure Information Flow Analysis
Software Engineering
Education
Ph.D., Computer Engineering, The University of Texas at Arlington, May 2018
M.Sc., Computer Science, The Catholic University of America, December 2012
B.E., Electrical Engineering, The Catholic University of America, May 2012
Tools
REAFFIRM: Model-Based Repair of Hybrid Systems for Improving Resiliency (main developer)
HyRG: A Random Generation Tool for Affine Hybrid Automata (main developer)
NNV: A Matlab Toolbox For Neural Network Verification (contributor)
Hynger: A Prototype toward Identifying Cyber-Physical Specification Mismatches (contributor)
HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models (contributor)
Teaching
Instructor at University of Dayton for:
Computer-Aided Verification (CPS 592), Spring 2024 and Fall 2024
Safety and Security in Autonomous Systems (CPS 573), Spring 2022, 2023, 2024 and Fall 2022, 2023, 2024
Cyber-Physical Systems and the Internet of Things (CPS 592), Fall 2020, and Spring 2021
Computer Organization and Architecture (CPS 250), Spring 2021, 2022, 2023, and Fall 2021, 2022, 2023, 2024
Teaching assistant at The University of Texas at Arlington for:
Operating Systems (CSE3320), Fall 2017 and Spring 2018
Object-oriented Programming (CSE1325), Spring 2014, 2015, Summer 2014, and Fall 2014
Publications
Journal Articles:
J12. Sung Woo Cho, Mykhailo Ivashchenko, Luan Viet Nguyen, and Hoang-Dung Tran, “Reachability Analysis of Sigmoidal Neural Networks,” ACM Transactions on Embedded Computing Systems, 2023 (link)
J11. Ernest Bonnah, Luan Viet Nguyen, and Khaza Anuarul Hoque, “Model Checking Time Window Temporal Logic for Hyperproperties,” IEEE Robotics and Automation Letters, 2023 (link)
J10. Luan Viet Nguyen, Hoang-Dung Tran, Taylor T. Johnson, and Vijay Gupta, “Decentralized Safe Control for Distributed Cyber-Physical Systems using Real-time Reachability Analysis,” IEEE Transactions on Control of Network Systems, 2023 (link)
J9. Hoang Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson, “Real-Time Verification for Distributed Cyber-Physical Systems,” Leibniz Transactions on Embedded Systems, Vol. 8 No. 2, Special Issue on Distributed Hybrid Systems, 2022 (invited paper) (link)
J8. Luan Viet Nguyen and Vijay Gupta, “Toward A Framework of Enforcing Resilient Operation of Cyber-Physical Systems with Unknown Dynamics,” IET Cyber-Physical Systems: Theory & Applications, 2021. (link)
J7. Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak and Taylor T. Johnson, “Verification of Piecewise Deep Neural Networks: A Star Set Approach with Zonotope Pre-Filter,” Formal Aspects of Computing, 2021 (link)
J6. Omar Beg, Luan Viet Nguyen, Taylor T. Johnson and Ali Davoudi, “Anomaly Detection in DC and AC Microgrids Using Parametric Time-frequency Logic,” IEEE Access, 2021 (link)
J5. Stanley Bak, Omar Beg, Sergiy Bogomolov, Taylor T. Johnson, Luan Viet Nguyen, and Christian Schilling, “Hybrid Automata: from Verification to Implementation,” International Journal on Software Tools for Technology Transfer, Springer, vol. 21, pp. 87-104, February 2019 (link)
J4. Luan Viet Nguyen, Khaza Anuarul Hoque, Stanley Bak, Steven Drager, and Taylor T. Johnson, “Cyber-Physical Specification Mismatches,” ACM Transactions on Cyber-Physical Systems (TCPS), September 2018 (link)
J3. Omar Beg, Luan Viet Nguyen, Taylor T. Johnson and Ali Davoudi, “Signal Temporal Logic-based Attack Detection in DC Microgrids,” IEEE Transactions on Smart Grid, 2017 (link)
J2. Hoang Dung Tran, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson, “Order-reduction abstractions for safety verification of high-dimensional linear systems,” Springer Discrete Event Dynamic Systems, Special Issue on Formal Methods in Control, February 2017 (link)
J1. Luan Viet Nguyen, Hoang-Dung Tran, and Taylor T. Johnson, “Virtual Prototyping for Distributed Control of a Fault-Tolerant Modular Multilevel Inverter for Photovoltaics,” in IEEE Transactions on Energy Conversion, vol. 29, pp. 841-850, December 2014 (link)
Conference Proceeding Papers:
C17. Ernest Bonnah, Luan Viet Nguyen, and Khaza Anuarul Hoque, “Motion Planning using Hyperproperties for Time Window Temporal Logic,” 21st ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2023), Hamburg, Germany, September 2023 (link)
C16. Mykhailo Ivashchenko, Sung Woo Choi, Luan Viet Nguyen, and Hoang-Dung Tran, “Verifying Binary Neural Networks on Continuous Input Space using Star Reachability,” in 11th International Conference on Formal Methods in Software Engineering (FORMALISE 2023), Melbourne, Victoria, Australia, May 2023 (link)
C15. Luan Viet Nguyen, Gautam Mohan, James Weimer, Oleg Sokolsky, Insup Lee, and Rajeev Alur, “REAFFIRM: Model-Based Repair of Hybrid Systems for Improving Resiliency,” in 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2020), Jaipur, India, December 2020 (link)
C14. Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T. Johnson, “NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems”, in 32nd International Conference on Computer-Aided Verification (CAV), 2020, July (link)
C13. Luan Viet Nguyen, Gautam Mohan, James Weimer, Oleg Sokolsky, Insup Lee, and Rajeev Alur, “Detecting Security Leaks in Hybrid Systems with Information Flow Analysis,” in 17th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2019), San Diego, October 2019 (Best Paper Award) (link)
C12. Hoang Dung Tran, Patrick Musau, Manxanas Lopez Diego, Xiao Dong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson, “Star-Based Reachability Analysis of Deep Neural Networks,” in 23rd International Symposium on Formal Methods (FM 2019), Portugal, October 2019. (link)
C11. Hoang Dung Tran, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson, “Reachability Analysis for High-Index Large Linear Differential Algebraic Equations,” in 17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMAT 2019), Amsterdam, Netherlands, August 2019 (link)
C10. Hoang Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson, “Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems,” in 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2019), Denmark, June 2019 (link)
C9. Hoang Dung Tran, Patrick Musau, Manxanas Lopez Diego, Xiao Dong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson, “Parallelizable Reachability Analysis Algorithms for Feed-Forward Neural Networks,” in 7th International Conference on Formal Methods in Software Engineering (FORMALISE 2019), Montreal, May 2019 (link)
C8. Luan Viet Nguyen, Gautam Mohan, James Weimer, Oleg Sokolsky, Insup Lee, and Rajeev Alur, “REAFFIRM: Model-Based Repair of Hybrid Systems for Improving Resiliency,” February, 2019 (arxiv)
C7. Luan Viet Nguyen, Bardh Hoxha, Georgios Fainekos and Taylor T. Johnson, “Mission Planning for Multiple Unmanned Vehicles using UxAS,” in IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2018), Oxford, July 2018 (link)
C6. Omar Beg, Luan Viet Nguyen, Taylor T. Johnson and Ali Davoudi, “Computer-Aided Formal Verification of Power Electronics Circuits,” Frontiers in Analog CAD, Proceedings of, pp. 1-6. VDE, 2017 (link)
C5. Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy Deshmukh, and Taylor T. Johnson, “Hyperproperties of Real-Valued Signals,” 15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017), Vienna, October 2017 (link)
C4. Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy Deshmukh, Ken Butts, and Taylor T. Johnson, “Abnormal Data Classification Using Time-Frequency Temporal Logic,” 20th ACM International Conference on Hybrid Systems: Computation and Control 2017 (HSCC 2017), Pittsburgh, PA, April 2017 (link)
C3. Parasara Sridhar Duggirala, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, Sergiy Bogomolov, Taylor T. Johnson, Luan Viet Nguyen, Christian Schilling, Andrew Sogokon, Hoang-Dung Tran, and Weiming Xiang, “Tutorial: Software Tools for Hybrid Systems Verification, Transformation, and Synthesis: C2E2, HyST, and TuLiP”, In Proceedings of the IEEE Multi-Conference on Systems and Controls (MSC 2016), Las Vegas, NV, USA, 2016, September (link)
C2. Luan Viet Nguyen, Christian Schilling, Sergiy Bogomolov, and Taylor T. Johnson, “Runtime Verification for Hybrid Analysis Tools,” in 15th International Conference on Runtime Verification (RV 2015), Vienna, Austria, September 2015 (link)
C1. Luan Viet Nguyen, Christian Schilling, Sergiy Bogomolov, and Taylor T. Johnson, “HyRG: A Random Generation Tool for Affine Hybrid Automata,” in 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015), CPSWeek 2015, Seattle, WA, April 2015 (link)
Workshop Proceeding Papers:
W7. Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T. Johnson, “Demo: The Neural Network Verification (NNV) Tool,” in IEEE Workshop on Design Automation for CPS and IoT (DESTION), 2021, April (link)
W6. Hoang-Dung Tran, Luan Viet Nguyen, Weiming Xiang and Taylor T. Johnson, “Distributed Autonomous Systems (Benchmark Proposal),” in 4th International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH 2017), Pittsburgh, PA, April 2017 (link)
W5. Hoang-Dung Tran, Luan Viet Nguyen, and Taylor T. Johnson, “Large-Scale Linear Systems from Order-Reduction (Benchmark Proposal),” in 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH 2016), Vienna, Austria, April 2016 (link)
W4. Luan Viet Nguyen, Djordje Maksimovic, Taylor T. Johnson, and Andreas Veneris, “Quantified Bounded Model Checking for Rectangular Hybrid Automata,” in 9th International Workshop on Constraints in Formal Verification (CFV 2015), Austin, TX, November 2015 (link)
W3. Hoang-Dung Tran, Luan Viet Nguyen, and Taylor T. Johnson, “Benchmark: A Nonlinear Reachability Analysis Test Set from Numerical Analysis,” in 2nd International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH 2015), CPSWeek 2015, Seattle, WA, April 2015 (link)
W2. Luan Viet Nguyen and Taylor T. Johnson, “Benchmark: DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters),” in 1st International Workshop on Applied Verification for Continuous and Hybrid Systems Workshop (ARCH 2014), Berlin, Germany, April 2014 (link)
W1. Luan Viet Nguyen, Eric Nelson, Amol Vengurlekar, Ruoshi Zhang, Kristopher I White, Victor Salinas, and Taylor T. Johnson, “Model-Based Design and Analysis of a Reconfigurable Continuous-Culture Bioreactor (Work-in-Progress),” in 4th ACM Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems (Cyphy 2014), Berlin, Germany, April 2014 (link)
Posters:
P3. Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy Deshmukh, and Taylor T. Johnson, “Hyperproperties of Real-Valued Signals” Hybrid Systems Computation and Control 2017 (HSCC 2017), Pittsburgh, PA, April 2017
P2. Luan Viet Nguyen, and Taylor T. Johnson, “Towards Bounded Model Checking for Timed and Hybrid Automata with a Quantified Encoding,” in PhD Student Forum, 15th International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX, September 2015
P1. Luan Viet Nguyen, and Taylor T. Johnson, “Model-Based Design and Analysis of a Continuous Culture Bioreactor for Systems Biology Experiments,” Texas Systems Day, Texas A&M University, College Station, TX, March 2014
Patents:
Jyotirmoy Deshmuk, James Kapinski, Xiaoqing Jin, and Luan Viet Nguyen, “Privacy-Aware Signal Monitoring Systems and Methods,” Patent No. US 11087568B2, August 2021 (link)
Award and Honors
UD Chapter Sigma Xi Early Career Award Recognition for Research, March 2024.
Best Paper Award for the paper “Detecting Security Leaks in Hybrid Systems with Information Flow Analysis,” in 17th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2019),San Diego, October 2019.
Toyota Travel Award for paper presentation at 20th ACM International Conference on Hybrid Systems: Computation and Control 2017 (HSCC 2017), Pittsburgh, PA, April 2017.
NSF Travel Award for PhD Student Forum, in 15th International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX.
NSF and ACM SIGBED Travel Awards for Cyber-Physical Systems Week (CPSWeek 2015), Seattle, WA.
NSF Travel Award for CPS Verification and Validation: Industrial Challenges and Foundations (CPS V&V I&F), Carnegie Mellon University, Pittsburgh, PA.
3rd Place Winner and $1000 Award in US/India Chamber DFW (USICOC) Spirit of Innovation Competition, Dallas, TX.