Chao Wang

Proceedings of the ICSE '20: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June, 2020

2019

Verifying and Quantifying Side-channel Resistance of Masked Software Implementations.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2019

Mitigating power side channels during compilation.

[BibT_eX]

[DOI]

Jingbo Wang

Chungha Sung

Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019

Abstract interpretation under speculative execution.

[BibT_eX]

[DOI]

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Debreach: Mitigating Compression Side Channels via Static Analysis and Transformation.

[BibT_eX]

[DOI]

Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, 2019

Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems.

[BibT_eX]

[DOI]

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

2018

Eliminating Path Redundancy via Postconditioned Symbolic Execution.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2018

Guest editorial: special issue on concurrent software quality.

[BibT_eX]

[DOI]

Softw. Qual. J., 2018

Adversarial symbolic execution for detecting concurrency-related cache timing leaks.

[BibT_eX]

[DOI]

Shengjian Guo

Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2018

CANAL: a cache timing analysis framework via LLVM transformation.

[BibT_eX]

[DOI]

Chungha Sung

Brandon Paulsen

Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

Datalog-based scalable semantic diffing of concurrent programs.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

Eliminating timing side-channel leaks using program repair.

[BibT_eX]

[DOI]

Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2018

SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

Security by compilation: an automated approach to comprehensive side-channel resistance.

[BibT_eX]

[DOI]

Patrick Schaumont

ACM SIGLOG News, 2017

Shield synthesis.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

DESCRY: reproducing system-level concurrency failures.

[BibT_eX]

[DOI]

Tingting Yu

Tarannum S. Zaman

Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017

Thread-modular static analysis for relaxed memory models.

[BibT_eX]

[DOI]

Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017

Symbolic execution of programmable logic controller code.

[BibT_eX]

[DOI]

Shengjian Guo

Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017

Modular verification of interrupt-driven software.

[BibT_eX]

[DOI]

Chungha Sung

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Systematic reduction of GUI test sequences.

[BibT_eX]

[DOI]

Lin Cheng

Zijiang Yang

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

RClassify: classifying race conditions in web applications via deterministic replay.

[BibT_eX]

[DOI]

Proceedings of the 39th International Conference on Software Engineering, 2017

Safety Guard: Runtime Enforcement for Safety-Critical Cyber-Physical Systems: Invited.

[BibT_eX]

[DOI]

Proceedings of the 54th Annual Design Automation Conference, 2017

2016

Verifying a quantitative relaxation of linearizability via refinement.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2016

Abstraction and mining of traces to explain concurrency bugs.

[BibT_eX]

[DOI]

Mitra Tabaei Befrouei

Georg Weissenbacher

Formal Methods Syst. Des., 2016

Static DOM event dependency analysis for testing web applications.

[BibT_eX]

[DOI]

Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016

Flow-sensitive composition of thread-modular abstract interpretation.

[BibT_eX]

[DOI]

Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016

Synthesizing Runtime Enforcer of Safety Properties Under Burst Error.

[BibT_eX]

[DOI]

Haibo Zeng

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Conc-iSE: incremental symbolic execution of concurrent software.

[BibT_eX]

[DOI]

Shengjian Guo

Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

GUICat: GUI testing as a service.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

Round-Up: Runtime Verification of Quasi Linearizability for Concurrent Data Structures.

[BibT_eX]

[DOI]

Arijit Chattopadhyay

IEEE Trans. Software Eng., 2015

Explaining Software Failures by Cascade Fault Localization.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2015

Quantitative Masking Strength: Quantifying the Power Side-Channel Resistance of Software Code.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2015

Shield Synthesis: - Runtime Enforcement for Reactive Systems.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Assertion guided symbolic execution of multithreaded programs.

[BibT_eX]

[DOI]

Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, 2015

Dynamic partial order reduction for relaxed memory models.

[BibT_eX]

[DOI]

Naling Zhang

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugs.

[BibT_eX]

[DOI]

Sepideh Khoshnood

Proceedings of the 2015 International Symposium on Software Testing and Analysis, 2015

Postconditioned Symbolic Execution.

[BibT_eX]

[DOI]

Proceedings of the 8th IEEE International Conference on Software Testing, 2015

A Synergistic Analysis Method for Explaining Failed Regression Tests.

[BibT_eX]

[DOI]

Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

Dynamic Generation of Likely Invariants for Multithreaded Programs.

[BibT_eX]

[DOI]

Arijit Chattopadhyay

Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

2014

Formal Verification of Software Countermeasures against Side-Channel Attacks.

[BibT_eX]

[DOI]

Patrick Schaumont

ACM Trans. Softw. Eng. Methodol., 2014

An SMT Based Method for Optimizing Arithmetic Computations in Embedded Software Code.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2014

Precisely Deciding Control State Reachability in Concurrent Traces with Limited Observability.

[BibT_eX]

[DOI]

Kevin Hoang

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

SMT-Based Verification of Software Countermeasures against Side-Channel Attacks.

[BibT_eX]

[DOI]

Patrick Schaumont

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Assertion guided abstraction: a cooperative optimization for dynamic partial order reduction.

[BibT_eX]

[DOI]

Proceedings of the ACM/IEEE International Conference on Automated Software Engineering, 2014

Runtime prevention of concurrency related type-state violations in multithreaded applications.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Software Testing and Analysis, 2014

QMS: Evaluating the Side-Channel Resistance of Masked Software from Source Code.

[BibT_eX]

[DOI]

Proceedings of the 51st Annual Design Automation Conference 2014, 2014

Synthesis of Masking Countermeasures against Side Channel Attacks.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Dynamic Analysis and Debugging of Binary Code for Security Applications.

[BibT_eX]

[DOI]

Lixin Li

Proceedings of the Runtime Verification - 4th International Conference, 2013

Round-up: Runtime checking quasi linearizability of concurrent data structures.

[BibT_eX]

[DOI]

Arijit Chattopadhyay

Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

CCmutator: A mutation generator for concurrency constructs in multithreaded C/C++ applications.

[BibT_eX]

[DOI]

Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

A novel statistical and circuit-based technique for counterfeit detection in existing ICs.

[BibT_eX]

[DOI]

Proceedings of the Great Lakes Symposium on VLSI 2013 (part of ECRC), 2013

Interlocking obfuscation for anti-tamper hardware.

[BibT_eX]

[DOI]

Proceedings of the Cyber Security and Information Intelligence, 2013

2012

Lock Removal for Concurrent Trace Programs.

[BibT_eX]

[DOI]

Vineet Kahlon

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Symbolic predictive analysis for concurrent programs.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2011

Predicting Concurrency Failures in the Generalized Execution Traces of x86 Executables.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - Second International Conference, 2011

On interference abstractions.

[BibT_eX]

[DOI]

Nishant Sinha

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Generating Data Race Witnesses by an SMT-Based Analysis.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2011

Predictive analysis for detecting serializability violations through Trace Segmentation.

[BibT_eX]

[DOI]

Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, 2011

BEST: A symbolic testing tool for predicting multi-threaded program failures.

[BibT_eX]

[DOI]

Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), 2011

Coverage guided systematic concurrency testing.

[BibT_eX]

[DOI]

Mahmoud Said

Proceedings of the 33rd International Conference on Software Engineering, 2011

Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2011

2010

Trace-Based Symbolic Analysis for Atomicity Violations.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Staged concurrent program analysis.

[BibT_eX]

[DOI]

Nishant Sinha

Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

Interval Analysis for Concurrent Trace Programs Using Transaction Sequence Graphs.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - First International Conference, 2010

Efficient state space exploration: Interleaving stateless and state-based model checking.

[BibT_eX]

[DOI]

Weihong Li

Proceedings of the 2010 International Conference on Computer-Aided Design, 2010

Scalable and precise program analysis at NEC.

[BibT_eX]

[DOI]

Nadia Papakonstantinou

Sriram Sankaranarayanan

Nishant Sinha

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Contessa: Concurrency Testing Augmented with Symbolic Analysis.

[BibT_eX]

[DOI]

Sudipta Kundu

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs.

[BibT_eX]

[DOI]

Vineet Kahlon

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

Model checking sequential software programs via mixed symbolic analysis.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2009

Foreword: Special issue on numerical software verification.

[BibT_eX]

[DOI]

Franjo Ivancic

Sriram Sankaranarayanan

Formal Methods Syst. Des., 2009

Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis.

[BibT_eX]

[DOI]

Yu Yang

Xiaofang Chen

Ganesh Gopalakrishnan

Proceedings of the Model Checking Software, 2009

Symbolic pruning of concurrent program executions.

[BibT_eX]

[DOI]

Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009

Symbolic Predictive Analysis for Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the FM 2009: Formal Methods, 2009

Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique.

[BibT_eX]

[DOI]

Vineet Kahlon

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Peephole Partial Order Reduction.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Modular verification of web services using efficient symbolic encoding and summarization.

[BibT_eX]

[DOI]

Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008

Embedded software verification: challenges and solutions.

[BibT_eX]

[DOI]

Proceedings of the 2008 International Conference on Computer-Aided Design, 2008

Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions.

[BibT_eX]

[DOI]

Yu Yang

Ganesh Gopalakrishnan

Proceedings of the Automated Technology for Verification and Analysis, 2008

2007

Disjunctive image computation for software verification.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2007

Hybrid CEGAR: combining variable hiding and predicate abstraction.

[BibT_eX]

[DOI]

Hyondeuk Kim

Proceedings of the 2007 International Conference on Computer-Aided Design, 2007

Induction in CEGAR for Detecting Counterexamples.

[BibT_eX]

[DOI]

Franjo Ivancic

Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Abstraction Refinement for Large Scale Model Checking

[BibT_eX]

[DOI]

Series on Integrated Circuits and Systems, Springer, ISBN: 978-0-387-34600-7, 2006

Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2006

Compositional SCC Analysis for Language Emptiness.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2006

SAT-Based Verification Methods and Applications in Hardware Verification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Hardware Verification, 2006

Mixed symbolic representations for model checking software programs.

[BibT_eX]

[DOI]

Proceedings of the 4th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2006), 2006

Disjunctive image computation for embedded software verification.

[BibT_eX]

[DOI]

Proceedings of the Conference on Design, Automation and Test in Europe, 2006

Predicate learning and selective theory deduction for a difference logic solver.

[BibT_eX]

[DOI]

Proceedings of the 43rd Design Automation Conference, 2006

Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Whodunit? Causal Analysis for Counterexamples.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2006

2005

Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure.

[BibT_eX]

[DOI]

Bing Li

Int. J. Softw. Tools Technol. Transf., 2005

Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2005

Model Checking C Programs Using F-SOFT.

[BibT_eX]

[DOI]

Proceedings of the 23rd International Conference on Computer Design (ICCD 2005), 2005

2004

Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 22nd IEEE International Conference on Computer Design: VLSI in Computers & Processors (ICCD 2004), 2004

Refining the SAT decision ordering for bounded model checking.

[BibT_eX]

[DOI]

Proceedings of the 41th Design Automation Conference, 2004

2003

A satisfiability-based approach to abstraction refinement in model checking.

[BibT_eX]

[DOI]

Bing Li

Proceedings of the First International Workshop on Bounded Model Checking, 2003

Improving Ariadneýs Bundle by Following Multiple Threads in Abstraction Refinement.

[BibT_eX]

[DOI]

Proceedings of the 2003 International Conference on Computer-Aided Design, 2003

The Compositional Far Side of Image Computation.

[BibT_eX]

[DOI]

Proceedings of the 2003 International Conference on Computer-Aided Design, 2003

Learning from BDDs in SAT-based bounded model checking.

[BibT_eX]

[DOI]

Proceedings of the 40th Design Automation Conference, 2003

Abstraction and BDDs Complement SAT-Based BMC in DiVer.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002

Sharp Disjunctive Decomposition for Language Emptiness Checking.

[BibT_eX]

[DOI]