Divide and Compose: SCC Refinement for Language Emptiness. - Chao Wang 001; Roderick Bloem; Gary D. Hachtel; Kavita Ravi; Fabio Somenzi (CONCUR, 2001)

Sharp Disjunctive Decomposition for Language Emptiness Checking. - Chao Wang 001; Gary D. Hachtel (FMCAD, 2002)

Abstraction and BDDs Complement SAT-Based BMC in DiVer. - Aarti Gupta; Malay K. Ganai; Chao Wang 001; Zijiang Yang 006; Pranav Ashar (CAV, 2003)

Learning from BDDs in SAT-based bounded model checking. - Aarti Gupta; Malay K. Ganai; Chao Wang 001; Zijiang Yang 006; Pranav Ashar (DAC, 2003)

The Compositional Far Side of Image Computation. - Chao Wang 001; Gary D. Hachtel; Fabio Somenzi (ICCAD, 2003)

Improving Ariadneýs Bundle by Following Multiple Threads in Abstraction Refinement. - Chao Wang 001; Bing Li; HoonSang Jin; Gary D. Hachtel; Fabio Somenzi (ICCAD, 2003)

A satisfiability-based approach to abstraction refinement in model checking. - Bing Li; Chao Wang 001; Fabio Somenzi (BMC@CAV, 2003)

Refining the SAT decision ordering for bounded model checking. - Chao Wang 001; HoonSang Jin; Gary D. Hachtel; Fabio Somenzi (DAC, 2004)

Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking. - Chao Wang 001; Gary D. Hachtel; Fabio Somenzi (ICCD, 2004)

Model Checking C Programs Using F-SOFT. - Franjo Ivancic; Ilya Shlyakhter; Aarti Gupta; Malay K. Ganai; Vineet Kahlon; Chao Wang 001; Zijiang Yang 006 (ICCD, 2005)

Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. - Chao Wang 001; Franjo Ivancic; Malay K. Ganai; Aarti Gupta (LPAR, 2005)

Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. - Bing Li; Chao Wang 001; Fabio Somenzi (Int. J. Softw. Tools Technol. Transf., 2005)

Whodunit? Causal Analysis for Counterexamples. - Chao Wang 001; Zijiang Yang 006; Franjo Ivancic; Aarti Gupta (ATVA, 2006)

Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. - Himanshu Jain; Franjo Ivancic; Aarti Gupta; Ilya Shlyakhter; Chao Wang 001 (CAV, 2006)

Predicate learning and selective theory deduction for a difference logic solver. - Chao Wang 001; Aarti Gupta; Malay K. Ganai (DAC, 2006)

Disjunctive image computation for embedded software verification. - Chao Wang 001; Zijiang Yang 006; Franjo Ivancic; Aarti Gupta (DATE, 2006)

Mixed symbolic representations for model checking software programs. - Zijiang Yang 006; Chao Wang 001; Aarti Gupta; Franjo Ivancic (MEMOCODE, 2006)

SAT-Based Verification Methods and Applications in Hardware Verification. - Aarti Gupta; Malay K. Ganai; Chao Wang 001 (SFM, 2006)

Compositional SCC Analysis for Language Emptiness. - Chao Wang 001; Roderick Bloem; Gary D. Hachtel; Kavita Ravi; Fabio Somenzi (Formal Methods Syst. Des., 2006)

Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement. - Chao Wang 001; Bing Li; HoonSang Jin; Gary D. Hachtel; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2006)

Abstraction Refinement for Large Scale Model Checking - Chao Wang 001; Gary D. Hachtel; Fabio Somenzi (Springer, 2006)

Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. - Chao Wang 001; Zijiang Yang 006; Aarti Gupta; Franjo Ivancic (CAV, 2007)

Induction in CEGAR for Detecting Counterexamples. - Chao Wang 001; Aarti Gupta; Franjo Ivancic (FMCAD, 2007)

Hybrid CEGAR: combining variable hiding and predicate abstraction. - Chao Wang 001; Hyondeuk Kim; Aarti Gupta (ICCAD, 2007)

Disjunctive image computation for software verification. - Chao Wang 001; Zijiang Yang 006; Franjo Ivancic; Aarti Gupta (ACM Trans. Design Autom. Electr. Syst., 2007)

Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. - Chao Wang 001; Yu Yang 013; Aarti Gupta; Ganesh Gopalakrishnan (ATVA, 2008)

Embedded software verification: challenges and solutions. - Chao Wang 001; Malay K. Ganai; Shuvendu K. Lahiri; Daniel Kroening (ICCAD, 2008)

Modular verification of web services using efficient symbolic encoding and summarization. - Fang Yu 001; Chao Wang 001; Aarti Gupta; Tevfik Bultan (SIGSOFT FSE, 2008)

Peephole Partial Order Reduction. - Chao Wang 001; Zijiang Yang 006; Vineet Kahlon; Aarti Gupta (TACAS, 2008)

Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. - Vineet Kahlon; Chao Wang 001; Aarti Gupta (CAV, 2009)

Symbolic Predictive Analysis for Concurrent Programs. - Chao Wang 001; Sudipta Kundu; Malay K. Ganai; Aarti Gupta (FM, 2009)

Symbolic pruning of concurrent program executions. - Chao Wang 001; Swarat Chaudhuri; Aarti Gupta; Yu Yang 013 (ESEC/SIGSOFT FSE, 2009)

Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis. - Yu Yang 013; Xiaofang Chen; Ganesh Gopalakrishnan; Chao Wang 001 (SPIN, 2009)

Foreword: Special issue on numerical software verification. - Franjo Ivancic; Sriram Sankaranarayanan 001; Chao Wang 001 (Formal Methods Syst. Des., 2009)

Model checking sequential software programs via mixed symbolic analysis. - Zijiang Yang 006; Chao Wang 001; Aarti Gupta; Franjo Ivancic (ACM Trans. Design Autom. Electr. Syst., 2009)

Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs. - Vineet Kahlon; Chao Wang 001 (CAV, 2010)

Contessa: Concurrency Testing Augmented with Symbolic Analysis. - Sudipta Kundu; Malay K. Ganai; Chao Wang 001 (CAV, 2010)

Scalable and precise program analysis at NEC. - Gogul Balakrishnan; Malay K. Ganai; Aarti Gupta; Franjo Ivancic; Vineet Kahlon; Weihong Li; Naoto Maeda; Nadia Papakonstantinou; Sriram Sankaranarayanan 001; Nishant Sinha 001; Chao Wang 001 (FMCAD, 2010)

Efficient state space exploration: Interleaving stateless and state-based model checking. - Malay K. Ganai; Chao Wang 001; Weihong Li (ICCAD, 2010)

Interval Analysis for Concurrent Trace Programs Using Transaction Sequence Graphs. - Malay K. Ganai; Chao Wang 001 (RV, 2010)

Staged concurrent program analysis. - Nishant Sinha 001; Chao Wang 001 (SIGSOFT FSE, 2010)

Trace-Based Symbolic Analysis for Atomicity Violations. - Chao Wang 001; Rhishikesh Limaye; Malay K. Ganai; Aarti Gupta (TACAS, 2010)

Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search. - Arnab Sinha 001; Sharad Malik; Chao Wang 001; Aarti Gupta (Haifa Verification Conference, 2011)

Coverage guided systematic concurrency testing. - Chao Wang 001; Mahmoud Said; Aarti Gupta (ICSE, 2011)

BEST: A symbolic testing tool for predicting multi-threaded program failures. - Malay K. Ganai; Nipun Arora; Chao Wang 001; Aarti Gupta; Gogul Balakrishnan (ASE, 2011)

Predictive analysis for detecting serializability violations through Trace Segmentation. - Arnab Sinha 001; Sharad Malik; Chao Wang 001; Aarti Gupta (MEMOCODE, 2011)

Generating Data Race Witnesses by an SMT-Based Analysis. - Mahmoud Said; Chao Wang 001; Zijiang Yang 006; Karem A. Sakallah (NASA Formal Methods, 2011)

On interference abstractions. - Nishant Sinha 001; Chao Wang 001 (POPL, 2011)

Predicting Concurrency Failures in the Generalized Execution Traces of x86 Executables. - Chao Wang 001; Malay K. Ganai (RV, 2011)

Symbolic predictive analysis for concurrent programs. - Chao Wang 001; Sudipta Kundu; Rhishikesh Limaye; Malay K. Ganai; Aarti Gupta (Formal Aspects Comput., 2011)

Lock Removal for Concurrent Trace Programs. - Vineet Kahlon; Chao Wang 001 (CAV, 2012)

Interlocking obfuscation for anti-tamper hardware. - Avinash R. Desai; Michael S. Hsiao; Chao Wang 001; Leyla Nazhandali; T. Simin Hall (CSIIRW, 2013)

A novel statistical and circuit-based technique for counterfeit detection in existing ICs. - Rashmi Moudgil; Dinesh Ganta; Leyla Nazhandali; Michael S. Hsiao; Chao Wang 001; T. Simin Hall (ACM Great Lakes Symposium on VLSI, 2013)

CCmutator: A mutation generator for concurrency constructs in multithreaded C/C++ applications. - Markus Kusano; Chao Wang 001 (ASE, 2013)

Round-up: Runtime checking quasi linearizability of concurrent data structures. - Lu Zhang 035; Arijit Chattopadhyay; Chao Wang 001 (ASE, 2013)

Dynamic Analysis and Debugging of Binary Code for Security Applications. - Lixin Li; Chao Wang 001 (RV, 2013)

Synthesis of Masking Countermeasures against Side Channel Attacks. - Hassan Eldib; Chao Wang 001 (CAV, 2014)

QMS: Evaluating the Side-Channel Resistance of Masked Software from Source Code. - Hassan Eldib; Chao Wang 001; Mostafa M. I. Taha; Patrick Schaumont (DAC, 2014)

Runtime prevention of concurrency related type-state violations in multithreaded applications. - Lu Zhang 035; Chao Wang 001 (ISSTA, 2014)

Assertion guided abstraction: a cooperative optimization for dynamic partial order reduction. - Markus Kusano; Chao Wang 001 (ASE, 2014)

SMT-Based Verification of Software Countermeasures against Side-Channel Attacks. - Hassan Eldib; Chao Wang 001; Patrick Schaumont (TACAS, 2014)

Precisely Deciding Control State Reachability in Concurrent Traces with Limited Observability. - Chao Wang 001; Kevin Hoang (VMCAI, 2014)

An SMT Based Method for Optimizing Arithmetic Computations in Embedded Software Code. - Hassan Eldib; Chao Wang 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2014)

Formal Verification of Software Countermeasures against Side-Channel Attacks. - Hassan Eldib; Chao Wang 001; Patrick Schaumont (ACM Trans. Softw. Eng. Methodol., 2014)

Dynamic Generation of Likely Invariants for Multithreaded Programs. - Markus Kusano; Arijit Chattopadhyay; Chao Wang 001 (ICSE (1), 2015)

A Synergistic Analysis Method for Explaining Failed Regression Tests. - Qiuping Yi; Zijiang Yang 006; Jian Liu 008; Chen Zhao; Chao Wang 001 (ICSE (1), 2015)

Postconditioned Symbolic Execution. - Qiuping Yi; Zijiang Yang 006; Shengjian Guo; Chao Wang 001; Jian Liu 008; Chen Zhao (ICST, 2015)

ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugs. - Sepideh Khoshnood; Markus Kusano; Chao Wang 001 (ISSTA, 2015)

Dynamic partial order reduction for relaxed memory models. - Naling Zhang; Markus Kusano; Chao Wang 001 (PLDI, 2015)

Assertion guided symbolic execution of multithreaded programs. - Shengjian Guo; Markus Kusano; Chao Wang 001; Zijiang Yang 006; Aarti Gupta (ESEC/SIGSOFT FSE, 2015)

Shield Synthesis: - Runtime Enforcement for Reactive Systems. - Roderick Bloem; Bettina Könighofer; Robert Könighofer; Chao Wang 001 (TACAS, 2015)

Quantitative Masking Strength: Quantifying the Power Side-Channel Resistance of Software Code. - Hassan Eldib; Chao Wang 001; Mostafa M. I. Taha; Patrick Schaumont (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2015)

Explaining Software Failures by Cascade Fault Localization. - Qiuping Yi; Zijiang Yang 006; Jian Liu 008; Chen Zhao; Chao Wang 001 (ACM Trans. Design Autom. Electr. Syst., 2015)

Round-Up: Runtime Verification of Quasi Linearizability for Concurrent Data Structures. - Lu Zhang 035; Arijit Chattopadhyay; Chao Wang 001 (IEEE Trans. Software Eng., 2015)

Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits. - Hassan Eldib; Meng Wu 001; Chao Wang 001 (CAV (2), 2016)

GUICat: GUI testing as a service. - Lin Cheng; Jialiang Chang; Zijiang Yang 006; Chao Wang 001 (ASE, 2016)

Conc-iSE: incremental symbolic execution of concurrent software. - Shengjian Guo; Markus Kusano; Chao Wang 001 (ASE, 2016)

Synthesizing Runtime Enforcer of Safety Properties Under Burst Error. - Meng Wu 001; Haibo Zeng 001; Chao Wang 001 (NFM, 2016)

Flow-sensitive composition of thread-modular abstract interpretation. - Markus Kusano; Chao Wang 001 (SIGSOFT FSE, 2016)

Static DOM event dependency analysis for testing web applications. - Chungha Sung; Markus Kusano; Nishant Sinha 001; Chao Wang 001 (SIGSOFT FSE, 2016)

Abstraction and mining of traces to explain concurrency bugs. - Mitra Tabaei Befrouei; Chao Wang 001; Georg Weissenbacher (Formal Methods Syst. Des., 2016)

Verifying a quantitative relaxation of linearizability via refinement. - Kiran Adhikari; James Street; Chao Wang 001; Yang Liu 003; Shao Jie Zhang (Int. J. Softw. Tools Technol. Transf., 2016)

Safety Guard: Runtime Enforcement for Safety-Critical Cyber-Physical Systems: Invited. - Meng Wu 001; Haibo Zeng 001; Chao Wang 001; Huafeng Yu (DAC, 2017)

RClassify: classifying race conditions in web applications via deterministic replay. - Lu Zhang 035; Chao Wang 001 (ICSE, 2017)

Systematic reduction of GUI test sequences. - Lin Cheng; Zijiang Yang 006; Chao Wang 001 (ASE, 2017)

Modular verification of interrupt-driven software. - Chungha Sung; Markus Kusano; Chao Wang 001 (ASE, 2017)

Symbolic execution of programmable logic controller code. - Shengjian Guo; Meng Wu 001; Chao Wang 001 (ESEC/SIGSOFT FSE, 2017)

Thread-modular static analysis for relaxed memory models. - Markus Kusano; Chao Wang 001 (ESEC/SIGSOFT FSE, 2017)

DESCRY: reproducing system-level concurrency failures. - Tingting Yu; Tarannum S. Zaman; Chao Wang 001 (ESEC/SIGSOFT FSE, 2017)

Shield synthesis. - Bettina Könighofer; Mohammed Alshiekh; Roderick Bloem; Laura R. Humphrey; Robert Könighofer; Ufuk Topcu; Chao Wang 001 (Formal Methods Syst. Des., 2017)

Security by compilation: an automated approach to comprehensive side-channel resistance. - Chao Wang 001; Patrick Schaumont (ACM SIGLOG News, 2017)

SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks. - Jun Zhang; Pengfei Gao; Fu Song; Chao Wang 001 (CAV (2), 2018)

Eliminating timing side-channel leaks using program repair. - Meng Wu 001; Shengjian Guo; Patrick Schaumont; Chao Wang 001 (ISSTA, 2018)

Datalog-based scalable semantic diffing of concurrent programs. - Chungha Sung; Shuvendu K. Lahiri; Constantin Enea; Chao Wang 001 (ASE, 2018)

CANAL: a cache timing analysis framework via LLVM transformation. - Chungha Sung; Brandon Paulsen; Chao Wang 001 (ASE, 2018)

Adversarial symbolic execution for detecting concurrency-related cache timing leaks. - Shengjian Guo; Meng Wu 001; Chao Wang 001 (ESEC/SIGSOFT FSE, 2018)

Guest editorial: special issue on concurrent software quality. - Zijiang Yang 006; Ting Liu 002; Daniel Xiapu Luo; Chao Wang 001 (Softw. Qual. J., 2018)

Eliminating Path Redundancy via Postconditioned Symbolic Execution. - Qiuping Yi; Zijiang Yang 006; Shengjian Guo; Chao Wang 001; Jian Liu 008; Chen Zhao (IEEE Trans. Software Eng., 2018)

Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems. - Meng Wu 001; Jingbo Wang 006; Jyotirmoy Deshmukh; Chao Wang 001 (FMCAD, 2019)

Debreach: Mitigating Compression Side Channels via Static Analysis and Transformation. - Brandon Paulsen; Chungha Sung; Peter A. H. Peterson; Chao Wang 001 (ASE, 2019)

Abstract interpretation under speculative execution. - Meng Wu 001; Chao Wang 001 (PLDI, 2019)

Mitigating power side channels during compilation. - Jingbo Wang 006; Chungha Sung; Chao Wang 001 (ESEC/SIGSOFT FSE, 2019)

Verifying and Quantifying Side-channel Resistance of Masked Software Implementations. - Pengfei Gao; Jun Zhang; Fu Song; Chao Wang 001 (ACM Trans. Softw. Eng. Methodol., 2019)

ReluDiff: differential verification of deep neural networks. - Brandon Paulsen; Jingbo Wang 006; Chao Wang 001 (ICSE, 2020)

Towards understanding and fixing upstream merge induced conflicts in divergent forks: an industrial case study. - Chungha Sung; Shuvendu K. Lahiri; Mike Kaufman; Pallavi Choudhury; Chao Wang 001 (ICSE (SEIP), 2020)

Towards understanding and fixing upstream merge induced conflicts in divergent forks: an industrial case study. - Chungha Sung; Shuvendu K. Lahiri; Mike Kaufman; Pallavi Choudhury; Jessica Wolk; Chao Wang 001 (ICSE (Companion Volume), 2020)

NEURODIFF: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation. - Brandon Paulsen; Jingbo Wang 006; Jiawei Wang; Chao Wang 001 (ASE, 2020)

ConTesa: Directed Test Suite Augmentation for Concurrent Software. - Tingting Yu 001; Zunchen Huang; Chao Wang 001 (IEEE Trans. Software Eng., 2020)

DiffRNN: Differential Verification of Recurrent Neural Networks. - Sara Mohammadinejad; Brandon Paulsen; Jyotirmoy V. Deshmukh; Chao Wang 001 (FORMATS, 2021)

Data-Driven Synthesis of Provably Sound Side Channel Analyses. - Jingbo Wang 006; Chungha Sung; Mukund Raghothaman; Chao Wang 001 (ICSE, 2021)

Example Guided Synthesis of Linear Approximations for Neural Network Verification. - Brandon Paulsen; Chao Wang 001 (CAV (1), 2022)

Synthesizing Fair Decision Trees via Iterative Constraint Solving. - Jingbo Wang 006; Yannan Li; Chao Wang 001 (CAV (2), 2022)

Symbolic Predictive Cache Analysis for Out-of-Order Execution. - Zunchen Huang; Chao Wang 001 (FASE, 2022)

Proving Robustness of KNN Against Adversarial Data Poisoning. - Yannan Li; Jingbo Wang 006; Chao Wang 001 (FMCAD, 2022)

Learning to Synthesize Relational Invariants. - Jingbo Wang 006; Chao Wang 001 (ASE, 2022)

LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions. - Brandon Paulsen; Chao Wang 001 (TACAS (1), 2022)

Understanding Concurrency Vulnerabilities in Linux Kernel. - Zunchen Huang; Shengjian Guo; Meng Wu 001; Chao Wang 001 (CoRR, 2022)

Certifying the Fairness of KNN in the Presence of Dataset Bias. - Yannan Li; Jingbo Wang 006; Chao Wang 001 (CAV (2), 2023)

Constraint Based Compiler Optimization for Energy Harvesting Applications. - Yannan Li; Chao Wang 001 (ECOOP, 2023)

Systematic Testing of the Data-Poisoning Robustness of KNN. - Yannan Li; Jingbo Wang 006; Chao Wang 001 (ISSTA, 2023)

Synthesizing MILP Constraints for Efficient and Robust Optimization. - Jingbo Wang 006; Aarti Gupta; Chao Wang 001 (Proc. ACM Program. Lang., 2023)

Constraint Based Program Repair for Persistent Memory Bugs. - Zunchen Huang; Chao Wang 001 (ICSE, 2024)

Discovering Likely Program Invariants for Persistent Memory. - Zunchen Huang; Srivatsan Ravi; Chao Wang 001 (ASE, 2024)

DL4SC: a novel deep learning-based vulnerability detection framework for smart contracts. - Yang Liu 003; Chao Wang 001; Yan Ma (Autom. Softw. Eng., 2024)

Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions. - Jacqueline L. Mitchell; Chao Wang 001 (ECOOP, 2025)

WaSCR: A WebAssembly Instruction-Timing Side Channel Repairer. - Liyan Huang; Junzhou He; Chao Wang 001; Weihang Wang 001 (WWW, 2025)

Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions (Artifact). - Jacqueline L. Mitchell; Chao Wang 001 (Dagstuhl Artifacts Ser., 2025)

An Incremental Algorithm for Algebraic Program Analysis. - Chenyu Zhou; Yuzhou Fang; Jingbo Wang 006; Chao Wang 001 (Proc. ACM Program. Lang., 2025)

Can LLMs Formally Reason as Abstract Interpreters for Program Analysis? - Jacqueline L. Mitchell; Brian Hyeongseok Kim; Chenyu Zhou; Chao Wang 001 (CoRR, 2025)

Efficient Symbolic Execution of Software under Fault Attacks. - Yuzhou Fang; Chenyu Zhou; Jingbo Wang 006; Chao Wang 001 (CoRR, 2025)