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 model checking.

Selected Experience:

Senior R&D Engineer, Verification Group, Synopsys, Mountain View, CA. 06/07 ~ Present.
- Develop a grid model checker which applies coarse-grained parallelism on formal verification.
- Tune the orchestration of tool: coordinating various types of formal engines.
- Design (artificial-intelligence-based) mechanisms for the tool to learn and manipulate orchestration on-the-fly to cope with various types of design.
- Study research papers to gather industrial and academic innovations.

Research Intern, NEC Laboratories America, Inc., Princeton, NJ. 10/06 ~ 01/07.
- Designed message passing and load balancing management interfaces allowing users to parallelize their formal verification tools, in particular Verisol and FSoft, with less effort.
- Implemented these interfaces (10 thousand lines of C code) using LAM/MPI and pthread and documented them using NaturalDoc.
- 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 C++ coded model checker for verifying critical avionics systems, in particular, the NASA byzantine-fault tolerant self-stabilizing pulse synchronization protocol.
- Published a NASA LaRC Tech. Report on the work.
- 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 model checker, SmartNOW, including 23 thousand lines of C code integrated with LAM/MPI and Omni-OpenMP.
- Published several research papers on parallel/distributed model checking.
- Responsible for setup a Linux-based heterogeneous cluster providing parallel computing tools, LAM/MPI, MPICH, Omni-OpenMP, PBS, etc.
- Worked on a 64-processor SGI Altix 4700 supercomputer system.
- 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:

Ming-Ying Chung, and Gianfranco Ciardo. Speculative Image Computation to Speedup Distributed Symbolic State-Space Generation. Journal of Logic and Computation. Oxford University Press. Feb. 2009.    (paper.pdf)

Ming-Ying Chung. Distributed Symbolic Reachability Analysis. PhD Thesis. University of California Riverside Press. Dec. 2007.    (paper.pdf) (slide.pdf)

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)