Chao Wang

Research staff member
NEC Labs America

Mail: 4 Independence way, Princeton, NJ 08540
Email: chaowang + at + nec-labs + dot + com
Index
I have graduated and stopped updating this page! Please visit my new home at http://www.nec-labs.com/~chaowang.

 
Research interests  
My current research is in formal specification and verification of concurrent systems. I am interested in improving the capacity of model checking techniques and promoting their applications to the design of real-world systems (hardware, software, embedded systems, etc.)
I received the 2003-2004 ACM Outstanding Ph.D. Dissertation Award in Electronic Design Automation.
Our book: Abstraction Refinement for Large Scale Model Checking , published by Springer in 2006. ISBN-10: 0-387-34155-2 (XIV, 186 p., 40 illus., Hardcover)
 
Publications (Copyrights belong to the publishers)  
( 2005 - present )
  • [BIB] [LNK] "Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra", C. Wang, Z. Yang, A. Gupta, and F. Ivancic. International Conference on Computer Aided Verification (CAV'07), Berlin, Germany. August 2007.
  • [BIB] [LNK] "Disjunctive Image Computation for Embedded Software Verification", C. Wang, Z. Yang, F. Ivancic, and A. Gupta. ACM Trans. on Design Automation of Electronic Systems, 2007 (journal version of the DATE'06 paper)
  • [LNK] [BIB] "Whodunit? Causal Analysis for Counterexamples", C. Wang, Z. Yang, F. Ivancic, A. Gupta. International Symposium on Automated Technology for Verification and Analysis (ATVA'06), pages 82-95. Springer LNCS 4218. October 2006.
  • [BIB] [LNK] "Using Statically Computed Invariants inside the Predicate Abstraction and Refinement Loop", H. Jain, F. Ivancic, A. Gupta, I. Shlyakhter, and C. Wang. International Conference on Computer Aided Verification (CAV'06), pages 137-151. Springer LNCS 4144. August 2006.
  • [BIB] [LNK] "Mixed Symbolic Representations for Model Checking Software Programs", Z. Yang, C. Wang, A. Gupta, and F. Ivancic. International Conference on Formal Methods and Models for Codesign (MEMOCODE'06), pages 17-26. Napa Valley, CA. July 2006.
  • [BIB] [LNK] "Predicate Learning and Selective Theory Deduction for a Difference Logic Solver", C. Wang, A. Gupta, and M. Ganai. ACM/IEEE Design Automation Conference (DAC'06), pages 235-240. San Francisco, CA. July 2006.
  • [BIB] [LNK] "SAT-based Verification Methods and Applications in Hardware Verification", A. Gupta, M. Ganai, and C. Wang. Formal Methods for Hardware Verification (SFM'06), pages 108-143. Springer, LNCS 3965. May 2006.
  • [BIB] [LNK] "Disjunctive Image Computation for Embedded Software Verification", C. Wang, Z. Yang, F. Ivancic, and A. Gupta. Design, Automation and Test in Europe (DATE'06), pages 1205-1210. Munich, Germany. March 2006.
  • [BIB] [LNK] "Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination," C. Wang, F. Ivancic, M. Ganai and A. Gupta. Logic for Programming Artificial Intelligence and Reasoning (LPAR'05), pages 322-336. Springer, 2005. In LNCS/LNAI 3835.
  • [BIB] [LNK] "Model Checking C Programs Using F-Soft," F. Ivancic, I. Shlyakhter, A. Gupta, M. Ganai, V. Kahlon, C. Wang and Z. Yang. IEEE International Conference on Computer Design (ICCD'05), pages 297-308. San Jose, CA. October 2005.
( 2001 - 2004 )
 
Teaching  
  • ECEN 5139, Formal verification of VLSI systems (Fall 2003)
  • CSCI 5454, Analysis and design of algorithms (Spring 2002)
 
Other links  
  • Formal methods
  • Tools and software packages
    • CUDD (BDD package) at University of Colorado - Boulder
    • VIS (Symbolic Model Checker) at University of Colorado - Boulder
    • Chaff (Propositional SAT solver) at Princeton University
    • Omega Library (Presburger Formulas Solver) at University of Maryland
  • Scientific literature search
  • Some formal verification conferences
    • CAV (Computer aided verification), submission deadline in  January 
    • CONCUR (Concurrent theory), submission deadline in April (CONCUR'05)
    • CHARME (Correct hardware design and verification methods), submission dead in April (odd years)
    • FMCAD (Formal methods in computer aided design), submission deadline in April (even years)
    • ICCAD (International conference on computer aided design), submission deadline in April
    • ICCD (International conference on computer design), submission deadline in May
    • ASP-DAC (Asia-pacific design automation conference), submission deadline July
    • LPAR (Logic for Programming Artificial Intelligence and Reasoning), submission deadline in July
    • DATE (Design and testing in Europe), submission deadline in September
    • TACAS (Tools and algorithms for the construction and analysis of system), submission deadline in October (TACAS'06)
    • DAC (Design automation conference), submission deadline in November or December
    • SPIN (SPIN workshop on model checking of software), submission deadline in December SPIN'06
    • SVV'05 (Workshop on software verification and validation), submission deadline in September
 
 
VLSI/CAD Lab | ECE Department | University of Colorado | Boulder Community

Last Revision:Sept. 2005