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:

Formal verification (model checking), parallel computing, distributed system.

Experience:

Senior R&D Engineer, Verification Group, Synopsys, Hillsboro, OR. 10/10 ~ Present.
- Developed a grid model checker which applies coarse-grained parallelism on formal verification.

Research Associate, Department of Systems & Information Engineering, University of Virginia, Charlottesville, VA. 07/10 ~ 09/10.
- Develop developing an infrastructure allowing formal verification and simulation tools to collaborate on trace analysis and to examine autonomy and authority safety issues in flight critical systems.
- Supervised by Prof. Ellen Bass and funded by NASA Ames.

Senior R&D Engineer, Verification Group, Synopsys, Mountain View, CA. 06/07 ~ 04/10.
- Developed a grid model checker which applies coarse-grained parallelism on formal verification.
- Tuned the orchestration of tool: coordinating various types of formal engines.
- Designed (artificial-intelligence-based) mechanisms for the tool to learn and manipulate orchestration on-the-fly to cope with various types of design.
- Studied 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 and Dr. Malay Ganai.

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 Prof. 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 Prof. Gianfranco Ciardo and co-funded by NSF and NASA.

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 Prof. Gianfranco Ciardo and co-funded by NSF and NASA.

Teaching Assistant, Department of Computer Science College of William & Mary, Williamsburg, VA. 09/02 ~ 12/02.
- Grader of a graduate-level course (Data Structures and Algorithms) and a senior-level course (Computer Organization).

Software Engineer, First International Computer (FIC), Taipei, Taiwan, 07/01 ~ 12/01.
- Maintained a software suite developed in C and GTK for personal information management in embedded system Linux (Midori).

Teaching Assistant, Department of Mathematics, Ohio University, Athens, OH. 09/00 ~ 06/01.
- Lectur of a freshman-level course (Introduction to Algebra).

Teaching Assistant, School of Art, Ohio University, Athens, OH. 09/99 ~ 03/01.
- Lectur of a freshman-level course (Introduction to Photography).
- Grader of a senior-level course (Advanced Photography).

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)