Publications

2024

Constraint Based Program Repair for Persistent Memory Bugs, Zunchen Huang and Chao Wang. International Conference on Software Engineering (ICSE), 2024.

2023

Synthesizing MILP Constraints for Efficient and Robust Optimization, Jingbo Wang, Aarti Gupta, and Chao Wang. ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), 2023.
(ACM SIGPLAN Distinguished Paper Award)

Certifying the Fairness of KNN in the Presence of Dataset Bias, Yannan Li, Jingbo Wang, and Chao Wang. International Conference on Computer Aided Verification (CAV), 2023.

Systematic Testing of the Data-Poisoning Robustness of KNN, Yannan Li, Jingbo Wang, and Chao Wang. ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2023.

Constraint Based Compiler Optimization for Energy Harvesting Applications , Yannan Li and Chao Wang. European Conference on Object-Oriented Programming (ECOOP), 2023.

2022

Learning to Synthesize Relational Invariants, Jingbo Wang and Chao Wang. International Conference on Automated Software Engineering (ASE), 2022.

Proving Robustness of KNNs Against Adversarial Data Poisoning, Yannan Li, Jingbo Wang and Chao Wang. International Conference on Formal Methods for Computer Aided Design (FMCAD), 2022.

Synthesizing Fair Decision Trees via Iterative Constraint Solving, Jingbo Wang, Yannan Li and Chao Wang. International Conference on Computer Aided Verification (CAV), 2022. (artifact)

Example Guided Synthesis of Linear Approximations for Neural Network Verification, Brandon Paulsen and Chao Wang. International Conference on Computer Aided Verification (CAV), 2022.

LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions, Brandon Paulsen and Chao Wang. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2022. (artifact)

Symbolic Predictive Cache Analysis for Out-of-Order Execution, Zunchen Huang and Chao Wang. International Conference on Fundamental Approaches to Software Engineering (FASE), 2022.

2021

Data-Driven Synthesis of a Provably Sound Side Channel Analysis, Jingbo Wang, Chungha Sung, Mukund Raghothaman, and Chao Wang. International Conference on Software Engineering (ICSE), 2021.

DiffRNN: Differential Verification of Recurrent Neural Networks, Sara Mohammadinejad, Brandon Paulsen, Jyotirmoy V. Deshmukh and Chao Wang. International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2021.

2020

NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation, Brandon Paulsen, Jingbo Wang, Jiawei Wang, and Chao Wang. IEEE/ACM International Conference on Automated Software Engineering (ASE), 2020. (artifact)

ReluDiff: Differential Verification of Deep Neural Networks, Brandon Paulsen, Jingbo Wang, and Chao Wang. International Conference on Software Engineering (ICSE), 2020.
(artifact)

Towards Understanding and Fixing Upstream Merge Induced Conflicts in Divergent Forks: An industrial Case Study, Chungha Sung, Shuvendu Lahiri, Mike Kaufman, Pallavi Choudhury, and Chao Wang. International Conference on Software Engineering (ICSE SEIP), 2020.

ConTesa: Directed Test Suite Augmentation for Concurrent Software,
Tingting Yu, Zunchen Huang, and Chao Wang.
IEEE Transactions on Software Engineering (TSE), 2020
(journal-first paper).

2019

Debreach: Mitigating compression side channels via static analysis and transformation, Brandon Paulsen, Chungha Sung, Peter Peterson, and Chao Wang. IEEE/ACM International Conference on Automated Software Engineering (ASE), 2019.
(artifact)

Shield synthesis for real: Enforcing safety in cyber-physical systems, Meng Wu, Jingbo Wang, Jyotirmoy Deshmukh, and Chao Wang. International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2019.

Mitigating power side channels during compilation, Jingbo Wang, Chungha Sung, and Chao Wang. ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2019. (artifact)

Abstract interpretation under speculative execution,
Meng Wu and Chao Wang.
ACM SIGPLAN Symposium on Programming Language Design and Implementation (PLDI), 2019.
(slides, artifact)

Verifying and quantifying side-channel resistance of masked software implementation,
Pengfei Gao, Jun Zhang, Fu Song, and Chao Wang.
ACM Transactions on Software Engineering and Methodology (TOSEM), 2019.

2018

Adversarial symbolic execution for detecting concurrency-related cache timing leaks,
Shengjian Guo, Meng Wu, and Chao Wang.
ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), Florida, USA. 2018.
(artifact)
(ACM SIGSOFT Distinguished Paper Award)

Datalog-based scalable semantic diffing of concurrent programs,
Chungha Sung, Shuvendu Lahiri, Constantin Enea and Chao Wang.
IEEE/ACM International Conference on Automated Software Engineering (ASE), Montpellier, France. 2018.
(artifact)

CANAL: A cache timing analysis framework via LLVM transformation,
Chungha Sung, Brandon Paulsen and Chao Wang.
IEEE/ACM International Conference on Automated Software Engineering (ASE) Tool Demo Track, Montpellier, France. 2018.
(artifactvideo)

Eliminating timing side-channel leaks using program repair,
Meng Wu, Shengjian Guo, Patrick Schaumont, and Chao Wang.
ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), Amsterdam, The Netherlands. 2018.
(artifact)

SCInfer: Refinement-based verification of software countermeasures against side-channel attacks,
Jun Zhang, Pengfei Gao, Fu Song, and Chao Wang.
International Conference on Computer Aided Verification (CAV), Oxford, UK. 2018.
(artifact)

Eliminating path redundancy via postconditioned symbolic execution,
Qiuping Yi, Zijiang Yang, Shengjian Guo, Chao Wang, Jian Liu, and Chen Zhao.
IEEE Transactions on Software Engineering, 2018. (extension of our ICST15 paper)

2017

Thread-modular static analysis for relaxed memory models,
Markus Kusano and Chao Wang.
ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), Paderborn, Germany. 2017.
(artifact)


Symbolic execution of programmable logic controller code
,
Shengjian Guo, Meng Wu and Chao Wang.
ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), Paderborn, Germany. 2017.

DESCRY: Reproducing system-level concurrency failures,
Tingting Yu, Tarannum Zaman and Chao Wang.
ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), Paderborn, Germany. 2017.

Modular verification of interrupt-driven software,
Chungha Sung, Markus Kusano and Chao Wang.
IEEE/ACM International Conference on Automated Software Engineering (ASE), Illinois, USA. 2017.
(artifact)

Systematic reduction of GUI test sequences,
Lin Cheng, Zijiang Yang and Chao Wang.
IEEE/ACM International Conference on Automated Software Engineering (ASE), Illinois, USA. 2017.

Shield synthesis,
Bettina Konighofer, Mohammed Alshiekh, Roderick Bloem, Laura Humphrey, Robert Konighofer, Ufuk Topcu, and Chao Wang.
International Journal on Formal Methods in Systems Design, 2017

RClassify: Classifying race conditions in web applications via deterministic replay,
Lu Zhang and Chao Wang.
IEEE/ACM International Conference on Software Engineering (ICSE), Buenos Aires, Argentina. 2017.

Security by Compilation: An automated approach to comprehensive side-channel resistance,
Chao Wang and Patrick Schaumont.
ACM SIGLOG News, Vol. 4, No. 2, April 2017.

Safety Guard: Runtime enforcement for safety-critical cyber-physical systems,
Meng Wu, Haibo Zeng, Chao Wang and Huafeng Yu.
ACM/IEEE Design Automation Conference, June 2017. (invited paper)

2016

Flow-sensitive composition of thread-modular abstract interpretation,
Markus Kusano and Chao Wang.
ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Seattle, WA, USA. 2016.
(artifact)

Static DOM event dependency analysis for testing web applications,
Chungha Sung, Markus Kusano, Nishant Sinha and Chao Wang.
ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Seattle, WA, USA. 2016.
(artifact)

Conc-iSE: Incremental Symbolic Execution of Concurrent Software,
Shengjian Guo, Markus Kusano and Chao Wang.
IEEE/ACM International Conference on Automated Software Engineering (ASE), Singapore. 2016.


GUICat: GUI Testing as a Service
,
Lin Cheng, Jialiang Chang, Zijiang Yang and Chao Wang.
IEEE/ACM International Conference on Automated Software Engineering (ASE), Singapore. 2016.

Synthesis of fault-attack countermeasures for cryptographic circuits,
Hassan Eldib, Meng Wu, and Chao Wang.
International Conference on Computer Aided Verification (CAV), Toronto, Canada. 2016. (artifact)

Synthesizing runtime enforcer of safety properties under burst error,
Meng Wu, Haibo Zeng, and Chao Wang.
NASA Formal Methods Symposium, Minneapolis, MN, USA. 2016.
(artifact)

Verifying a quantitative relaxation of linearizability via refinement,
Kiran Adhikari, James Street, Chao Wang, Yang Liu and Shaojie Zhang.
Journal on Software Tools for Technology Transfer, 2016. (extension of SPIN13 paper)

Abstraction and mining of traces to explain concurrency bugs,
Mitra Befrouei, Chao Wang, and Georg Weissenbacher.
International Journal on Formal Methods in System Design, 2016. (extension of RV14 paper)

2015

Assertion guided symbolic execution of multithreaded programs,
Shengjian Guo, Markus Kusano, Chao Wang, Zijiang Yang, and Aarti Gupta.
ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Bergamo, Italy. 2015.

ConcBugAssist: Constraint solving for diagnosis and repair of concurrency bugs,
Sepideh Khoshnood, Markus Kusano, and Chao Wang.
International Symposium on Software Testing and Analysis (ISSTA), Baltimore, Maryland, USA. 2015.
(artifact)

Dynamic partial order reduction for relaxed memory models,
Naling Zhang, Markus Kusano, and Chao Wang.
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Portland, Oregon, USA. 2015.
(artifact)

Dynamic generation of likely invariants for multithreaded programs,
Markus Kusano, Arijit Chattopadhyay, and Chao Wang.
IEEE/ACM International Conference on Software Engineering (ICSE), Florence, Italy. 2015.
(artifact)

A synergistic analysis method for explaining failed regression tests,
Qiuping Yi, Zijiang Yang, Jian Liu, Chen Zhao, and Chao Wang.
IEEE/ACM International Conference on Software Engineering (ICSE), Florence, Italy. 2015.

Post conditioned symbolic execution,
Qiuping Yi, Zijiang Yang, Shengjian Guo, Chao Wang, Jian Liu, and Chen Zhao.
IEEE International Conference on Software Testing, Verification and Validation (ICST), Graz, Austria. 2015.

Shield synthesis: Runtime enforcement for reactive systems,
Roderick Bloem, Bettina Konighofer, Robert Konighofer, and Chao Wang.
International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), London, UK. 2015.

Explaining software failures by cascade fault localization,
Qiuping Yi, Zijiang Yang, Jian Liu, Chen Zhao, and Chao Wang.
ACM Transactions on Design Automation of Electronic Systems, 2015.

Round-Up: Runtime verification of quasi linearizability for concurrent data structures,
Lu Zhang, Arijit Chattopadhyay, and Chao Wang.
IEEE Transactions on Software Engineering (TSE). 2015. (extension of ASE13 paper)
(artifact)

Quantitative masking strength: Quantifying the power side-channel resistance of software code,
Hassan Eldib, Chao Wang, Mostafa Taha, and Patrick Schaumont.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2015. (extension of our DAC14 paper)

2014

Formal verification of software countermeasures against side-channel attacks,
Hassan Eldib, Chao Wang, and Patrick Schaumont.
ACM Transactions on Software Engineering and Methodology, 24(2), 2014. (extension of our TACAS14 paper)

An SMT based method for optimizing arithmetic computations in embedded software code,
Hassan Eldib and Chao Wang.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 33(11):1611-1622, 2014. (extension of our FMCAD13 paper)

Assertion guided abstraction: a cooperative optimization for dynamic partial order reduction,
Markus Kusano and Chao Wang.
IEEE/ACM International Conference on Automated Software Engineering (ASE), pp.175-186. 2014.

Abstraction and mining of traces to explain concurrency bugs,
Mitra Befrouei, Chao Wang, and Georg Weissenbacher.
International Conference on Runtime Verification (RV), pp. 162-177. 2014.

Synthesis of masking countermeasures against side channel attacks,
Hassan Eldib and Chao Wang.
International Conference on Computer Aided Verification (CAV), pp. 114-130. 2014.
(artifact)

Runtime prevention of concurrency related type-state violations in multithreaded applications,
Lu Zhang and Chao Wang.
International Symposium on Software Testing and Analysis (ISSTA), pp. 1-12. 2014.

QMS: Evaluating the side-channel resistance of masked software from source code,
Hassan Eldib, Chao Wang, Mostafa Taha, and Patrick Schaumont.
ACM/IEEE Design Automation Conference (DAC), pp. 1-6. 2014.

SMT-based verification of software countermeasures against side-channel attacks,
Hassan Eldib, Chao Wang, and Patrick Schaumont.
International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 62-77. 2014.

Precisely deciding control state reachability in concurrent traces with limited observability,
Chao Wang and Kevin Hoang.
International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 376-394. 2014.

2013

Round-Up: Runtime checking quasi linearizability of concurrent data structures,
Lu Zhang, Arijit Chattopadhyay, and Chao Wang.
IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 4-14. 2013.
(artifact)

CCmutator: A mutation generator for concurrency constructs in multithreaded C/C++ applications,
Markus Kusano and Chao Wang.
IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 722-725. 2013.

An SMT based method for optimizing arithmetic computations in embedded software code,
Hassan Eldib and Chao Wang.
International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 129-136. 2013.
(artifact)
(FMCAD Best Paper Award)

Verifying a quantitative relaxation of linearizability via refinement,
Kiran Adhikari, James Street, Chao Wang, Yang Liu and Shaojie Zhang.
International SPIN Symposium on Model Checking of Software (SPIN), pp. 24-42. 2013.

Dynamic analysis and debugging of binary code for security applications,
Lixin Li and Chao Wang.
International Conference on Runtime Verification (RV), pp. 403-423. 2013.

A novel statistical and circuit-based technique for counterfeit detection in existing ICs,
R. Moudgil, D. Ganta, L. Nazhandali, M. Hsiao, C. Wang and S. Hall.
ACM Great Lakes Symposium on VLSI, pp.1-6. 2013.

Interlocking obfuscation for anti-tamper hardware,
Desai, M. Hsiao, C. Wang, L. Nazhandali, and S. Hall.
The Eighth Annual Cyber Security and Information Intelligence Research Workshop. 2013.

Anti-counterfeit integrated circuits using fuse and tamper-resistant time-stamp circuitry,
Desai, D. Ganta, M. Hsiao, L. Nazhandali, C. Wang and S. Hall.
IEEE International Conference on Technologies for Homeland Security, pp. 480-485. 2013.

2012

Lock removal for concurrent trace programs,
V. Kahlon and C. Wang.
International Conference on Computer Aided Verification (CAV), pp. 227-243. LNCS 7358. Springer, 2012.

2011

On interference abstraction,
N. Sinha and C. Wang.
ACM Symposium on Principles of Programming Languages (POPL), pp. 423-434. Austin, TX. January 2011.

Coverage guided systematic concurrency testing,
Chao Wang, M. Said and A. Gupta.
IEEE/ACM International Conference on Software Engineering (ICSE). Honolulu, Hawaii. May 2011.

Predicting concurrency failures in the generalized execution traces of x86 executables
,
C. Wang and M. Ganai.
International Conference on Runtime Verification (RV). San Francisco, CA. 2011.

Generating data race witnesses by an SMT-based analysis,
M. Said, C. Wang, K. Sakallah and Z. Yang.
NASA Formal Methods Symposium. Pasadena, CA. April 2011.

BEST: A symbolic testing tool for predicting multi-threaded program failures,
M. Ganai, N. Arora, C. Wang, A. Gupta and G. Balakrishnan.
IEEE/ACM International Conference on Automated Software Engineering (ASE). 2011

Predictive Analysis for Detecting Serializability Violations through Trace Segmentation,
A. Sinha, S. Malik, C. Wang and A. Gupta.
ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE). Cambridge, UK. July 2011.

Predicting serializability violations: SMT-based search vs. DPOR-based search,
A. Sinha, S. Malik, C. Wang and A. Gupta.
Haifa Verification Conference. 2011.

2010

Staged concurrent program analysis,
N. Sinha and C. Wang.
ACM International Symposium on Foundations of Software Engineering (FSE), pp. 47-56. Santa Fe, NM. 2010.
(ACM SIGSOFT Distinguished Paper Award)

Universal causality graphs: a precise happens-before model for detecting bugs in concurrent programs,
V. Kahlon and C. Wang.
International Conference on Computer Aided Verification (CAV), pp. 434-449. Springer 2010. LNCS 6174.

CONTESSA: concurrency testing augmented with symbolic analysis,
S. Kundu, M. Ganai and C. Wang.
International Conference on Computer Aided Verification (CAV), pp. 127-131. Springer 2010. LNCS 6174.

Trace-based symbolic analysis for atomicity violations,
C. Wang, R. Limaye, M. Ganai, and A. Gupta.
International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pages 328-342. Springer 2010. LNCS 6015.

Interval analysis for concurrent trace programs using transaction sequence graphs,
M. Ganai and C. Wang.
International Conference on Runtime Verification (RV), pages 253-269. Springer, 2010. LNCS 6418.

Efficient state space exploration: interleaving stateless and state-based model checking,
M. Ganai, C. Wang and W. Li.
International Conference on Computer-Aided Design (ICCAD), pages 786-793. San Jose, CA. 2010.

Scalable and precise program analysis at NEC,
G. Balakrishnan, M. Ganai, A. Gupta, F. Ivancic, V. Kahlon, W. Li, N. Maeda, N. Papakonstantinou, S. Sankaranarayanan, N. Sinha, and C. Wang.
International Conference on Formal Methods for Computer Aided Design (FMCAD). 2010.

2009

Symbolic pruning of concurrent program executions,
C. Wang, S. Chaudhuri, A. Gupta, and Y. Yang.
ACM International Symposium on Foundations of Software Engineering (FSE), pages 23-32. August 2009. Amsterdam, The Netherlands.

Monotonic partial order reduction: an optimal symbolic POR technique,
V. Kahlon, C. Wang, and A. Gupta.
International Conference on Computer Aided Verification (CAV), pages 398-413. Springer 2009. Lecture Notes in Computer Science 5643.

Symbolic predictive analysis of concurrent programs,
C. Wang, S. Kundu, M. Ganai, and A. Gupta.
International Symposium on Formal Methods (FM), pages 256-272. Springer 2009. Lecture Notes in Computer Science 5850.

Automatic discovery of transition symmetry in multithreaded programs using dynamic analysis,
Y. Yang, X. Chen, G. Gopalakrishnan, and C. Wang.
International SPIN Workshop on Model Checking Software, pages 279-295. Springer 2009. LNCS 5578.

Model checking sequential software programs via mixed symbolic analysis,
Z. Yang, C. Wang, A. Gupta, and F. Ivancic.
ACM Transactions on Design Automation of Electronic Systems, 13(1): (2009).

2008

Peephole partial order reduction,
C. Wang, Z. Yang, V. Kahlon, and A. Gupta.
International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pages 382-396. Springer 2008. LNCS 4963.

Dynamic model checking with property driven pruning to detect race conditions,
C. Wang, Y. Yang, A. Gupta, and G. Gopalakrishnan.
Intl. Symp. Automated Technology for Verification and Analysis (ATVA), pages 126-140. Springer 2008. LNCS 5311.

Modular verification of web services using efficient symbolic encoding and summarization,
F. Yu, C. Wang, A. Gupta, and T. Bultan.
ACM International Symposium on Foundations of Software Engineering (FSE), pages 192-202. ACM 2008.

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), 2008.

2007

Disjunctive image computation for embedded software verification,
C. Wang, Z. Yang, F. Ivancic, and A. Gupta.
ACM Trans. Design Autom. Electr. Syst. 12(2): (2007).
(Best Paper of the Year Award)

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), pages 352-365. Springer 2007. LNCS 4590.

Hybrid CEGAR: combining variable hiding and predicate abstraction,
C. Wang, H. Kim, and A. Gupta.
IEEE International Conference on Computer-Aided Design (ICCAD), pages 310-317. San Jose, CA. 2007.

Induction in CEGAR for detecting counterexamples,
C. Wang, A. Gupta, and F. Ivancic.
International Conference on Formal Methods in Computer Aided Design (FMCAD), pages 77-84. IEEE 2007. Austin, TX.

2006

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), pages 137-151. Springer LNCS 4144. August 2006.

Whodunit? Causal analysis for counterexamples,
C. Wang, Z. Yang, F. Ivancic, A. Gupta.
International Symposium on Automated Technology for Verification and Analysis (ATVA), pages 82-95. Springer LNCS 4218. October 2006.

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), pages 17-26. Napa Valley, CA. July 2006.

Predicate learning and selective theory deduction for a difference logic solver,
C. Wang, A. Gupta, and M. Ganai.
ACM/IEEE Design Automation Conference (DAC), pages 235-240. San Francisco, CA. July 2006.

Disjunctive image computation for embedded software verification,
C. Wang, Z. Yang, F. Ivancic, and A. Gupta.
Design, Automation and Test in Europe (DATE), pages 1205-1210. Munich, Germany. March 2006.

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, 25(11): 2297-2316, (2006).

Compositional SCC analysis for language emptiness checking,
C. Wang, R. Bloem, K. Ravi, G. D. Hachtel and F. Somenzi.
International Journal on Formal Methods in System Design, 28(1):5-36 (2006).

SAT-based verification methods and applications in hardware verification,
A. Gupta, M. Ganai, and C. Wang.
Formal Methods for Hardware Verification, pages 108-143. Springer, LNCS 3965. May 2006.

2005

Deciding difference 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), pages 322-336. Springer, 2005. In LNCS/LNAI 3835.

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), pages 297-308. San Jose, CA. October 2005.

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, 7(2):143-155 (2005).

2004

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), San Jose, CA, October 2004.

Refining the SAT decision ordering for bounded model checking,
C. Wang, H. Jin, G. D. Hachtel and F. Somenzi.
ACM/IEEE 41th Design Automation Conference (DAC), pages 535-538. San Diego, CA, June 2004.

2003

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), pages 408-415. San Jose, CA, 2003.

The compositional far side of image computation,
C. Wang, G. D. Hachtel and F. Somenzi.
Proceedings of International Conference on Computer Aided Design (ICCAD), pages 334-340. San Jose, CA, 2003.

A satisfiability-based approach to abstraction refinement in model checking,
B. Li, C. Wang and F. Somenzi.
International Workshop on Bounded Model Checking. Electronic Notes in Theoretical Computer Science, 89(4):(2003).

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), pages 206-209. Springer-Verlag, 2003. Lecture Notes in Computer Science 2725.

Learning from BDDs in SAT-based bounded model checking,
A. Gupta, M. Ganai, C. Wang, Z. Yang and P. Ashar.
ACM/IEEE 40th Design Automation Conference (DAC), pages 824-829, Anaheim, CA, 2003.

2002

Sharp disjunctive decomposition for language emptiness checking,
C. Wang, G. D. Hachtel.
International Conference on Formal Methods in Computer Aided Design (FMCAD), pages 106-122. Springer-Verlag 2002. Lecture Notes in Computer Science 2517.

2001

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), pages 456-474. Springer-Verlag, 2001. Lecture Notes in Computer Science 2154.

(Ph.D. Dissertation, 2004)

Abstraction refinement for large scale model checking,
University of Colorado at Boulder, June 2004.
(ACM Outstanding Dissertation Award in Electronic Design Automation)
Springer published it as a book.