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 (aka model checking), parallel and distributed computing, and artificial intelligence.

Experience:

Senior R&D II Engineer, Verification Group, Synopsys, Hillsboro, OR. 10/10 ~ Present.
- Designed a new distributed verification infrastructure, Tanglewood, which provides formal verification service, allows third party tools (any executable understanding common verification formats, eg. AIG, SNL, DFG, etc) to be plug-in without hassle, and supports programmable orchestration language.
- Collaborated with two engineers, implemented Tanglewood in C and CDPL (Synopsys internal distributed processing library), delivered this tool in release quality in 12 months. Has been tested to scale upto 1K nodes.
- Tanglewood has already been integrated under existing verification products, eg. Magellan, to as the new backend engine and reported 2~3X speedup on customer’s real world benchmark.

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 II Engineer, Verification Group, Synopsys, Mountain View, CA. 06/07 ~ 04/10.
- Improved the distributed version of an existing formal verification product, Magellan (in C/C++/TCL), to release quality.
- Reshaped the benchmark system to tune Magellan’s orchestration: coordinating various types of formal solvers (SAT-based, BDD-based, and ATPG-based) in parallel.
- Developed mechanisms and various heuristics for Magellan to learn and manipulate orchestration on-the-fly for dealing with real world problems.

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.

Teaching Assistant, Department of Computer Science College of William & Mary, Williamsburg, VA. 09/02 ~ 12/02.
- Assisted in teaching 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.
- Lecturer of a freshman-level course (Introduction to Algebra).

Teaching Assistant, School of Art, Ohio University, Athens, OH. 09/99 ~ 03/00.
- Lecturer of a freshman-level course (Introduction to Photography).
- Assisted in teaching 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)