Sr. Principle Software Engineer
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.
Formal verification (aka model checking), parallel computing, distributed system, and artificial intelligence.
Sr. Principle Software Engineer,
Digital Signoff Group,
Cadence Design Systems, Inc.,
San Jose, CA. 03/15 ~ Present.
- Conform's logical equivalence checker.
Staff R&D Engineer,
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,
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.
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.
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.
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.
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.
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).
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).
Department of Mathematics,
Ohio University, Athens, OH. 09/00 ~ 06/01.
- Lecturer of a freshman-level course (Introduction to Algebra).
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).
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)