|
Publications (copyrights belong to the publishers)
|
|
|
[
PDF |
BIB ]
|
Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions,
C. Wang, Y. Yang, A. Gupta, and G. Gopalakrishnan.
ATVA 2008.
|
|
[
PDF |
BIB]
|
Modular Verification of Web Services Using Efficient Symbolic Encoding and Summarization,
F. Yu, C. Wang, A. Gupta, and T. Bultan.
SIGSOFT/FSE 2008.
|
|
[
PDF
|
BIB
]
|
Peephole Partial Order Reduction, C. Wang, Z. Yang, V. Kahlon, and A. Gupta.
International Conference on Tools and Algorithms for the Construction and Analysis of Systems
(TACAS’08).
|
|
[
PDF
| BIB
]
|
Towards Precise and Scalable Verification of Embedded Software, M. Ganai, A. Gupta, F. Ivancic, V. Kahlon, W. Li,
N. Papakonstantinou, S. Sankaranarayanan, and C. Wang.
Design and Verification Conference (DVCon'08).
|
|
|
|
|
[
PDF
|
BIB
]
|
Induction in CEGAR for Detecting Counterexamples, C. Wang, A.
Gupta, and F. Ivancic. In International Conference on Formal Methods
in Computer Aided Design (FMCAD'07).
|
|
[
PDF
|
BIB
]
|
Hybrid CEGAR: Combining Variable Hiding and Predicate Abstraction,
C. Wang, H. Kim, and A. Gupta. In International Conference on Computer
Aided Design (ICCAD'07).
|
|
[
PDF
|
BIB
]
|
Using Counterexamples for Improving the Precision of Reachability
Computation with Polyhedra, C. Wang, Z.
Yang, A. Gupta, and F. Ivancic. In International Conference on
Computer Aided Verification (CAV'07).
In the original version
Algorithm 1 was not
presented correctly. We found and fixed this problem before the
CAV'07 conference presentation.
(Presentation Slides)
|
|
|
Disjunctive Image Computation for Software Verification, C.
Wang, Z. Yang, F. Ivancic, and A. Gupta. In ACM Trans. on Design
Automation of Electronic Systems. 12(2):10, April 2007
|
|
|
|
|
[LNK | BIB]
|
Whodunit? Causal Analysis for Counterexamples, C. Wang, Z.
Yang, F. Ivancic, and A. Gupta. International Symposium on Automated
Technology for Verification and Analysis (ATVA’06).
|
|
[LNK | BIB]
|
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).
|
|
[LNK | BIB]
|
Predicate Learning and Selective Theory Deduction for a Difference
Logic Solver, C. Wang, A. Gupta, and M. Ganai. In ACM/IEEE
Design Automation Conference (DAC'2006).
|
|
[LNK | BIB]
|
Disjunctive Image Computation for Embedded Software Verification, C.
Wang, Z. Yang, F. Ivancic, and A. Gupta. In Design, Automation
and Test in Europe (DATE'2006).
|
|
[LNK
| BIB]
|
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’2006).
|
|
[LNK | BIB]
|
SAT-based Verification Methods and Applications in Hardware
Verification, A. Gupta, M. Ganai, and C. Wang. Formal Methods for
Hardware Verification (SFM’06). May 2006.
|
|
|
Improved Ariadne's Bundle by Following
Multiple Threads in Abstraction Refinement, C.
Wang, B. Li, H. Jin, G. D. Hachtel and F. Somenzi. In IEEE Trans. on Computer-Aided
Design (T-CAD),25(11):2297-2316, (2006)
|
|
|
Compositional SCC analysis for Language Emptiness Checking, C.
Wang, R. Bloem, K. Ravi, G. D. Hachtel and F. Somenzi.
In Journal on Formal Methods in Systems Design. 28(1):5-26
(2006)
|
|
|
|
|
[LNK | BIB]
|
Deciding Separation Logic Formulae by SAT and Incremental Negative
Cycle Elimination, C. Wang, F.
Ivancic, M. Ganai and A. Gupta. In Logic for Programming
Artificial Intelligence and Reasoning (LPAR'2005).
|
|
[LNK | BIB]
|
Model Checking C Programs Using F-Soft,
F. Ivancic, I. Shlyakhter, A. Gupta, M.
Ganai, V. Kahlon, C. Wang and Z. Yang. In IEEE International
Conference on Computer Design (ICCD'2005).
|
|
|
Abstraction Refinement in Symbolic Model Checking Using
Satisfiability as the Only Decision Procedure, B. Li, C. Wang
and F. Somenzi. In Journal on Software
Tools for Technology Transfer (STTT), 7(2):143-155 (2005).
|
|
|
|
|
[PDF | BIB]
|
Fine-Grain Abstraction and Sequential Don't Cares for Large Scale
Model Checking, C. Wang, G. D. Hachtel and F. Somenzi. In IEEE International Conference on
Computer Design (ICCD'2004).
|
|
[LNK | BIB]
|
Abstraction Refinement for Large Scale Model Checking, Chao
Wang, Ph.D. Dissertation, University
of Colorado at Boulder.
June 2004. (Springer has published it as a book.)
|
|
[PDF | BIB ]
|
Refining the SAT Decision Ordering for Bounded Model Checking, C. Wang, H. Jin, G. D. Hachtel
and F. Somenzi. In ACM/IEEE 41th Design Automation Conference (DAC'2004),
pages 535-538.
|
|
|
|
|
[PDF
| BIB ]
|
Improving Ariadne's Bundle by Following
Multiple Threads in Abstraction Refinement, C. Wang, B. Li, H. Jin,
G. D. Hachtel and F. Somenzi.
In International Conference on Computer Aided Design (ICCAD'2003), pages
408-415.
|
|
[PDF
| BIB ]
|
The Compositional Far Side of Image Computation, C. Wang, G. D. Hachtel
and F. Somenzi. In International
Conference on Computer Aided Design (ICCAD'2003), pages 334-340.
|
|
[ PDF
| BIB ]
|
A Satisfiability-based Approach to Abstraction Refinement in Model
Checking, B. Li, C. Wang and F. Somenzi. International Workshop on Bounded Model
Checking (BMC'2003). ENTCS 89(4): (2003).
|
|
[ PDF
| BIB ]
|
Abstraction and BDDs complement SAT-based BMC in DiVer, A. Gupta,
M. Ganai, C. Wang, Z. Yang and P. Ashar.
In International Conference on Computer Aided Verification (CAV'2003),
pages 206-209.
|
|
[ PDF
| BIB ]
|
Learning from BDDs in SAT-based Bounded Model Checking, A.
Gupta, M. Ganai, C. Wang, Z. Yang and P. Ashar.
In ACM/IEEE 40th Design Automation Conference (DAC'2003), pages
824-829.
|
|
|
|
|
[ PDF
| BIB ]
|
Sharp Disjunctive Decomposition for Language Emptiness Checking,
C. Wang, G. D. Hachtel. In International
Conference on Formal Methods in Computer Aided Design (FMCAD'02),
pages 106-122.
|
|
[ PDF
| BIB ]
|
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.
|
|
|
|
|
|