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)

• [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.
  

• [LNK] [BIB] "Improved Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement," C. Wang, B. Li, H. Jin, G. D. Hachtel and F. Somenzi. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (T-CAD), 25(11): 2297-2316, (2006).
• [BIB] [LNK] "Compositional SCC analysis for Language Emptiness Checking," C. Wang, R. Bloem, K. Ravi, G. D. Hachtel and F. Somenzi. Journal on Formal Methods in Systems Design, 28(1):5-36 (2006).
• [BIB] [LNK] "Abstraction Refinement in Symbolic Model Checking Using Satisfiability as the Only Decision Procedure," B. Li, C. Wang and F. Somenzi. Journal on Software Tools for Technology Transfer (STTT), 7(2):143-155 (2005).
• [BIB] [LNK] "Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking," C. Wang, G. D. Hachtel and F. Somenzi. IEEE International Conference on Computer Design (ICCD'04), San Jose, CA, October 2004.
• [BIB] [LNK] Abstraction Refinement for Large Scale Model Checking, Chao Wang, Ph.D. Thesis, University of Colorado at Boulder. June 2004. (thesis abstract)
• [BIB] [LNK] "Refining the SAT Decision Ordering for Bounded Model Checking," C. Wang, H. Jin, G. D. Hachtel and F. Somenzi. Proceedings of the ACM/IEEE 41th Design Automation Conference (DAC'04), pages 535-538. San Diego, CA, June 2004.
• [BIB] [LNK] "Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement," C. Wang, B. Li, H. Jin, G. D. Hachtel and F. Somenzi. Proceedings of International Conference on Computer Aided Design (ICCAD'03), pages 408-415. San Jose, CA, 2003.
• [BIB] [LNK] "The Compositional Far Side of Image Computation," C. Wang, G. D. Hachtel and F. Somenzi. Proceedings of International Conference on Computer Aided Design (ICCAD'03), pages 334-340. San Jose, CA, 2003.
• [BIB] [LNK] "A Satisfiability-based Approach to Abstraction Refinement in Model Checking," B. Li, C. Wang and F. Somenzi. International Workshop on Bounded Model Checking (BMC'03). Electronic Notes in Theoretical Computer Science, 89(4): (2003).
• [BIB] [LNK] "Abstraction and BDDs complement SAT-based BMC in DiVer," A. Gupta, M. Ganai, C. Wang, Z. Yang and P. Ashar. International Conference on Computer Aided Verification (CAV'03), pages 206-209. Springer-Verlag, 2003. Lecture Notes in Computer Science 2725.
• [BIB] [LNK] "Learning from BDDs in SAT-based Bounded Model Checking," A. Gupta, M. Ganai, C. Wang, Z. Yang and P. Ashar. Proceedings of the ACM/IEEE 40th Design Automation Conference (DAC'03), pages 824-829, Anaheim, CA, 2003.
• [BIB] [LNK] "Sharp Disjunctive Decomposition for Language Emptiness Checking," C. Wang, G. D. Hachtel. International Conference on Formal Methods in Computer Aided Design (FMCAD'02), pages 106-122. Springer-Verlag 2002. Lecture Notes in Computer Science 2517.
• [BIB] [LNK] "Divide and Compose: SCC Refinement for Language Emptiness," C. Wang, R. Bloem, G.D. Hachtel, K. Ravi and F. Somenzi. International Conference on Concurrency Theory (CONCUR'01), pages 456-474. Springer-Verlag, 2001. Lecture Notes in Computer Science 2154.

• ECEN 5139, Formal verification of VLSI systems (Fall 2003)
• Check the class notes of my lectures on Bounded Model Checking, and some online references.
• CSCI 5454, Analysis and design of algorithms (Spring 2002)
• I was a grader. Check the advanced algorithm courses at Professor Gabow's website.

• Formal methods
• Jonathan Bowen's  Formal Methods (a collection of links)
• Some books on formal verification
• Anecdotes: Bugs are everywhere; formal verification is practical
• 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
• DBLP at uni-trier.de
• ACM digital library
• 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