Ming-Ying Chung
|
|
Sr. R&D Engineer |
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)
Multimedia: