Min Wan (万 旻)

I graduated as PhD student in 2008 from Department of Computer Science & Engineering, University of California, Riverside.
My research interests are in the areas of formal verification, specifically in logic and stochastic model checking with decision diagrams.

Now I'm working at Yahoo! Inc in Sunnyvale, CA.

Education

• Ph.D. Computer Science 12/2008
  University of California at Riverside, Riverside, CA
  Thesis: "Decision Diagram Algorithm for Logic and Timed Verification Techniques".
  Advisor: Prof. Gianfranco Ciardo
  
  
• B.S. Computer Science 06/2003
  Zhejiang University, Hangzhou, China
  Thesis: "Open-Source Distance Learning Management System".
  Advisor: Prof. Deren Chen

Research

• Research assistant in Logic and Stochastic Verification Lab
• Advisor: Prof. Gianfranco Ciardo
  
• Activities
  • Symbolic state space generation, symbolic model checking, numerical solution of large markov models
  • Methodology: Petri nets, decision diagrams, Saturation, aggregated approximation, Jacobi and Gauss-Seidel methods
  • Software Tool development:
    • SMART2: the Symbolic Model checking Analyzer for Reliability and Timing ver.2
    • DDL: The Decision Diagram Library

Publications

• "Approximating stationary measures of structured continuous-time Markov models using matrix diagrams". with G. Ciardo, A. S. Miner and A. J. Yu. SIGMETRICS Performance Evaluation Review 35(3): 16-18 (2007)
• "Symbolic Reachability Analysis of Integer Timed Petri Nets". with G.Ciardo. SOFSEM 2009: 595-608
• "Symbolic State-Space Generation of Asynchronous Systems Using Extensible Decision Diagrams". with G.Ciardo. SOFSEM 2009: 582-594
• "P-semiflow computation using decision diagrams". with G. Ciardo, G. Mecham and E. Paviot-Adet. Petri Nets 2009: 143-162
• "Advanced Features in Smart: the Stochastic Model checker Analyzer for Reliability and Timing". with G. Ciardo and A. S. Miner. Special Issue of Elsevier Performance Evaluation Journal (2009).
• "Decision-diagram-based approximate steady-state analysis of large structured Markov models". with G. Ciardo and A. S. Miner. preparing.

Teaching

• 2003 - 2004 Teaching assistant for CS8