Education:

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

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

MFA (all but dissertation)  in   Photography  at   Ohio University, Athen, OH. Check out Ming's old photography work.

BA  in   History  at   Soochow University, Taipei, Taiwan.   June 1995.

Research Interest:

Formal verification (aka model checking), parallel computing, distributed system, and artificial intelligence.

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)

Experience:

Staff R&D Engineer, Verification Group, Synopsys, San Jose, CA. 01/16 ~ Present.
- Developed a machine-learning platform (Yoda) for EDA applications.
- Developed and patterned (US20180144071) an AI-based solution for SVA hardness estimation.
- Developed various features in Zebu emulator’s waveform expansion flow, Simzilla.

Sr. Principle Software Engineer, Digital Signoff Group, Cadence Design Systems, Inc., San Jose, CA. 03/15 ~ 12/15.
- Working on the combinational logical equivalence checking tool, Conformal. Delivered 5 enhancements in 8 months focusing on - improving compare­ points mapping via identifying RTL and gate­level netlists structural similarity
- developing instance name aliasing methodology to replace the problematic change name issues created by synthesis tools
- composing hierarchical modeling, mapping, and compare results to flat forms in order to skip model re­flattening in various applications
- implementing utilities to facilitate verification related information sharing (among tools) via JSON
- analyzing abort cones to provide synthesis guidance on synthesis datapath via SVP.

Staff R&D Engineer, Verification Group, Synopsys, Hillsboro, OR. 05/13 ~ 02/15.
Senior R&D II Engineer, Verification Group, Synopsys, Hillsboro, OR. 10/10 ~ 04/13.
- Working on 3 applications of Verification Compiler: [property|model] checking, connection checking, code coverage analysis.
- Implemented a distributed verification infrastructure for orchestrating formal engines.
- Delivered an automatic code coverage solution in VCS.
- Built a regression and benchmark system for tuning formal products.

Resigned from Synopsys and took a break from EDA industry. 05/10 ~ 09/10.
- Joined a team trying to boost an iPhone app startup.
- Shortly involved in a NASA Ames RC funded project in University of Virginia and applyied formal verification and simulation to validate flight critical systems.

Senior R&D II Engineer, Verification Group, Synopsys, Mountain View, CA. 06/09 ~ 04/10.
Senior R&D I Engineer, Verification Group, Synopsys, Mountain View, CA. 06/07 ~ 05/09.
- Implemented grid modes in Magellan which orchestrates formal engines interacting with VCS simulator.
- Built benchmarking system for orchestration tuning.

Research Intern, NEC Laboratories America, Inc., Princeton, NJ. 10/06 ~ 01/07.
- Designed a message-passing-based distributed task management library allowing researchers to parallelize verification tools with less effort. Implemented the tool in [C|MPI|Pthreads].
- 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 SMV-like symbolic model checker in [C|C++|MPICH] to validate an avionics system: 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 and distributed symbolic model checker in [C|MPI|OpenMP].
- Published 8 conference/journal papers in the parallel/distributed verification literature.
- Setup/maintain a Linux-based heterogeneous cluster providing parallel computing services via [LAM|MPI|MPICH|OpenMP|PBS].
- 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).