Education:

Ph.D.  in   Computer Science  at   University of California-Riverside, Riverside, CA.   December 2007.

M.S.  in   Mathematics (Computational Track)  at   Ohio University, Athen, OH.   June 2001.

B.A.  in   History  at   Soochow University, Taipei, Taiwan.   June 1995.

Research Interest:

Parallel and distributed formal verification.

Selected Experience:

Senior R&D Engineer, Verification Group, Synopsys, Mountain View, CA. 06/07 ~ Present.
- Developing coarse-grained parallel model checker.

Research Intern, NEC Laboratories America, Inc., Princeton, NJ. 10/06 ~ 01/07.
- Developed message passing and load balancing management interfaces using for NEC internal model checkers, VeriSol (DiVer) and F-Soft.
- Supervised by Dr. Aarti Gupta, Dr. Malay Ganai, and Dr. Vineet Kahlon.

Research Intern, National Institute of Aerospace (NIA) (affiliated to NASA Langley Research Center), Hampton, VA. 05/06 ~ 07/06.
- Parallelized a coded model checker for verifying a very complex critical avionics systems, the NASA byzantine-fault tolerant self-stabilizing pulse synchronization protocol.
- Supervised by Dr. Radu I. Siminiceanu and funded by NASA LaRC.

Research Assistant, Department of Computer Science & Engineering, University of California-Riverside, Riverside, CA. 01/04 ~ 06/07.
- Developed a parallel and distributed model checker, SMARTNow and published several refereed conference papers on parallel and distributed model checking.
- Supervised by Dr. Gianfranco Ciardo and funded by NSF.

Research Assistant, Department of Computer Science, College of William & Mary, Williamsburg, VA. 01/03 ~ 12/03.
- Designed and implemented parallel verification algorithms within a large-scale software, SMART.
- Supervised by Dr. Gianfranco Ciardo and co-funded by NSF and NASA.

Publications: (DBLP)

Ming-Ying Chung, and Gianfranco Ciardo. Speculative Image Computation to Speedup Distributed Symbolic State-Space Generation. Journal of Logic and Computation. Invited Submission.   

Ming-Ying Chung, Gianfranco Ciardo, and Radu I. Siminiceanu. Caching, Hashing, and Garbage Collection for Distributed State Space Construction. Parallel and Distributed Methods in verifiCation (PDMC). July 2007. (paper.pdf)

Ming-Ying Chung, Gianfranco Ciardo, and Radu I. Siminiceanu. Distributed Saturation. NASA LaRC Technical Report. February 2007. (paper.pdf)

Ming-Ying Chung, Gianfranco Ciardo, and Andy Jinqing Yu. A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability Analysis. In Proc. Automated Technology for Verification and Analysis (ATVA). Beijing, China. LNCS Springer-Verlag. October 2006. (pp. 51-66)    (paper.pdf)

Ming-Ying Chung, and Gianfranco Ciardo. A Dynamic Firing Speculation to Speedup Distributed Symbolic State-Space Generation. In Proc. International Parallel & Distributed Processing Symposium (IPDPS). Rhodes Island, Greece. IEEE Computer Society Press. April 2006.    (paper.pdf) (slide.pdf)

Ming-Ying Chung, and Gianfranco Ciardo. A Pattern Recognition Approach for Speculative Firing Prediction in Distributed Saturation State-Space Generation. In Proc. Parallel and Distributed Methods in verifiCation (PDMC). Lisboa, Portugal. ENTCS Elsevier. July 2005. (pp. 65-79)    (paper.pdf) (slide.pdf)

Ming-Ying Chung, and Gianfranco Ciardo. Saturation NOW. In Proc. Quantitative Evaluation of Systems (QEST). Enschede, The Netherlands, IEEE Computer Society Press. September 2004. (pp. 272-281)    (paper.pdf) (slide.pdf)

Ming-Ying Chung, Gianfranco Ciardo, Susanna Donatelli, Ning He, Brigitte Plateau, William Stewart, Eiad Sulaiman, and Andy Jinqing Yu. A Comparison of Structural Formalisms for Modeling Large Markov Models. In Proc. Next Generation Software (NGS). Santa Fe, New Mexico, U.S.A.. IEEE Computer Society Press. April 2004. (pp. 196-203)    (paper.pdf)