Experience :

• R&D Engineer, Verification Group, Synopsys Inc., CA, 06/2009 ~ present

Research and development in the verification engine of Magellan, Synopsys's formal property verification product.

• Senior member of technical staff, Averant, Inc., CA, 05/2007 ~ 06/2009

Research and development in the verification engine of Solidify, Averant's formal verification tool. Key contributor in the following projects:

1. New Verification Engine. Developed a new engine based on proprietary algorithms capable of proving some previously unproven properties.
2. Next Generation Testbench-less Bug Hunting.
3. Sequential Equivalence Checking.
4. Improved Debugging. Rewrote the debugging sub-system and delivered a 10X improvement in performance in some cases for complex designs.

• Research Assistant, Dept. of CS, University of California at Riverside, Riverside, CA, USA, 01/2004 ~ 05/2007

Symbolic model checking and formal verification (Lead by Prof. Gianfranco Ciardo and funded by NSF and NASA)

• Research Assistant, Dept. of CS, College of William & Mary, Williamsburg, VA, USA, 06/2003 ~ 12/2003

Symbolic model checking and formal verification (Lead by Prof. Gianfranco Ciardo and funded by NSF and NASA)

• Teaching Assistant, Dept. of CS, College of William & Mary, Williamsburg, VA, USA, 09/2000 ~ 06/2003.

Grading for Data Structures and Algorithms, and Discrete Mathematics.

Grading for undergraduate courses : Statistics,  Differential Equations,  Multivariable calculus;  Lab instructor for calculus.

Research Interests : 

My research interest is in systematic and automatic verification of complex hardware and software systems using formal techniques. 

•   Research:  

  •  BDDs, SAT-solver, Abstraction

  •  Symbolic Reachability Analysis, Symbolic Model Checking, Combinational and Sequential Equivalence Checking

•  Applications: 

  •  Hardware systems: Synchronous sequential circuits

  •  Software systems: Network Protocol verification, Program Verification, and Generalized Stochastic Petri nets 

Education :

•  Ph.D.   Computer Science  University of California, Riverside, CA. March 2008

•  M.S.    Computer Science  College of William & Mary, VA.   2002

•  B.S.     University of Science and Technology of China, Hefei, Anhui, China  2000

Publications :

Journal papers:

•   Andy Jinqing Yu, Gianfranco Ciardo  and  Gerald luettgen ,  Decision-diagram-based Techniques for Bounded Reachability Checking of Asynchronous Systems. , Accepted to a special issue of the international journal on SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (STTT), 2008.   

Conference papers:

•   Gianfranco Ciardo,  Andrew Miner, Min Wan and  Andy Jinqing Yu ,  Approximating stationary measures of structured continuous-time Markov models using matrix diagrams., SIGMETRICS Performance Evaluation Review 35(3): 16-18 (2007)   

•   Gianfranco Ciardo,  Gerald luettgen, and  Andy Jinqing Yu ,  Improving static variable order via invariants , Accepted to 28th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (ICATPN), Siedlce, Poland, June 25-29, 2007.   

       Postscript: ,  PDF:

•   Andy Jinqing Yu, Gianfranco Ciardo  and  Gerald luettgen ,  Bounded reachability checking of asynchronous systems using decision diagrams , Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of systems (TACAS), LNCS, 24 March-1 April, 2007, Braga, Portugal. (STUDENT PAPER AWARD)