Design automation has brought us from circuits with tens of transistors to multi-core CPUs with billions of transistors. It will also be a key enabler in bringing emerging cyber-physical systems such as smart medical devices and self-driving cars to market. However, despite decades of advances in automation, human inputs remain central to the design, verification and operation of computing systems. In this talk, I will present a set of formal techniques that either reduce the human effort or incorporate human factors in a principled way in these processes.
In the first part of the talk, I will summarize my research on reverse engineering untrusted circuit netlists. I will describe a systematic way to derive human comprehensible high-level structures from bit-level descriptions of digital circuits, and illustrate how formal methods such as symbolic simulation and equivalence checking make this possible. I will demonstrate the effectiveness of the approach on circuit benchmarks including a design with half a million gates. In the second part of the talk, I will focus on the synthesis of provably correct human-in-the-loop controllers. Similar to semi-autonomous vehicles, these are controllers whose correctness depends on the autonomous controller, the actions of the human operator, and the interaction between the two entities. I will show how to formalize the problem and automatically synthesize the controllers from temporal logic specifications. I will conclude by discussing my current research on designing safe and secure distributed cyber-physical systems and my future vision on human-centric formal methods.
Dr. Wenchao Li is currently Computer Scientist at SRI International. He received his Ph.D. in EECS from UC Berkeley in 2013. His research develops theory and tools for the construction of provably dependable systems, with a focus on human-centric formal methods. His research has been recognized with the ACM Outstanding Ph.D. Dissertation Award in Electronic Design Automation and the Leon O. Chua Award for outstanding achievement in nonlinear science.