Publications

Selected Publications:

  • POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems
    Yixuan Wang*, Weichao Zhou*, Jiameng Fan, Zhilu Wang, Jiajun Li, Xin Chen, Chao Huang, Wenchao Li, and Qi Zhu. (* indicating equal contributions)
    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2023.
    POLAR-Express is the state-of-the-art tool for reachability analysis of neural-network controlled systems.
  • Byzantine Resilience at Swarm Scale: A Decentralized Blocklist Protocol from Inter-robot Accusations
    Kacper Wardega, Max von Hippel, Roberto Tron, Cristina Nita-Rotaru and Wenchao Li.
    The 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 2023.
    This work proposes the use of a decentralized blocklist protocol (DBP) based on inter-robot accusations as a means to provide Byzantine resilience for multi-robot systems. DBP generalizes to applications not implemented via the Linear Consensus Protocol and is adaptive to the number of Byzantine robots while simultaneously reducing the required network connectivity compared with the Weighted-Mean Subsequence Reduced (W-MSR) algorithm. 
  • POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems
    Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li and Qi Zhu.
    The 20th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2022. [arXiv version][tool link]
    POLAR is a principled framework for reachability analysis of neural-network controlled systems based on Taylor model propagation. It substantially outperforms current SOTA techniques for this problem in terms of general applicability, efficiency, and precision. 
  • DRIBO: Robust Deep Reinforcement Learning via Multi-View Information Bottleneck
    Jiameng Fan and Wenchao Li.
    The 39th International Conference on Machine Learning (ICML), 2022. [arXiv version]
    Introduces a novel multi-view information bottleneck (MIB) objective that maximizes the mutual information between sequences of observations and sequences of representations while reducing the task-irrelevant information identified through the multi-view observations. Achieves state-of-the-art results on the DeepMind Control Suite (with videos playing in the background as visual distractors) and the Procgen Benchmark (in terms of the performance of generalizing the learned policy to unseen levels).
  • A Hierarchical Bayesian Approach to Inverse Reinforcement Learning with Symbolic Reward Machines
    Weichao Zhou and Wenchao Li.
    The 39th International Conference on Machine Learning (ICML), 2022. [arXiv version]
    Proposes a novel reward function structure called symbolic reward machines (SRMs) and a hierarchical Bayesian approach for inferring appropriate reward outputs in the SRMs from expert demonstrations. Experimental results demonstrate significant improvements in training efficiency and the ability to generalize across different environment configurations for complex RL tasks.
  • Sound and Complete Neural Network Repair with Minimality and Locality Guarantees
    Feisi Fu and Wenchao Li.
    The 10th International Conference on Learning Representations (ICLR), 2022.
    First sound and complete repair method for repairing ReLU networks with strong guarantees on minimality and locality of the resulting changes.
  • Programmatic Reward Design by Example
    Weichao Zhou and Wenchao Li.
    36th AAAI Conference on Artificial Intelligence (AAAI), 2022.
    Reward design is a fundamental problem in reinforcement learning. We propose a novel paradigm of using programs to specify the reward function. Another major contribution of this paper is a probabilistic framework that can infer the best candidate programmatic reward function from expert demonstrations.
  • MISA: Online Defense of Trojaned Models using Misattributions
    Panagiota Kiourti, Wenchao Li, Anirban Roy, Karan Sikka and Susmit Jha.
    Annual Computer Security Applications Conference (ACSAC), 2021. [arXiv version]
    A novel attribution-based method for detecting Trojan triggers for neural networks at inference time. 
  • Adversarial Training and Provable Robustness: A Tale of Two Objectives
    Jiameng Fan and Wenchao Li.
    The 35th AAAI Conference on Artificial Intelligence (AAAI), February 2021. [arXiv version][code]
    A principled framework that combines adversarial training and provable robustness verification for training certifiably robust neural networks. Achieves state-of-the-art results for l_\infty provable robustness.
  • 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.
    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), Volume: 39, Issue: 11, PP. 3323 – 3335, November 2020. [link to pdf]
    Combines propagation-based and constraint programming-based methods for output range analysis of DNNs. Achieves state-of-the-art results for l_\infty-norm-bounded perturbations.
  • 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][code]
    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.
    ACM Transactions on Embedded Computing Systems (TECS), Volume 18, Issue 5s, Article 106, October 2019. [link to pdf][arXiv version][code]
    Formal verification of neural-network controlled systems via Bernstein Polynomial approximation. Generally applicable to any Lipschitz-continuous neural network.
  • 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.
    Combines 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.
    Synthesizes 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.
    Verification of PTCL properties for 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.
    Deriving 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.
    Finding 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]

    • Secure Control of Connected and Automated Vehicles Using Trust-Aware Robust Event-Triggered Control Barrier Functions
      H M Sabbir Ahmad, Ehsan Sabouni, Akua Dickson, Wei Xiao, Christos Cassandras and Wenchao Li.
      ISOC Symposium on Vehicle Security and Privacy (VehicleSec), 2024 (to appear).
    • DeLF: Designing Learning Environments with Foundation Models
      Aida Afshar and Wenchao Li.
      The 38th Annual AAAI Conference on Artificial Intelligence (AAAI), Workshop on Synergy of Reinforcement Learning and Large Language Models, 2024 (to appear).
    • REGLO: Provable Neural Network Repair for Global Robustness Properties
      Feisi Fu, Zhilu Wang, Weichao Zhou, Yixuan Wang, Jiameng Fan, Chao Huang, Zhu Qi, Xin Chen and Wenchao Li.
      The 38th Annual AAAI Conference on Artificial Intelligence (AAAI), 2024 (to appear).
    • Universal Trojan Signatures in Reinforcement Learning
      Manoj Acharya, Weichao Zhou, Anirban Roy, Xiao Lin, Wenchao Li and Susmit Jha.
      Annual Conference on Neural Information Processing Systems (NeurIPS), Workshop on Backdoors in Deep Learning (BUGS), 2023.
    • POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems
      Yixuan Wang*, Weichao Zhou*, Jiameng Fan, Zhilu Wang, Jiajun Li, Xin Chen, Chao Huang, Wenchao Li and Qi Zhu. (* indicating equal contributions)
      IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2023.
    • Verification and Design of Robust and Safe Neural Network-enabled Autonomous Systems
      Qi Zhu, Wenchao Li, Chao Huang, Xin Chen, Weichao Zhou, Yixuan Wang, Jiajun Li and Feisi Fu.
      The 59th Annual Allerton Conference on Communication, Control, and Computing (Allerton), 2023 (Invited).
    • Dormant Neural Trojans
      Feisi Fu, Panagiota Kiourti and Wenchao Li.
      The 22nd IEEE International Conference on Machine Learning and Applications (ICMLA), 2023.
    • Merging Control in Mixed Traffic with Safety Guarantees: A Safe Sequencing Policy with Optimal Motion Control
      Ehsan Sabouni, H M Sabbir Ahmad, Wei Xiao, Christos G. Cassandras and Wenchao Li.
      The 26th IEEE International Conference on Intelligent Transportation Systems (ITSC), 2023.
    • Trust-Aware Resilient Control and Coordination of Connected and Automated Vehicles
      H M Sabbir Ahmad, Ehsan Sabouni, Wei Xiao, Christos G. Cassandras and Wenchao Li.
      The 26th IEEE International Conference on Intelligent Transportation Systems (ITSC), 2023.
    • Optimal Control of Connected Automated Vehicles with Event-Triggered Control Barrier Functions: a Test Bed for Safe Optimal Merging
      Ehsan Sabouni*, H M Sabbir Ahmad*, Wei Xiao, Christos G. Cassandras and Wenchao Li. (* indicating joint first-authors)
      The 7th IEEE Conference on Control Technology and Applications (CCTA), 2023 (Outstanding Student Paper Award).
    • Evaluations of Cyber Attacks on Cooperative Control of Connected and Autonomous Vehicles at Bottleneck Points
      H M Sabbir Ahmad, Ehsan Sabouni, Wei Xiao, Christos G. Cassandras and Wenchao Li.
      ISOC Symposium on Vehicle Security and Privacy (VehicleSec), 2023.
    • Byzantine Resilience at Swarm Scale: A Decentralized Blocklist Protocol from Inter-robot Accusations
      Kacper Wardega, Max von Hippel, Roberto Tron, Cristina Nita-Rotaru and Wenchao Li.
      The 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 2023.
    • HoLA Robots: Mitigating Plan-Deviation Attacks in Multi-Robot Systems with Co-Observations and Horizon-Limiting Announcements
      Kacper Wardega, Max von Hippel, Roberto Tron, Cristina Nita-Rotaru and Wenchao Li.
      The 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 2023.
    • REGLO: Provable Neural Network Repair for Global Robustness Properties
      Feisi Fu, Zhilu Wang, Jiameng Fan, Yixuan Wang, Chao Huang, Qi Zhu, Xin Chen and Wenchao Li.
      NeurIPS Workshop on Trustworthy and Socially Responsible Machine Learning (TSRML), 2022.
    • POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems
      Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li and Qi Zhu.
      The 20th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2022. [arXiv version]
    • DRIBO: Robust Deep Reinforcement Learning via Multi-View Information Bottleneck
      Jiameng Fan and Wenchao Li.
      The 39th International Conference on Machine Learning (ICML), 2022. [arXiv version]
    • A Hierarchical Bayesian Approach to Inverse Reinforcement Learning with Symbolic Reward Machines
      Weichao Zhou and Wenchao Li.
      The 39th International Conference on Machine Learning (ICML), 2022. [arXiv version]
    • Sound and Complete Neural Network Repair with Minimality and Locality Guarantees
      Feisi Fu and Wenchao Li.
      The 10th International Conference on Learning Representations (ICLR), 2022. [arXiv version]
    • Programmatic Reward Design by Example
      Weichao Zhou and Wenchao Li.
      The 36th AAAI Conference on Artificial Intelligence (AAAI), 2022. [arXiv version]
    • Opportunistic Communication with Latency Guarantees for Intermittently-Powered Devices
      Kacper Wardega, Wenchao Li, Hyoseung Kim, Yawen Wu, Zhenge Jia and Jingtong Hu.
      Design, Automation and Test in Europe Conference (DATE), 2022.
    • MISA: Online Defense of Trojaned Models using Misattributions
      Panagiota Kiourti, Wenchao Li, Anirban Roy, Karan Sikka and Susmit Jha.
      Annual Computer Security Applications Conference (ACSAC), 2021.
    • Cross-Layer Adaptation with Safety-Assured Proactive Task Job Skipping
      Zhilu Wang, Chao Huang, Hyoseung Kim, Wenchao Li and Qi Zhu.
      ACM Transactions on Embedded Computing Systems (TECS), 2021.
    • Adversarial Training and Provable Robustness: A Tale of Two Objectives
      Jiameng Fan and Wenchao Li.
      The 35th AAAI Conference on Artificial Intelligence (AAAI), February 2021.
    • 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 and Hyunjong Choi.
      International Conference on Computer Aided Design (ICCAD), November 2020.
    • 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.
    • 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.
      IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), Volume: 39, Issue: 11, PP. 3323 – 3335, November 2020.
    • ReachNN*: A Tool for Reachability Analysis of Neural-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. 
    • 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]
    • 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.
    • 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.
    • 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.
    • ReachNN: Reachability Analysis of Neural-Network Controlled Systems
      Chao Huang, Jiameng Fan, Wenchao Li, Xin Chen and Qi Zhu.
      ACM Transactions on Embedded Computing Systems (TECS), Volume 18, Issue 5s, Article 106, October 2019.
    • 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.
    • 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.
    • 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.
    • 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.
    • Formal Verification of Weakly-Hard Systems
      Chao Huang, Wenchao Li and Qi Zhu.
      International Conference on Hybrid Systems: Computation and Control (HSCC), April 2019.
    • Safety-Aware Apprenticeship Learning.
      Weichao Zhou and Wenchao Li.
      International Conference on Computer Aided Verification (CAV), July 2018.
    • 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.
    • 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.
    • 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.
    • 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.
    • 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.
    • 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.
    • 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.
    • 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. 
    • 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.
    • 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.
    • 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.
    • 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.
    • 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]
    • 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.
    • 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.
    • Sparse Coding for Specification Mining and Error Localization.
      Wenchao Li and Sanjit A. Seshia.
      International Conference on Runtime Verification (RV), September 2012.
    • 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.
    • CrowdMine: Towards Crowdsourced Human-Assisted Verification.
      Wenchao Li, Sanjit A. Seshia and Somesh Jha.
      ACM/IEEE Design Automation Conference (DAC), June 2012.
    • 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.
    • Scalable Specification Mining for Verification and Diagnosis.
      Wenchao Li, Alessandro Forin and Sanjit A. Seshia.
      ACM/IEEE Design Automation Conference (DAC), June 2010.
    • 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.
    • 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.
    • 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.
    • 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.
    •  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.
    • 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.
    • 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.
    • 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.