Chao Wang    

  Publications (copyrights belong to publishers)

 

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.

 

Thread-modular static analysis for relaxed memory models,

Markus Kusano and Chao Wang.

ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Paderborn, Germany. 2017.

(artifact)

 

Symbolic execution of programmable logic controller code,

Shengjian Guo, Meng Wu and Chao Wang.

ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Paderborn, Germany. 2017.

 

DESCRY: Reproducing system-level concurrency failures,

Tingting Yu, Tarannum Zaman and Chao Wang.

ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Paderborn, Germany. 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)

 

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, 2017. (extension of ICST15 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. 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 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 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 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)

(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.