Welcome to Luan V. Nguyen's Homepage

Luan Nguyen 

Luan V. Nguyen, Ph.D.
Department of Computer and Information Science
University of Pennsylvania
Email: luanvn at seas dot upenn dot edu

Luan V. Nguyen is currently a postdoctoral research associate at the PRECISE Center, University of Pennsylvania, working under the supervision of Prof. Rajeev Alur . He graduated with honors from M.Sc. program in December 2012 at The Catholic University of America, where he had previously earned his B.E. in May 2012. During his Ph.D., he was a member of the Verivital Lab at The University of Texas at Arlington, under the supervision of Prof. Taylor T. Johnson. His major research areas include cyber-physical systems, hybrid systems, formal method, temporal logic, and model-based design. Particularly, he is interested in research related simulation-based testing, reachability analysis, specification mining and model-based repair of cyber-physical systems for improving safety and resiliency. Furthermore, he has been involved in the development of highly cited, state-of-the-art tools in this area.

What's new

  • August 2019: Paper accepted at MEMOCODE 2019

  • July 2019: Papers accepted at FM and FORMAT 2019

  • May 2019: Submitted a paper to ASE 2019

  • April 2019: Submitted two papers to FM 2019

  • April 2019: Paper accepted at FORTE 2019

  • March 2019: Paper accepted at FORMALISE 2019

  • Feb 2019: Submitted a paper to FORTRE 2019

  • Jan 2019: Submitted a paper to FORMALISE 2019

Research Interest

  • Cyber-Physical Systems: Formal Verification, Testing, and Specification Mining

  • Model-based Repair for Improving Resiliency of Hybrid Systems

  • Safe Artificial Intelligent Systems

  • Logic Driven Data Science

  • Software Engineering

Education

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)

Publications

  • Journal Articles:

    • 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 (2019) 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:

    • 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 19th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2019), San Diego, October 2019. (To Appear)

    • 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. (To Appear)

    • 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. (To Appear)

    • 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:

    • 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 20180286143, April 2018 (link)

Teaching

Teaching assistant at The University of Texas at Arlington for:

  • Operating Systems (CSE3320), Fall 2017 and Spring 2018

  • Object-oriented Programming (CSE1325), Spring 2014, Summer 2014, Fall 2014, and Spring 2015

Award and Honors

  • 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.