Since May 2007, I have been working full time as a senior member of technical stuff at Averant, Inc.

My job is to do research and development in the verification engine of Solidify, Averant's formal verification tool.

Please send email to   .

I only check my old email   every now and then.

Research Interests : 

I'm a member of the Logic and Stochastic Verification Lab at U.C. Riverside. My advisor is Dr. Gianfranco Ciardo. 

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

•   Research:  

  •  BDDs, Automata, SAT-solver, Predicate abstraction

  •  Symbolic Reachability Analysis, Symbolic Model Checking, and Symbolic Evaluation Trajectory

•  Applications: 

  •  Hardware systems: Asynchronous circuits, Synchronous 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 :

Conference papers:

•   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 2007), 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)   

•  Asynchronous circuits: 

  •   Distributed mutual exclusion (DME) circuit benchmark (from NuSMV distribution).  

    •   The state space (1.1*10^189 states) of the DME circuit models with 200 cells can be easily constructed in 14 seconds, using the technique described in my CHARME2005 paper. Significantly outperforms all other BDD-based and SAT-based techniques, e.g. NuSMV and VIS symbolic model checker.    

    •  Links: NuSMV DME circuit models with 16 cells 

    •  Case study on DME circuit performed by Dr. Ken L. McMillan using his unfolding technique,  "A Technique of State Space Search Based on Unfoldings", Formal Methods in System Design, 6, pp. 45-65, 1995.

•  Network protocol:

  •   Leader election protocol    

Experience :

Research Assistant, Dept. of CS, University of California at Riverside, Riverside, CA, USA, 01/04 ~ Present

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

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/02 ~ 06/03

Grading for Data Structures and Algorithms, and Discrete Mathematics.

Teaching Assistant, Dept. of Mathematics, College of William & Mary, Williamsburg, VA, USA, 09/00 ~ 09/02 

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