Publications

Selected Publications:

  • TrojDRL: Evaluation of Backdoor Attacks on Deep Reinforcement Learning
    Panagiota Kiourti, Kacper Wardega, Susmit Jha and Wenchao Li.
    ACM/EDAC/IEEE Design Automation Conference (DAC), July 2020. [arXiv version]
    Implanting backdoors in deep reinforcement learning agents by poisoning only 0.025% of training data.
    Coverage by the WIRED magazine: “Tainted Data Can Teach Algorithms the Wrong Lessons” [link]
  • Towards Verification-Aware Knowledge Distillation for Neural-Network Controlled Systems
    Jiameng Fan, Chao Huang, Wenchao Li, Xin Chen and Qi Zhu.
    International Conference on Computer Aided Design (ICCAD), November 2019. [link to pdf]
    Verification made easier by reducing the Lipschitz constants of neural network controllers through knowledge distillation.
  • ReachNN: Reachability Analysis of Neural-Network Controlled Systems
    Chao Huang, Jiameng Fan, Wenchao Li, Xin Chen and Qi Zhu.
    International Conference on Embedded Software (EMSOFT), October 2019. [link to pdf][arXiv version]
    Verify neural-network controlled systems via Bernstein Polynomial approximation.
  • Safety-Guided Deep Reinforcement Learning via Online Gaussian Process Estimation
    Jiameng Fan and Wenchao Li.
    International Conference on Learning Representation (ICLR), Workshop on Safe Machine Learning: Specification, Robustness, and Assurance, May 2019. [pdf]
    Formulate the state-action value function of a notion of trajectory-based safety as a candidate Lyapunov function and extend control-theoretic results to approximate its derivative using online Gaussian Process estimation.
  • Formal Verification of Weakly-Hard Systems
    Chao Huang, Wenchao Li and Qi Zhu.
    International Conference on Hybrid Systems: Computation and Control (HSCC), April 2019. [link to pdf]
    Techniques for verifying the safety of nonlinear dynamical systems whose computation may miss deadlines under the (m, K) model.
  • Safety-Aware Apprenticeship Learning. [pdf]
    Weichao Zhou and Wenchao Li.
    International Conference on Computer Aided Verification (CAV), July 2018.
    Combine probabilistic model checking with apprenticeship learning to ensure both safety and performance in learning from demonstration.
  • Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities. [pdf]
    Sanjit A. Seshia, Shiyan Hu, Wenchao Li and Qi Zhu.
    IEEE Transactions on Computer-Aided Design of Circuits and Systems (TCAD), September 2017.
    A survey of unique challenges, opportunities and foundational directions for the design automation of CPS.
  • Design and Verification for Multi-Rate Distributed Systems. [pdf]
    Wenchao Li, Leonard Gerard and Natarajan Shankar.
    ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), September 2015.
    Model of computation, architectural description language specification, and formal verification techniques for building high-assurance CPS.
  • Synthesis for Human-in-the-Loop Control Systems.  [pdf]
    Wenchao Li, Dorsa Sadigh, S. Shankar Sastry and Sanjit A. Seshia.
    International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), April 2014.
    Synthesize provably safe controllers from high-level specifications with human-in-the-loop.
  • Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. [pdf]
    Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia.
    International Conference on Computer Aided Verification (CAV), July 2013.
    Verify PTCL properties of MDPs whose transition probabilities lie in convex uncertainty sets in polynomial time.
  • Reverse Engineering Circuits Using Behavioral Pattern Mining. [pdf]
    Wenchao Li, Zach Wasson and Sanjit A. Seshia.
    IEEE International Symposium on Hardware-Oriented Security and Trust (HOST), June 2012.
    Derive the high-level description of an unknown circuit given only its gate-level representation.
  • Mining Assumptions for Synthesis. [pdf]
    Wenchao Li, Lili Dworkin and Sanjit A. Seshia.
    ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2011.
    Find likely missing assumptions that cause specifications to be unrealizable.
  • Scalable Specification Mining for Verification and Diagnosis. [pdf]
    Wenchao Li, Alessandro Forin and Sanjit A. Seshia. 

    ACM/IEEE Design Automation Conference (DAC), June 2010.
    Efficiently mine temporal specifications from traces of millions of cycles in hardware designs and use the mined specifications to localize errors.
  • A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance. [pdf]
    Orna Kupferman, Wenchao Li and Sanjit A. Seshia. 

    IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), November 2008.
    A theory to study vacuity, coverage, and fault tolerance in a unified setting where mutations are applied either to the specification or to the implementation. 
  • Verification-guided soft error resilience. [pdf]
    Sanjit A. Seshia, Wenchao Li and Subhasish Mitra. 

    IEEE/ACM Conference on Design, Automation and Test in Europe (DATE), April 2007.
    Use model checking to identify the circuit components that must be protected to reduce the overhead of adding circuit mechanisms for error resilience.

Full Publication List: [Google Scholar Profile]

  1. Know the Unknowns: Addressing Disturbances and Uncertainties in Autonomous Systems
    Qi Zhu, Wenchao Li, Hyoseung Kim, Yecheng Xiang, Kacper Wardega, Zhilu Wang, Yixuan Wang, Hengyi Liang, Chao Huang, Jiameng Fan, Hyunjong Choi.
    International Conference on Computer Aided Design (ICCAD), November 2020 (to appear).
  2. Runtime-Safety-Guided Policy Repair
    Weichao Zhou, Ruihan Gao, BaekGyu Kim, Eunsuk Kang and Wenchao Li.
    The 20th International Conference on Runtime Verification (RV), October 2020.
  3. Divide and Slide: Layer-Wise Refinement for Output Range Analysis of Deep Neural Networks
    Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li and Qi Zhu.
    International Conference on Embedded Software (EMSOFT), September 2020.
  4. ReachNN*: A Tool for Reachability Analysis ofNeural-Network Controlled Systems
    Jiameng Fan, Chao Huang, Xin Chen, Wenchao Li and Qi Zhu.
    The 18th International Symposium on Automated Technology for Verification and Analysis (ATVA), October 2020 (to appear). 
  5. TrojDRL: Evaluation of Backdoor Attacks on Deep Reinforcement Learning
    Panagiota Kiourti, Kacper Wardega, Susmit Jha and Wenchao Li.
    ACM/EDAC/IEEE Design Automation Conference (DAC), July 2020. [arXiv version]
    Coverage by the WIRED magazine: “Tainted Data Can Teach Algorithms the Wrong Lessons” [link]
  6. Opportunistic Intermittent Control with Safety Guarantees for Autonomous Systems
    Chao Huang, Shichao Xu, Zhilu Wang, Shuyue Lan, Wenchao Li and Qi Zhu.
    ACM/IEEE Design Automation Conference (DAC), July 2020.
  7. Application-Aware Scheduling of Networked Applications over the Low-Power Wireless Bus
    Kacper Wardega and Wenchao Li.
    Design, Automation and Test in Europe Conference (DATE), March 2020.
  8. Towards Verification-Aware Knowledge Distillation for Neural-Network Controlled Systems
    Jiameng Fan, Chao Huang, Wenchao Li, Xin Chen and Qi Zhu.
    International Conference on Computer Aided Design (ICCAD), November 2019.
  9. ReachNN: Reachability Analysis of Neural-Network Controlled Systems
    Chao Huang, Jiameng Fan, Wenchao Li, Xin Chen and Qi Zhu.
    International Conference on Embedded Software (EMSOFT), October 2019.
  10. Safety-Guided Deep Reinforcement Learning via Online Gaussian Process Estimation
    Jiameng Fan and Wenchao Li.
    International Conference on Learning Representation (ICLR), Workshop on Safe Machine Learning: Specification, Robustness, and Assurance, May 2019.
  11. Resilience of Multi-Robot Systems to Physical Masquerade Attacks
    Kacper Wardega, Roberto Tron and Wenchao Li.
    IEEE Workshop on the Internet of Safe Things (SafeThings), May 2019.
  12. Masquerade Attack Detection Through Observation Planning for Multi-Robot Systems
    Kacper Wardega, Roberto Tron and Wenchao Li.
    International Conference on Autonomous Agents and Multiagent Systems (AAMAS), May 2019.
  13. Exploring Weakly-hard Paradigm for Networked Systems
    Chao Huang, Kacper Wardega, Wenchao Li and Qi Zhu.
    International Workshop on Design Automation for CPS and IoT (DESTION), April 2019.
  14. Formal Verification of Weakly-Hard Systems
    Chao Huang, Wenchao Li and Qi Zhu.
    International Conference on Hybrid Systems: Computation and Control (HSCC), April 2019.
  15. Safety-Aware Apprenticeship Learning.
    Weichao Zhou and Wenchao Li.
    International Conference on Computer Aided Verification (CAV), July 2018.
  16. Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities.
    Sanjit A. Seshia
    , Shiyan Hu, Wenchao Li and Qi Zhu.
    IEEE Transactions on Computer-Aided Design of Circuits and Systems (TCAD), September 2017.
  17. Extensibility-Driven Automotive In-Vehicle Architecture Design.
    Qi Zhu, Hengyi Liang, Licong Zhang, Debayan Roy, Wenchao Li and Samarjit Chakraborty.
    ACM/IEEE Design Automation Conference (DAC), June 2017.
  18. Delay-Aware Design, Analysis and Verification of Intelligent Intersection Management.
    Bowen Zheng, Chung-Wei Lin, Hengyi Liang, Shinichi Shiraishi, Wenchao Li and Qi Zhu.
    IEEE International Conference on Smart Computing (SMARTCOMP), May 2017.
  19. Analysis of Production Data Manipulation Attacks in Petroleum Cyber-Physical Systems.
    Xiaodao Chen, Yuchen Zhou, Hong Zhou, Chaowei Wan, Qi Zhu, Wenchao Li and Shiyan Hu.
    IEEE/ACM International Conference on Computer-Aided Design (ICCAD), November 2016.
  20. Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems.
    Devesh Bhatt, Arunabh Chattopadhyay, Wenchao Li, David Oglesby, Sam Owre and Natarajan Shankar.
    NASA Formal Methods Symposium (NFM), June 2016.
  21. ARSENAL: Automatic Requirements Specification Extraction from Natural Language.
    Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar and Wilfried Steiner.
    NASA Formal Methods Symposium (NFM), June 2016.
  22. Detecting Similar Programs via the Weisfeiler-Leman Graph Kernel.
    Wenchao Li, Hassen Saidi, Huascar Sanchez, Martin Schaf, and Pascal Schweitzer.
    International Conference on Software Reuse (ICSR), June 2016.
  23. Design and Verification for Multi-Rate Distributed Systems.
    Wenchao Li, Leonard Gerard and Natarajan Shankar.
    ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), September 2015. 
  24. Design and Verification for Transportation System Security.
    Bowen Zheng, Wenchao Li, Peng Deng, Leonard Gerard, Qi Zhu and Natarajan Shankar.
    ACM/IEEE Design Automation Conference (DAC), June 2015.
  25. Synthesis for Human-in-the-Loop Control Systems.
    Wenchao Li, Dorsa Sadigh, S. Shankar Sastry and Sanjit A. Seshia.
     International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), April 2014.
  26. Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior.
    Dorsa Sadigh, Katherine Driggs-Campbell, Alberto Puggelli, Wenchao Li, Victor Shia, Ruzena Bajcsy, Alberto Sangiovanni-Vincentelli, S. Shankar Sastry and Sanjit A. Seshia.
    AAAI Symposium on Modeling in Human Machine Systems: Challenges for Formal Verification, March 2014.
  27. Reverse Engineering Digital Circuits Using Structural and Functional Analyses.
    Pramod Subramanyan, Nestan Tsiskaridze, Wenchao Li, Adria Gascon, Wei Yang Tan, Ashish Tiwari, Natarajan Shankar, Sanjit A. Seshia and Sharad Malik.
    IEEE Transactions on Emerging Topics in Computing: Special Issue on Nanoscale Architectures for Hardware Security, Trust and Reliability (TETC), December 2013.
  28. Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties.
    Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia. 
    International Conference on Computer Aided Verification (CAV), July 2013. [Longer Tech. Report Version]
  29. WordRev: Finding Word-Level Structures in a Sea of Bit-Level Gates.
    Wenchao Li, Adria Gascon, Pramod Subramanyan, Wei Yang Tan, Ashish Tiwari, Sharad Malik, Natarajan Shankar, Sanjit A. Seshia.
    IEEE International Symposium on Hardware-Oriented Security and Trust (HOST), June 2013.
  30. Power-Aware Dynamic Control of Error-Resilience Mechanisms.
    Wenchao Li, Susmit Jha and Sanjit A. Seshia.
    Workshop on Silicon Errors in Logic – System Effects (SELSE), March 2013.
  31. Sparse Coding for Specification Mining and Error Localization.
    Wenchao Li and Sanjit A. Seshia.
    International Conference on Runtime Verification (RV), September 2012.
  32. Reverse Engineering Circuits Using Behavioral Pattern Mining.
    Wenchao Li, Zach Wasson and Sanjit A. Seshia. 

    IEEE International Symposium on Hardware-Oriented Security and Trust (HOST), June 2012.
  33. CrowdMine: Towards Crowdsourced Human-Assisted Verification.
    Wenchao Li, Sanjit A. Seshia and Somesh Jha.
    ACM/IEEE Design Automation Conference (DAC), June 2012.
  34. Mining Assumptions for Synthesis.
    Wenchao Li, Lili Dworkin and Sanjit A. Seshia.
    ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2011.
  35. Scalable Specification Mining for Verification and Diagnosis.
    Wenchao Li, Alessandro Forin and Sanjit A. Seshia.
    ACM/IEEE Design Automation Conference (DAC), June 2010.
  36. Localizing Transient Faults Using Dynamic Bayesian Networks.
    Susmit Jha, Wenchao Li and Sanjit A. Seshia.
    IEEE International High Level Design Validation and Test Workshop (HLDVT), November 2009.
  37. Algorithms for Green Buildings: Learning-Based Techniques for Energy Prediction and Fault Diagnosis.
    Daniel Holcomb, Wenchao Li and Sanjit A. Seshia.
    Technical Report, University of California, Berkeley, UCB/EECS-2009-138, October 2009.
  38. Optimizations of an Application-Level Protocol for Enhanced Dependability in FlexRay.
    Wenchao Li, Marco D. Natale, Wei Zheng, Paolo Giusto, Alberto Sangiovanni-Vincentelli and Sanjit A. Seshia.
    IEEE/ACM Design, Automation and Test in Europe (DATE), April 2009.
  39. Design as You See FIT: System-Level Soft Error Analysis of Sequential Circuits.
    Daniel Holcomb, Wenchao Li and Sanjit A. Seshia.
    IEEE/ACM Design, Automation and Test in Europe (DATE), April 2009.
  40.  A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance.
    Orna Kupferman, Wenchao Li and Sanjit A. Seshia.

    IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), November 2008.
  41. On the Duality between Vacuity and Coverage.
    Orna Kupferman, Wenchao Li and Sanjit A. Seshia.
    Technical Report, University of California, Berkeley, UCB/EECS-2008-26, March 2008.
  42. Verification-guided soft error resilience.
    Sanjit A. Seshia, Wenchao Li and Subhasish Mitra. 

    IEEE/ACM Conference on Design, Automation and Test in Europe (DATE), April 2007.
  43. Physical Activity Monitoring for Assisted Living at Home.
    Roozbeh Jafari, Wenchao Li, Ruzena Bajcsy, Steven Glaser and Shankar Sastry.
    International Conference on Body Sensor Networks (BSN), March 2007.

Theses:

  • Specification Mining: New Formalisms, Algorithms and Applications.
    Wenchao Li.
    Ph.D. Thesis, University of California, Berkeley. [Tech. Report Link]
  • Formal Methods for Reverse Engineering Gate-Level Netlists.
    Wenchao Li.
    Master Report, University of California, Berkeley. [Tech. Report Link]

The documents referenced on this page are included by the contributing authors as a means to ensure timely dissemination of technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author’s or owner’s copyright.