Yan Peng

Table of Contents

PhD student
Department of Computer Science
University of British Columbia
2329 West Mall, Vancouver, BC V6T 1Z4

Email: (@ yanpeng '(cs . ubc . ca))

Introduction

Hi there! Glad that you find me. Hope you can get something useful for your life from here. Here is my CV.

I'm a second year PhD student at the University of British Columbia. I'm working with Professor Mark Greenstreet on formal verification. My interests are not constrained to a specific kind of verification. I wish at the end of my PhD I will be able to automatically verify to the lowest level of a physical phenomenon and to the highest level of a philosophical thought. And all these are only possible through the smart design and construction of an intelligent computer program.

Why do we need formal verification?

My supervisor made this comment the other day that I think gives some taste on why formal verification should be a requirement (not word by word):

I've been frustrated by ACL2 several times when it fails to prove my theorems, of which, about 10% to 20% of them are my fault. It is either because I made a typo or more importantly there is a real bug in my code. It is much better that ACL2 catches the bug than letting the bug slip into real designs.

Let's see if you can find what is wrong about this piece of code:

(defun replace-sublist (char-list old-list new-list)
  (cond ((endp char-list) nil)
        ((equal (take (len old-list) char-list) old-list)
         (append new-list (replace-sublist (nthcdr (len old-list) char-list) old-list new-list)))
        (t (cons (car char-list) (replace-sublist (cdr char-list) old-list new-list)))))

Research projects

Catching glitches in a net

paper

Just like what compilers do, in digital circuit design, a logic synthesis tool is used for compiling high-level RTL behavioural models into gate-level netlist implementations. Even though logic synthesis maintains boolean equivalence, it is still possible to introduce bugs into the netlist implementation even when the RTL behavioural model prohibits such bugs. This is due to the lack of knowledge about timing in logic synthesis.

We use the theorem prover ACL2 and the SAT solver Glucose to help circuit designers identify such bugs and we've got very nice results. This is the first time for me to use formal methods to solve a real-world-scale problem. The process is both challenging and exciting.

Integrating SMT solvers into a theorem prover

repository paper

My first project and my major project for now.

This is an idea that combines SMT solvers with a theorem prover. The starting point of this combination has nothing to do with an SMT solver, nor a theorem prover. Instead, we were aiming at proving global convergence of a digital Phase-Locked Loop. After a while of researching, we find Z3's arithmetic capabilities super powerful. We developed a mathematical proof. For arithmetic inequalities in the proof, which are not within the computing power of a human brain, we use Z3 for discharging the claims.

However, we are not satisfied with that, because there are still unproven theorems that form the other parts or the structure of this proof. For example, there is an induction proof that is very crucial to the circuit convergence. Unfortunately, the current Z3 does not handle that kind of induction proof. Then, ta-da, we found ACL2.

We combine Z3 as an external subprocedure for ACL2 and we call our interface Smtlink. With its help, we are able to formulate the other parts of our proof into ACL2 and when ACL2 becomes slow in proving complicated arithmetic formulas, we fire Z3.

A huge amount of work has been done to ensure the soundness of this integration, in the standard of a theorem prover. Check out the code and paper for details.

Machine learning proof

report

Mathmeticians working in the optimization aspect of machine learning have been continuously coming up with new optimization algorithms that promotes the efficiency of machine learning tasks. Simple algorithms had already been explored and new algorithms tend to be much more sophisticated as in why they should achieve better performance. A typical proof of convergence rate can expand 10 or more pages with a lot of details being omitted. In another perspective, the researchers have strong belief that they are over-constraining their algorithm parameters. It will be great if their proofs can be made symbolic so that they can easily push the parameters to the limit and see if the proofs will break.

This report is a very prelimitary attempt at automating machine learning proofs to solve above problems.

Automatic differentiation

report

Automatic differentiation automatically calculates the exact gradient of a function at a specific data point.

For analog circuits verification, it will be very useful if a program can easily calculates the tendency of change of any quantity in the circuit in comparison to another quantity. For example, we can properly model a correctness specification for a circuit in a mathematical function. We can also produce a mathematical model for a circuit. The correctness function will in some sense relate to the circuit model's state variables or even parameters. Thus, by calculating the derivatives, we are able to see the relative relations between those quantities. This information can be used in proving specifications of a circuit, generating new designs and etc.

This prelimitary work attempts at applying automatic differentiation to real circuit designs modeled in MATLAB functions.

Publications

Finding Glitches Using Formal Methods paper slides
Yan Peng, Ian W. Jones, Mark R. Greenstreet, The 22nd IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2016).

Extending ACL2 with SMT solvers paper slides
Yan Peng, Mark R. Greenstreet, 13th Inernational Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2015).

Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification paper slides
Yan Peng, Mark R. Greenstreet, NASA Formal Methods (NFM), Lecture Notes in Computer Science Volume 9058, 2015, pp 310-326.

AMS verification with Theorem Proving and SMT paper slides
Yan Peng, Mark R. Greenstreet, International Workshop on Frontiers in Analog CAD (FAC), Grenoble, France, July, 2014.

Verifying Global Convergence for a Digital Phase-Locked Loop paper slides
Jijie Wei, Yan Peng, Grace Yu, Mark R. Greenstreet, Proceedings of the 13th Conference on Formal Methods in Computer Aided Design (FMCAD), October, 2013, pp 113-120.

Thesis

Combining SMT with theorem proving for AMS verification : analytically verifying global convergence of a digital PLL thesis slides
Master of Science, Computer Science program, University of British Columbia, Vancouver, BC, Canada, April 28th 2015.

Posters and Talks

Verifying Global Convergence of a Digital Phase-Locked Loop with Z3 poster
Y. Peng, M. Greenstreet, International Workshop on Design Automation for Analog and Mixed-Signal Circuits, San Jose, CA, November, 2013.

Verifying Global Convergence of a Digital Phase-Locked Loop with Z3 slides
Microsoft, Redmond, WA, US, September, 2013.

Teaching

  • APSC160 Introduction to Computation in Engineering Design (2012 W1)
  • CPSC312 Functional and Logic Programming (2013 W1)
  • CPSC311 Definition of Programming Languages (2015 W1)

Other interests

I love English transcription and English translation into Chinese. I might also be interested in Chinese-to-English translation, but it might not be equally good. I'm a TED translator and coursera translator. Check out one of my favorite videos: Nathalie Cabrol: How Mars might hold the secret to the origin of life

I'm also a big fan of music and scifi readings. Check out this story that has given me a hit: The Algorithms for Love

Courses

  • CPSC501 Introduction to Theory of Computing
  • CPSC521 Parallel Algorithms and Architectures
  • CPSC542G Topics in Numerical Computation - BREADTH SCI COMP
  • CPSC406 Computational Optimization
  • CPSC513 Integrated System Design (Formal Verification)
  • CPSC502 Artificial Intelligence I
  • CPSC314 Computer Graphics
  • CPSC540 Machine Learning
  • CPSC509 Programming Language Principles (AUDIT)

Bug in the code?

What will happen if old-list is nil?

Author: Yan Peng

Created: 2017-07-20 Thu 15:57

Validate