Yuan Lu's Resume

Yuan Lu

4909 Centre Ave Apt 14
Pittsburgh, PA 15213
U.S.A.

Phone: (412)-268-3730 (office)
Phone: (412)-683-1383 (home)
Email: yuanlu@cs.cmu.edu
WWW: http://www.cs.cmu.edu/~yuanlu

OBJECTIVE

Seeking engineer/research position on design verification, protocol/security design and verification, or VLSI CAD.

EDUCATION

BSc. Department of Electrical Engineering, Jiao Tong University, China, 1992 (GPA 3.88/4.00).

MSc. Department of Electrical and Computer Engineering, University of Iowa, 1996 (GPA : 4.00/4.00)

Ph.D. Department of Electrical and Computer Engineering, Carnegie Mellon University, 2000

COURSE HIGHLIGHT

Formal Verification	Computer Architecture
VLSI CAD and Design	Mathematical Logic
Digital Design using HDL	C++ Language
Testing Digital Circuits	IC Manufacture
Superscalar Processor Design	Algorithm and Graph Theory
Software Engineering	Operating Systems

INDUSTRIAL EXPERIENCE

Fujitsu Lab of America, CA (Summer of 1997 and 1998)

PROJECTS

Formal Specification for Bus Protocol	Develop techniques to specify bus protocol (eg. PCI Local bus) formally and automatically check the consistency of the protocol specifications. Currently, we use LTL to specify the protocol and ATL to verify the consistency.
New Abstraction Techniques for Model Checking	Target to develop new abstraction-refinement techniques to model-check the large industrial hardware designs. The techniques include value-driven static program analysis and refinement procedures.
Verifying Industrial IP-Cores	Developping techniques automatic techniques to verify industrial IP based designs.

Projects in the past

aBDD based Model Checking	Using abstract BDD to reduce the abstraction cost for large designs.
Verifying PCI Bus Protocol	Verifing basic PCI local bus protocol using SMV and found a bug in the protocol
Variable Ordering Using aBDD	Generating samples of a boolean function using aBDD and selecting the order to minimize the BDD size. This approach can obtain the known-best results for ISCAS85 circuits.

PUBLICATIONS

Edmund Clarke, Somesh Jha, Yuan Lu, Helmut Veith, Tree-like Counterexamples in Model Checking. Logic In Computer Science (LICS'02), 2002
Yuan Lu, Weimin Li, A Semi-formal Verification Methodology. invited paper in Asian ASIC Conference (ASICON'01), 2001
Edmund Clarke, Steve German, Yuan Lu, Helmut Veith, Dong Wang, Excutable Protocol Specifications in ESL. Formal Methods in Computer-Aided Design (FMCAD'00), 2000
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided Abstraction Refinement. Computer-Aided Verification (CAV'00), July 2000
Yuan Lu, Jawahar Jain, Edmund Clarke and Masahiro Fujita. Efficient Variable Ordering Using an aBDD Based Sampling. 37th Design Automation Conference (DAC'00), 2000
Jawahar Jain, Dinos, Ingor Wegner, Yuan Lu. Analysis of Composition, and How to Obtain Smaller Canonical Graphs. 37th Design Automation Conference (DAC'00), 2000
Yuan Lu, Jawahar Jain, Koichiro Takayama. BDD Variable Ordering Using Window-based Sampling. International Workshop in Logic Synthesis (IWLS'00), 2000
Edmund Clarke, Somesh Jha, Yuan Lu, and Dong Wang. Abstract BDDs: A Technique for Using Abstraction in Model Checking. Proceedings of CHARME'99, in LNCS 1703. September, 1999
Pankaj Chauhan, Edmund Clarke, Yuan Lu, and Dong Wang. Verifying IP-Core Based System-on-chip Designs. IEEE Intl. ASIC/SOC Conference, 1999
Somesh Jha, Yuan Lu, Marius Minea, and Edmund Clarke. Equivalence Checking Using Abstract BDDs. IEEE Computer Design Conference (ICCD'97), October 1997

REFERENCE

Edmund M. Clarke	FORE Systems Professor in CS
Phone: (412)-268-2628	Carnegie Mellon University