Wonhong Nam

Research Area

• Formal Methods, Formal Verification, (Symbolic) Model Checking
• Interface Synthesis
• Automated Planning
• Analysis for Web Services

Office

• 313B IST Building
  College of Information Sciences and Technology,
  Pennsylvania State University,
  University Park, PA, 16802

Ph.D. Dissertation

• Synthesis and Compositional Verification Using Language Learning [PDF], University of Pennsylvania, 2007.

Publications

• Type-Aware Web Service Composition Using Boolean Satisfiability Solver.
  with Hyunyoung Kil and Dongwon Lee.
  IEEE Joint Conference on E-Commerce Technology (CEC'08) and Enterprise Computing, E-Commerce and E-Services (EEE'08).
• Automatic Symbolic Compositional Verification by Learning Assumptions.
  with Rajeev Alur and P. Madhusudan.
  Formal Methods in System Design, Vol. 32(3):207-234, 2008.
• Learning Plans for Safety and Reachability Goals with Partial Observability.
  with Rajeev Alur.
  Tech Report MS-CIS-07-16, University of Pennsylvania, 2007.
• Learning-based Symbolic Assume-guarantee Reasoning with Automatic Decomposition.
  with Rajeev Alur.
  The 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), Beijing, China, 2006.
  Lecture Notes in Computer Science (LNCS) 4218, pp.170-185.
• Formal Verification of Industrial Benchmarks Using Flexible Engine Architecture.
  with X. du, A. Kuehlmann, R.P. Kurshan and K.L. McMillan.
  Cadence Technical Conference, 2006. The best paper award.
• Symbolic Compositional Verification by Learning Assumptions. [PDF]
  with Rajeev Alur and P. Madhusudan.
  The 17th International Conference on Computer Aided Verification (CAV'05), Edinburgh, Scotland, UK, 2005.
  Lecture Notes in Computer Science (LNCS) 3576, pp.548-562.
• Synthesis of Interface Specifications for Java Classes. [PDF]
  with Rajeev Alur, Cerny Pavol and P. Madhusudan.
  The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05), Long Beach, California, USA, pp.98-109, 2005.
• Symbolic Computational Techniques for Solving Games.
  with Rajeev Alur and P. Madhusudan.
  International Journal on Software Tools for Technology Transfer (STTT), Vol.7(2), pp.118-128, 2005.
  - Preliminary version [PDF] : The 1st International Workshop on Bounded Model Checking (BMC'03), Boulder, Colorado, USA, 2003.
  Electronic Notes in Theoretical Computer Science (ENTCS), Vol 89(4), pp.578-592.
• Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System.
  with R. Alur, D. Arney, E. L. Gunter, I. Lee et al.
  International Journal in Software Tools for Technology Transfer (STTT), Vol.5(4), pp.308-319, 2004.