Publications

Experience Report: Insights from Deploying Educational Static Analysis in Introductory Programming Courses

Write Your Own CodeChecker: An Automated Test-Driven Checker Development Approach with LLMs

A Chopping-Based Approach for Debloating Android Applications

A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic

ConstraintLLM: A Neuro-Symbolic Framework for Industrial-Level Constraint Programming

IceBear: A Fine-Grained Incremental Scheduler for C/C++ Static Analyzers

StriCT-Bj:A String Constraint Benchmark from Real Java Programs

Automatic Construction of HD Maps for Simulation-Based Testing of Autonomous Driving Systems

Detecting Element Accessing Bugs in C++ Sequence Containers

DMMPP: Constructing Dummy Main Methods for Android Apps with Path-Sensitive Predicates

Fix the Tests: Augmenting LLMs to Repair Test Cases with Static Collector and Neural Reranker

Panda: A Concurrent Scheduler for Compiler-Based Tools

Parallel Verification for $\delta$-Equivalence of Neural Network Quantization

Can Graph Neural Networks Learn to Solve the MaxSAT Problem? (Student Abstract)

Detecting Exception Handling Bugs in C++ Programs

Detecting Memory Errors in Python Native Code by Tracking Object Lifecycle with Reference Count

Detection of Java Basic Thread Misuses Based on Static Event Analysis

ICTDroid: Parameter-Aware Combinatorial Testing for Components of Android Apps

Improving Bit-Blasting for Nonlinear Integer Constraints

Investigating the Existence of Holey Latin Squares via Satisfiability Testing

Locating Framework-specific Crashing Faults with Compact and Explainable Candidate Set

NRAgo: Solving SMT(NRA) Formulas with Gradient-Based Optimization

Operand-Variation-Oriented Differential Analysis for Fuzzing Binding Calls in PDF Readers

PSMT: Satisfiability Modulo Theories Meets Probability Distribution

Quantifying Robustness to Adversarial Word Substitutions

Runtime Monitoring DNN-Based Perception

Scope-based Compiler Differential Testing

Simulation-Based Validation for Autonomous Driving Systems

Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning.

Variable-strength combinatorial testing of exported activities based on misexposure prediction

A Comprehensive Evaluation of Android ICC Resolution Techniques

Adversarial Input Detection Based on Critical Transformation Robustness

AllSATCC: Boosting AllSAT Solving with Efficient Component Analysis

AUGER: automatically generating review comments with pre-training models

ComOpT: Combination and Optimization for Testing Autonomous Driving Systems

ExcePy: A Python Benchmark for Bugs with Python Built-in Types

Hunting bugs with accelerated optimal graph vertex matching

ICCBot: Fragment-Aware and Context-Sensitive ICC Resolution for Android Applications

Improving Simulated Annealing for Clique Partitioning Problems

Layer-Specific Repair of Neural Network Classifiers

Solving multi-objective constrained minimum weighted bipartite assignment problem: a case study on energy-aware radio broadcast scheduling

String Test Data Generation for Java Programs

Test case prioritization with neuron valuation based pattern

Word Level Robustness Enhancement: Fight Perturbation with Perturbation

𝜀 -weakened robustness of deep neural networks

Are the Scala Checks Effective? Evaluating Checks with Real-world Projects

Continuous Safety Verification of Neural Networks

Detecting Memory-Related Bugs by Tracking Heap Memory Management of C++ Smart Pointers

Dynamic Detection of AsyncTask Related Defects

Efficient SAT-Based Minimal Model Generation Methods for Modal Logic S5

Efficient testing of GUI applications by event sequence reduction

Investigating the Existence of Costas Latin Squares via Satisfiability Testing

Monitoring Object Detection Abnormalities via Data-Label and Post-Algorithm Abstractions

Stability evaluation for text localization systems via metamorphic testing

Testing Autonomous Systems with Believed Equivalence Refinement

A decomposition-based memetic algorithm using helper objectives for shortwave radio broadcast resource allocation problem in China

Combinatorial Testing of Browsers’ Support for Multimedia

Contention-Aware Mapping and Scheduling Optimization for NoC-Based MPSoCs.

GTFuzz: Guard Token Directed Grey-Box Fuzzing

Improving Fault-Localization Accuracy by Referencing Debugging History to Alleviate Structure Bias in Code Suspiciousness

Learning the Satisfiability of Pseudo-Boolean Problem with Graph Neural Networks

Multiple-entry testing of Android applications by constructing activity launching contexts

Neuron Activation Frequency Based Test Case Prioritization

PEACEPACT: Prioritizing Examples to Accelerate Perturbation-Based Adversary Generation for DNN Classification Testing

SinkFinder: harvesting hundreds of unknown interesting function pairs with just one seed

Static asynchronous component misuse detection for Android applications

ACFNet: Attentional Class Feature Network for Semantic Segmentation

Adaptive Random Testing for XSS Vulnerability

Analyses for specific defects in android applications: a survey

Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps

Androlic: an extensible flow, context, object, field, and path-sensitive static analysis framework for Android

Approximating Integer Solution Counting via Space Quantification for Linear Constraints

DroidLeaks: a comprehensive database of resource leaks in Android apps

Fine-Grained Communication-Aware Task Scheduling Approach for Acyclic and Cyclic Applications on MPSoCs

Investigating the Existence of Orthogonal Golf Designs via Satisfiability Testing

On some matching problems under the color-spanning model

Reorganizing and Optimizing Post-Inspection on Suspicious Bug Reports in Path-Sensitive Analysis

SMT-based Multi-objective Optimization for Scheduling of MPSoC Applications

Solving the Satisfiability Problem of Modal Logic S5 Guided by Graph Coloring

SPrinter: A Static Checker for Finding Smart Pointer Errors in C++ Programs

Testing the Message Flow of Android Auto Apps

Understanding Ineffective Events and Reducing Test Sequences for Android Applications

A Community-Division Based Algorithm for Finding Relations Among Linear Constraints

A New Probabilistic Algorithm for Approximate Model Counting

Android Stack Machine

Characterizing and identifying misexposed activities in Android applications

Checking Activity Transition Systems with Back Transitions Against Assertions

Computing and estimating the volume of the solution space of SMT(LA) constraints

Design Verification and Validation for Reliable Safety-Critical Autonomous Control Systems

Energy-Efficient Fault-Tolerant Mapping and Scheduling on Heterogeneous Multiprocessor Real-Time Systems

Energy-Efficient Scheduling of Periodic Applications on Safety-Critical Time-Triggered Multiprocessor Systems

Formal Collision Avoidance Analysis for Rigorous Building of Autonomous Marine Vehicles

Fuzzing: State of the Art

Generating minimal test set satisfying MC/DC criterion via SAT based approach

Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing

LAND: a user-friendly and customizable test generation tool for Android apps

Lightweight energy consumption analysis and prediction for Android applications

On the Fixed-Parameter Tractability of Some Matching Problems Under the Color-Spanning Model

Resource-Aware Design for Reliable Autonomous Applications with Multiple Periods

VolCE: An Efficient Tool for Solving #SMT(LA) Problems.

A Hybrid Multi-objective Evolutionary Algorithm for Energy-Aware Allocation and Scheduling Optimization of MPSoCs

A theoretical analysis on cloning the failed test cases to improve spectrum-based fault localization

Combinatorial Testing on Implementations of HTML5 Support

Comprehensive Static Analysis for Configurable Software via Combinatorial Instantiation

Detecting Energy Bugs in Android Apps Using Static Analysis

InsDal: A safe and extensible instrumentation tool on Dalvik byte-code for Android applications

Integrating ILP and SMT for Shortwave Radio Broadcast Resource Allocation and Frequency Assignment

On the Fixed-Parameter Tractability of Some Matching Problems Under the Color-Spanning Model.

Weak QMV algebras and some ring-like structures

Widget-Sensitive and Back-Stack-Aware GUI Exploration for Testing Android Apps

A deployable sampling strategy for data race detection

Component-based verification using incremental design and invariants

Fixing Resource Leaks in Android Apps with Light-Weight Static Analysis and Low-Overhead Instrumentation

Generating Covering Arrays with Pseudo-Boolean Constraint Solving and Balancing Heuristic

Light-Weight, Inter-Procedural and Callback-Aware Resource Leak Detection for Android Apps

Lightweight Method-Level Energy Consumption Estimation for Android Applications

Optimizing Shortwave Radio Broadcast Resource Allocation via Pseudo-Boolean Constraint Solving and Local Search

PEDAL: a dynamic analysis tool for efficient concurrency bug reproduction in big data environment

Relda2: an effective static analysis tool for resource leak detection in Android apps

The Floating-Point Extension of Symbolic Execution Engine for Bug Detection

A Fast and Practical Method to Estimate Volumes of Convex Polytopes

Automatic Detection of Parameter Shielding for Test Case Generation

Boundary value analysis in automatic white-box test generation

Communication Optimizations for Multithreaded Code Generation from Simulink Models

Formal consistency checking over specifications in natural languages.

Melton: a practical and precise memory leak detection tool for C programs

SMT Solving for the Theory of Ordering Constraints

Software Pipeline–Based Partitioning Method with Trade-Off between Workload Balance and Communication Optimization

Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking

Automated Coverage-Driven Test Data Generation Using Dynamic Symbolic Execution

Automatic Generation of Combinatorial Test Data

Automatic Test Data Generation for Unit Testing to Achieve MC/DC Criterion

Canalyze: a static bug-finding tool for C programs

Choreography Scenario-Based Test Data Generation

Generating combinatorial test suite using combinatorial optimization

ILP Based Multithreaded Code Generation for Simulink Model

Modeling and Verifying of CPS Component Services Based on Hybrid Automata

A Search Strategy Guided by Uncovered Branches for Concolic Testing

Cascade: A Test Generation Tool for Combinatorial Testing

Characterizing and detecting resource leaks in Android applications

Communication Pipelining for Code Generation from Simulink Models

Finding orthogonal latin squares using finite model searching tools

High throughput VLSI architecture for H.264/AVC context-based adaptive binary arithmetic coding (CABAC) decoding

MACE4 and SEM: A Comparison of Finite Model Generators

Performance Estimation Using Symbolic Data

Profile directed systematic testing of concurrent programs

Solving Nonlinear SMT Problems Based on an Efficient Lazy Method

Towards Conformance Testing of Choreography Based on Scenario

A Path-oriented Approach to Generating Executable Test Sequences for Extended Finite State Machines

An Efficient Lazy SMT Solver for Nonlinear Numerical Constraints

Faulty Interaction Identification via Constraint Solving and Optimization

Integrating Standard Dependency Schemes in QCSP Solvers

Solving Generalized Optimization Problems Subject to SMT Constraints

Characterizing failure-causing parameter interactions by adaptive testing

Memory Leak Detection Based on Memory State Transition Graph

Model Construction and Priority Synthesis for Simple Interaction Systems

Program analysis: from qualitative analysis to quantitative analysis (NIER track)

Searching for Doubly Self-orthogonal Latin Squares

Tuple density: a new metric for combinatorial test suites (NIER track)

A Memory Model for Static Analysis of C Programs

Automatic Bug Triage using Semi-Supervised Text Classification.

Combinatorial Testing with Shielding Parameters

Constraint solving techniques for software testing and analysis

JUTA: An Automated Unit Testing Framework for JavaJUTA: 一个Java自动化单元测试工具

Combinatorial Testing: Principles and Methods组合测试：原理与方法

Infinite Loop Detection Based on Path Analysis基于路径分析的死循环检测

Solving Global Unconstrained Optimization Problems by Symmetry-Breaking

Volume Computation for Boolean Combination of Linear Arithmetic Constraints

A backtracking search tool for constructing combinatorial test suites

An efficient method to generate feasible paths for basis path testing

Finding Orthogonal Arrays Using Satisfiability Checkers and Symmetry Breaking Constraints

Path and Context Sensitive Inter-procedural Memory Leak Detection

Path-based verification for composition of semantic web services

Test Data Generation for C Programs with String-Handling Functions

Computer Search for Large Sets of Idempotent Quasigroups

Improvements for the Symbolic Verification of Timed Automata

Volume Computation Using a Direct Monte Carlo Method

A Powerful Technique to Eliminate Isomorphism in Finite Model Search

A Test Data Generation Tool for Unit Testing of C Programs

Backtracking Algorithms and Search Heuristics to Generate Test Suites for Combinatorial Testing

BPEL4WS Unit Testing: Test Case Generation Using a Concurrent Path Analysis Approach

Finding Relations Among Linear Constraints

SAT Based Automated Test Case Generation for MUMCUT Coverage

Computer Search for Counterexamples to Wilkie’s Identity

Constraint Solving and Symbolic Execution

Predicate-Oriented Isomorphism Elimination in Model Finding.

Extending Finite Model Searching with Congruence Closure Computation

Improving First-order Model Searching by Propositional Reasoning and Lemma Learning.

Path-Oriented Test Data Generation Using Symbolic Execution and Constraint Solving Techniques.

Quantitative Analysis of Symbolic Execution

Symbolic execution of program paths involving pointer and structure variables

Automated test case generation for the stress testing of multimedia systems

Parallel Execution of Stochastic Search Procedures on Reduced SAT Instances

A CONSTRAINT SOLVER AND ITS APPLICATION TO PATH FEASIBILITY ANALYSIS

A path-based approach to the detection of infinite looping

Automatic generation of database instances for white-box testing

Automatic symmetry breaking method combined with SAT

Specification analysis and test data generation by solving Boolean combinations of numeric constraints

Stress Testing of Distributed Multimedia Software Systems.

System Description: MCS: Model-Based Conjecture Searching

Finite model generation and formal specification development

Combining Local Search and Backtracking Techniques for Constraint Satisfaction.

Constructing finite algebras with FALCON

System description generating models by SEM

Constraint propagation in model generation

SEM: a System for Enumerating Models.

Problems on the generation of finite models