The rapid advancement of diffusion models and personalization techniques has made it possible to recreate individual portraits from just a few publicly available images. While such capabilities empower various creative applications, they also introduce serious privacy concerns, as adversaries can exploit them to generate highly realistic impersonations. To counter these threats, anti-personalization methods have been proposed, which add adversarial perturbations to published images to disrupt the training of personalization models. However, existing approaches largely overlook the intrinsic multi-image nature of personalization and instead adopt a naive strategy of applying perturbations independently, as commonly done in single-image settings. This neglects the opportunity to leverage inter-image relationships for stronger privacy protection. Therefore, we advocate for a group-level perspective on privacy protection against personalization. Specifically, we introduce Cross-image Anti-Personalization (CAP), a novel framework that enhances resistance to personalization by enforcing style consistency across perturbed images. Furthermore, we develop a dynamic ratio adjustment strategy that adaptively balances the impact of the consistency loss throughout the attack iterations. Extensive experiments on the classical CelebA-HQ and VGGFace2 benchmarks show that CAP outperforms eight existing methods.

We present an on-the-fly synthesis framework for Linear Temporal Logic over Finite Traces ( LTL \({}_{f}\) ) based on top-down deterministic automata construction. Existing approaches rely on constructing a complete Deterministic Finite Automaton ( DFA ) corresponding to the LTL \({}_{f}\) specification, a process with doubly exponential complexity relative to formula size in the worst case. In this case, the synthesis cannot be conducted until the entire DFA is constructed. This inefficiency is the main bottleneck of existing approaches. To address this challenge, we first present a method for converting LTL \({}_{f}\) into Transition-Based DFA ( TDFA ) by directly leveraging LTL \({}_{f}\) semantics, incorporating intermediate results as direct components of the final automaton to enable parallelized synthesis and automata construction. We then explore the relationship between LTL \({}_{f}\) synthesis and TDFA games and subsequently develop an algorithm for performing LTL \({}_{f}\) synthesis via on-the-fly TDFA game solving. This algorithm traverses the state space in a global forward manner combined with a local backward method, along with detecting strongly connected components. Moreover, we introduce two optimization techniques—model-guided synthesis and state entailment—to enhance the practical efficiency of our approach. Experimental results demonstrate that our on-the-fly approach achieves the best performance on the tested benchmarks and effectively complements existing approaches.

In recent years, Text-to-Image (T2I) models have garnered significant attention due to their remarkable advancements. However, security concerns have emerged due to their potential to generate inappropriate or Not-Safe-For-Work (NSFW) images. In this paper, inspired by the observation that texts with different semantics can lead to similar human perceptions, we propose an LLM-driven perception-guided jailbreak method, termed PGJ. It is a black-box jailbreak method that requires no specific T2I model (model-free) and generates highly natural attack prompts. Specifically, we propose identifying a safe phrase that is similar in human perception yet inconsistent in text semantics with the target unsafe word and using it as a substitution. The experiments conducted on six open-source models and commercial online services with thousands of prompts have verified the effectiveness of PGJ.

Yihao Huang, Chong Wang, Xiaojun Jia, Qing Guo, Felix Juefei-Xu, Jian Zhang, Yang Liu, Geguang Pu. Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2025.

Reactive synthesis from Linear Temporal Logic over finite traces (LTLf) can be reduced to a two-player game over a Deterministic Finite Automaton (DFA) of the LTLf specification. The primary challenge here is DFA construction, which is 2EXPTIME-complete in the worst case. Existing techniques either construct the DFA compositionally before solving the game, leveraging automata minimization to mitigate state-space explosion, or build the DFA incrementally during game solving to avoid full DFA construction. However, neither is dominant. In this paper, we introduce a compositional on-the-fly synthesis framework that integrates the strengths of both approaches, focusing on large conjunctions of smaller LTLf formulas common in practice. This framework applies composition during game solving instead of automata (game arena) construction. While composing all intermediate results may be necessary in the worst case, pruning these results simplifies subsequent compositions and enables early detection of unrealizability. Specifically, the framework allows two composition variants: pruning before composition to take full advantage of minimization or pruning during composition to guide on-the-fly synthesis. Compared to state-of-the-art synthesis solvers, our framework is able to solve a notable number of instances that other solvers cannot handle. A detailed analysis shows that both composition variants have unique merits.

Model checking has achieved remarkable success in the hardware domain, largely due to the accumulation of intricate optimizations and finely tuned implementation details. As tools evolve, diagnosing performance differences to better understand the interplay of these factors has become increasingly important. Yet existing problems that reveal such differences are often too large for meaningful inspection, limiting their diagnostic value.To address the problem, this paper proposes AIGROW, a framework for generating hardware model checking problems, and introduces our experience on diagnosing performance differences in model checkers with the generated problems. AIGROW uses a feedback-guided process that evolves problems based on runtime information, selectively retaining those that become more difficult for a target checker. Performance differences are then revealed by evaluating these problems across hardware model checkers that have similar algorithms.Our evaluation demonstrates that AIGROW generates problems that are more than 100 times smaller than those produced by existing generators, while still revealing substantial performance differences. Diagnosing the performance differences has led to concrete improvements in CAR-based checkers: (1) uncovering structural inefficiencies in their exploration strategies, (2) solving 18 previously unsolvable HWMCC’24 problems, and (3) reducing runtime from hours to minutes in several cases.

Model checking is an automatic formal verification technique that is widely used in hardware verification. The state-of-the-art complete model-checking techniques, based on IC3/PDR and its general variant CAR, are based on computing symbolically sets of under- and over-approximating state sets (called “frames”) with multiple calls to a SAT solver. The performance of those techniques is sensitive to the order of the assumptions with which the SAT solver is invoked, because it affects the unsatisfiable cores that it emits if the formula is unsatisfiable—which the solver emits when the formula is unsatisfiable—that crucially affect the search process. This observation was previously published (Dureja et al., 2020), where two partial assumption ordering strategies, intersection and rotation were suggested (partial in the sense that they determine the order of only a subset of the literals). In this article we extend and improve these strategies based on an analysis of the reason for their effectiveness. We prove that intersection is effective because of what we call locality of the cores, and our improved strategy is based on this observation. We conclude our paper with an extensive empirical evaluation of the various ordering techniques. One of our strategies, Hybrid-CAR, which switches between strategies at runtime, not only outperforms other, fixed ordering strategies, but also outperforms other state-of-the-art bug-finding algorithms, such as ABC-BMC.

The advent of local continuous image function (LIIF) has garnered significant attention for arbitrary-scale super-resolution (SR) techniques. However, while the vulnerabilities of fixed-scale SR have been assessed, the robustness of continuous representation-based arbitrary-scale SR against adversarial attacks remains an area warranting further exploration. The elaborately designed adversarial attacks for fixed-scale SR are scale-dependent, which will cause time-consuming and memory-consuming problems when applied to arbitrary-scale SR. To address this concern, we propose a simple yet effective “scale-invariant” SR adversarial attack method with good transferability, termed SIAGT. Specifically, we propose to construct resource-saving attacks by exploiting finite discrete points of continuous representation. In addition, we formulate a coordinate-dependent loss to enhance the cross-model transferability of the attack. The attack can significantly deteriorate the SR images while introducing imperceptible distortion to the targeted low-resolution (LR) images. Experiments carried out on three popular LIIF-based SR approaches and four classical SR datasets show remarkable attack performance and transferability of SIAGT.

Although recent personalization methods have democratized high-resolution image synthesis by enabling swift concept acquisition with minimal examples and lightweight computation, they also present an exploitable avenue for highly accessible backdoor attacks. This paper investigates a critical and unexplored aspect of text-to-image (T2I) diffusion models - their potential vulnerability to backdoor attacks via personalization. By studying the prompt processing of popular personalization methods (epitomized by Textual Inversion and DreamBooth), we have devised dedicated personalization-based backdoor attacks according to the different ways of dealing with unseen tokens and divide them into two families: nouveau-token and legacy-token backdoor attacks. In comparison to conventional backdoor attacks involving the fine-tuning of the entire text-to-image diffusion model, our proposed personalization-based backdoor attack method can facilitate more tailored, efficient, and few-shot attacks. Through comprehensive empirical study, we endorse the utilization of the nouveau-token backdoor attack due to its impressive effectiveness, stealthiness, and integrity, markedly outperforming the legacy-token backdoor attack.

Co-salient object detection (CoSOD) aims to identify the common and salient (usually in the foreground) regions across a given group of images. Although achieving sig-nificant progress, state-of-the-art CoSODs could be easily affected by some adversarial perturbations, leading to sub-stantial accuracy reduction. The adversarial perturbations can mislead CoSODs but do not change the high-level se-mantic information (e.g., concept) of the co-salient objects. In this paper, we propose a novel robustness enhancement framework by first learning the concept of the co-salient ob-jects based on the input group images and then leveraging this concept to purify adversarial perturbations, which are subsequently fed to CoSODs for robustness enhancement. Specifically, we propose Cosalpure containing two modules, i.e., group-image concept learning and concept-guided diffusion purification. For the first module, we adopt a pre-trained text-to-image diffusion model to learn the con-cept of co-salient objects within group images where the learned concept is robust to adversarial examples. For the second module, we map the adversarial image to the latent space and then perform diffusion generation by embedding the learned concept into the noise prediction function as an extra condition. Our method can effectively alleviate the in-fluence of the SOTA adversarial attack containing different adversarial patterns, including exposure and noise. The ex-tensive results demonstrate that our method could enhance the robustness of Cos ODs significantly. The project is avail-able at https://vllen.github.io/CosalPure/.

The adversarial patch attack aims to fool image classifiers within a bounded, contiguous region of arbitrary changes. To address this problem in a trustworthy way, the certified patch defense methods are proposed. However, the state-of-the-art certified defenses inevitably needed to access the size of the adversarial patch, which is unreasonable and impractical in real-world attack scenarios. To improve the feasibility of the architecture-agnostic certified defense in a black-box setting, we propose a novel two-stage Iterative Black-box Certified Defense method, termed IBCD. In the first stage, it estimates the patch size in a search-based manner by evaluating the size relationship between the patch and mask with pixel masking. In the second stage, the accuracy results are calculated by the existing white-box certified defense methods with the estimated patch size. The experiments conducted on two popular model architectures and two datasets verify the effectiveness and efficiency of IBCD.

As a rapidly evolving AI technology, deep neural networks are becoming increasingly integrated into human society, yet raising concerns about fairness issues. Previous studies have proposed a metric called causal fairness to measure the fairness of machine learning models and proposed some search algorithms to mine individual discrimination instance pairs (IDIPs). Fairness issues can be alleviated by retraining models with corrected IDIPs. However, the number of samples that are used as seeds for these methods is often limited due to the pursuit of efficiency. In addition, the quantity of IDIPs generated on different seeds varies, so it makes sense to select appropriate samples as seeds, which has not been sufficiently considered in past studies. In this paper, we study the imbalance in IDIP quantities for various datasets and sensitive attributes, highlighting the need for selecting and ranking seed samples. Then, we proposed FIPSER, a feature importance and perturbation potential-based seed prioritization method. Our experimental results show that, on average, when applied to the current state-of-the-art method of IDIP mining, FIPSER can improve its effectiveness by 45% and efficiency by 11%.

Finding non-crashing functional bugs for Android apps is challenging for both manual testing and automated GUI testing techniques. This paper introduces and designs a general and practical testing technique based on the idea of property-based testing for finding such bugs. Specifically, our technique incorporates (1) a property description language (PDL) to allow specifying desired app properties, and (2) two exploration strategies as the input generators for effectively validating the properties. We implemented our technique as a tool named Kea and evaluated it on 124 historical bugs from eight real-world, popular Android apps. Our evaluation shows that our PDL can specify all the app properties violated by these historical bugs, demonstrating its generability for finding functional bugs. Kea successfully found 66 (68.0%) and 92 (94.8%) of the 97 historical bugs in scope under the two exploration strategies, demonstrating its practicability. Moreover, Kea found 25 new functional bugs on the latest versions of these eight apps, given the specified properties. To date, all these bugs have been confirmed, and 21 have been fixed. In comparison, prior state-of-the-art techniques found only 13 (13.4%) historical bugs and 1 new bug. We have made all the artifacts publicly available at https://github.com/ecnusse/Kea.

The current high-fidelity generation and high-precision detection of DeepFake images are at an arms race. We believe that producing DeepFakes that are highly realistic and “detection evasive” can serve the ultimate goal of improving future generation DeepFake detection capabilities. In this paper, we propose a simple yet powerful pipeline to reduce the artifact patterns of fake images without hurting image quality by performing implicit spatial-domain notch filtering. We first demonstrate that frequency-domain notch filtering, although famously shown to be effective in removing periodic noise in the spatial domain, is infeasible for our task at hand due to the manual designs required for the notch filters. We, therefore, resort to a learning-based approach to reproduce the notch filtering effects, but solely in the spatial domain. We adopt a combination of adding overwhelming spatial noise for breaking the periodic noise pattern and deep image filtering to reconstruct the noise-free fake images, and we name our method DeepNotch. Deep image filtering provides a specialized filter for each pixel in the noisy image, producing filtered images with high fidelity compared to their DeepFake counterparts. Moreover, we also use the semantic information of the image to generate an adversarial guidance map to add noise intelligently. Our large-scale evaluation on 3 representative DeepFake detection methods (tested on 16 types of DeepFakes) has demonstrated that our technique significantly reduces the accuracy of these 3 fake image detection methods, 36.79% on average and up to 97.02% in the best case.

Universal adversarial perturbation (UAP), also known as image-agnostic perturbation, is a fixed perturbation map that can fool the classifier with high probabilities on arbitrary images, making it more practical for attacking deep models in the real world. Previous UAP methods generate a scale-fixed and texture-fixed perturbation map for all images, which ignores the multi-scale objects in images and usually results in a low fooling ratio. Since the widely used convolution neural networks tend to classify objects according to semantic information stored in local textures, it seems a reasonable and intuitive way to improve the UAP from the perspective of utilizing local contents effectively. In this work, we find that the fooling ratios significantly increase when we add a constraint to encourage a small-scale UAP map and repeat it vertically and horizontally to fill the whole image domain. To this end, we propose texture scale-constrained UAP (TSC-UAP), a simple yet effective UAP enhancement method that automatically generates UAPs with category-specific local textures that can fool deep models more easily. Through a low-cost operation that restricts the texture scale, TSC-UAP achieves a considerable improvement in the fooling ratio and attack transferability for both data-dependent and data-free UAP methods. Experiments conducted on two state-of-the-art UAP methods, eight popular CNN models and four classical datasets show the remarkable performance of TSC-UAP.

Bokeh effect is a natural shallow depth-of-field phenomenon that blurs the out-of-focus part in photography. In recent years, a series of works have proposed automatic and realistic bokeh rendering methods for artistic and aesthetic purposes. They usually employ cutting-edge data-driven deep generative networks with complex training strategies and network architectures. However, these works neglect that the bokeh effect, as a real phenomenon, can inevitably affect the subsequent visual intelligent tasks like recognition, and their data-driven nature prevents them from studying the influence of bokeh-related physical parameters (i.e., depth-of-the-field) on the intelligent tasks. To fill this gap, we study a totally new problem, i.e.,natural & adversarial bokeh rendering, which consists of two objectives: rendering realistic and natural bokeh and fooling the visual perception models (i.e., bokeh-based adversarial attack). To this end, beyond the pure data-driven solution, we propose a hybrid alternative by taking the respective advantages of data-driven and physical-aware methods. Specifically, we propose thecircle-of-confusion predictive network (CoCNet)by taking the all-in-focus image and depth image as inputs to estimate circle-of-confusion parameters for each pixel, which are employed to render the final image through a well-known physical model of bokeh. With the hybrid solution, our method could achieve more realistic rendering results with the naive training strategy and a much lighter network. Moreover, we propose the adversarial bokeh attack by fixing the CoCNet while optimizing the depth map w.r.t. the visual perception tasks. Then, we are able to study the vulnerability of deep neural networks according to the depth variations in the real world. The extensive experiments show that our method produces more realistic bokeh than the state-of-the-art methods while fooling the powerful deep neural networks with a high accuracy drop.

Abstract / and its variants have been the prominent approaches to safety model checking in recent years. Compared to the previous model-checking algorithms like (Bounded Model Checking) and (Interpolation Model Checking), / is attractive due to its completeness (vs. ) and scalability (vs. ). / maintains an over-approximate state sequence for proving the correctness. Although the sequence refinement methodology is known to be crucial for performance, the literature lacks a systematic analysis of the problem. We propose an approach based on the definition of i- good lemmas, and the introduction of two kinds of heuristics, i.e., and , to steer the search towards the construction of $$i$$ -good lemmas. The approach is applicable to and its variant (Complementary Approximate Reachability), and it is very easy to integrate within existing systems. We implemented the heuristics into two open-source model checkers, and , as well as into the mature platform, and carried out an extensive experimental evaluation on HWMCC benchmarks. The results show that the proposed heuristics can effectively compute more $$i$$ -good lemmas, and thus improve the performance of all the above checkers.

Android apps are ubiquitous and serve many aspects of our daily lives. Ensuring their functional correctness is crucial for their success. To date, we still lack a general and in-depth understanding of functional bugs, which hinders the development of practices and techniques to tackle functional bugs. To fill this gap, we conduct the first systematic study on 399 functional bugs from 8 popular open-source and representative Android apps to investigate the root causes, bug symptoms, test oracles, and the capabilities and limitations of existing testing techniques. This study took us substantial effort. It reveals several new interesting findings and implications which help shed light on future research on tackling functional bugs. Furthermore, findings from our study guided the design of a proof-of-concept differential testing tool, RegDroid, to automatically find functional bugs in Android apps. We applied RegDroid on 5 real-world popular apps, and successfully discovered 14 functional bugs, 10 of which were previously unknown and affected the latest released versions—all these 10 bugs have been confirmed and fixed by the app developers. Specifically, 10 out of these 14 found bugs cannot be found by existing testing techniques. We have made all the artifacts (including the dataset of 399 functional bugs and RegDroid) in our work publicly available at https://github.com/Android-Functional-bugs-study/home.

Most researchers have tried to enhance the robustness of deep neural networks (DNNs) by revealing and repairing the vulnerability of DNNs with specialized adversarial examples. Parts of the attack examples have imperceptible perturbations restricted by Lp norm. However, due to their high-frequency property, the adversarial examples can be defended by denoising methods and are hard to realize in the physical world. To avoid the defects, some works have proposed unrestricted attacks to gain better robustness and practicality. It is disappointing that these examples usually look unnatural and can alert the guards. In this paper, we propose Adversarial Lightness Attack (ALA), a white-box unrestricted adversarial attack that focuses on modifying the lightness of the images. The shape and color of the samples, which are crucial to human perception, are barely influenced. To obtain adversarial examples with a high attack success rate, we propose unconstrained enhancement in terms of the light and shade relationship in images. To enhance the naturalness of images, we craft the naturalness-aware regularization according to the range and distribution of light. The effectiveness of ALA is verified on two popular datasets for different tasks (i.e., ImageNet for image classification and Places-365 for scene recognition).

Interlocking has long played a crucial role in railway systems. Its functional correctness, particularly concerning safety, forms the foundation of the entire signaling system. To date, numerous efforts have been made to formally model and verify interlocking systems. However, two main problems persist in most prior work: (1) The formal description of the interlocking system heavily depends on reusing existing models, which often results in overgeneralization and failing to fully utilize the intrinsic characteristics of interlocking systems. (2) The verification techniques of current approaches may quickly become outdated, and there is no adaptable method to integrate state-of-the-art verification algorithms or tools.

Benchmarking software testing tools against known bugs is a classic approach to evaluating the tools’ bug finding abilities. However, this approach is difficult to give some clues on the tool-missed bugs to aid diagnosing the testing tools. As a result, heavy and ad hoc manual analysis is needed. In this work, in the setting of GUI testing for Android apps, we introduce an automata-based trace analysis approach to tackling the key challenge of manual analysis, i.e., how to analyze the lengthy event traces generated by a testing tool against a missed bug to find the clues. Our key idea is that, we model a bug in the form of a finite automaton which captures its bug-triggering traces; and match the event traces generated by the testing tool (which misses this bug) against this automaton to obtain the clues. Specifically, the clues are presented in the form of three designated automata-based coverage values. We apply our approach to enhance Themis, a representative benchmark suite for Android, to aid diagnosing GUI testing tools. Our extensive evaluation on nine state-of-the-art GUI testing tools and the involvement with several tool developers shows that our approach is feasible and useful. Our approach enables Themis+ (the enhanced benchmark suite) to provide the clues on the tool-missed bugs, and all the Themis+’s clues are identical or useful, compared to the manual analysis results of tool developers. Moreover, the clues have helped find several tool weaknesses, which were unknown or unclear before. Based on the clues, two actively-developing industrial testing tools in our study have quickly made several optimizations and demonstrated their improved bug finding abilities. All the tool developers give positive feedback on the usefulness and usability of Themis+’s clues. Themis+ is available at https://github.com/DDroid-Android/home.

Like many software applications, data manipulation functionalities( DMFs ) are prevalent in Android apps, which perform the common CRUD operations (create, read, update, delete) to handle app-specific data. Thus, ensuring the correctness of these DMFs is fundamentally important for many core app functionalities. However, the bugs related to DMFs (named as data manipulation errors, DMEs ), especially those non-crashing logic ones, are prevalent but difficult to find. To this end, inspired by property-based testing, we introduce a property-based fuzzing approach to effectively finding DMEs in Android apps. Our key idea is that, given some type of app data of interest, we randomly interleave its relevant DMFs and other possible events to explore diverse app states for thorough validation. Specifically, our approach characterizes DMFs in (data) model-based properties and leverage the consistency between the data model and the UI layouts as the handler to do property checking. The properties of DMFs are specified by human according to specific app features. To support the application of our approach, we implemented an automated GUI testing tool, PBFDroid. We evaluated PBFDroid on 20 real-world Android apps, and successfully found 30 unique and previously unknown bugs in 18 apps. Out of the 30 bugs, 29 of which are DMEs (22 are non-crashing logic bugs, and 7 are crash ones). To date, 19 have been confirmed and 9 have already been fixed. Many of these bugs are non-trivial and lead to different types of app failures. Our further evaluation confirms that none of the 22 non-crashing DMEs can be found by the state-of-the-art techniques. In addition, a user study shows that the manual cost of specifying the DMF properties with the assistance of our tool is acceptable. Overall, given accurate DMF properties, our approach can automatically find DMEs without any false positives. We have made all the artifacts publicly available at:https:// github.com/ property-based-fuzzing/ home.

Abstract We present , a fuzzer to generate random word-level model checking problems in Btor2 format. Btor2 is one of the mainstream input formats for word-level hardware model checking and was used in the most recent hardware model checking competition. Compared to bit-level one, word-level model checking is a more complex research field at an earlier stage of development. Therefore, it is necessary to develop a tool that can produce a large number of test cases in Btor2 format to test either existing or under-developed word-level model checkers. To evaluate the practicality of , we tested the state-of-the-art word-level model checkers and with the generated benchmarks. Experimental results show that both tools are buggy and not mature enough, which reflects the practical value of .

Model checking is an automatic formal verification method that is widely applied to hardware verification. Safety properties are the mainly verified properties in practice that can be falsified within finite steps if they do not hold for systems. However, state-of-the-art safety model-checking algorithms cannot meet the performance requirement driven by the industry as the sizes of (hardware) systems to be verified increase rapidly. Therefore, more efficient techniques are still eagerly in demand. Recently, a new safety model-checking technique complementary approximate reachability (CAR) was presented and received considerable concerns from the community. CAR has shown its advantages in unsafe checking (bug finding), but cannot be as competitive as other state-of-the-art techniques, e.g., IC3/PDR, on safe checking (proving correctness). In this article, we propose four kinds of heuristics, two inspired by IC3/PDR and another two dedicated to CAR, to improve the performance of CAR. We integrate the heuristics into the open-source model checker SimpleCAR and compare the performance to the original CAR and IC3/PDR on 748 instances from the hardware model-checking competitions. Our results show that by fixing the time and memory resources, CAR can solve 124 more instances with the four proposed heuristics, i.e., 53.4% more instances can be solved comparing to the original CAR. Furthermore, CAR in both forward and backward directions can solve ten more instances than IC3/PDR in corresponding directions, and uniquely solve 44 more instances that IC3/PDR in corresponding directions cannot solve, which increases the capability of the current model-checking portfolio.

Android, the most popular mobile system, offers a number of user-configurable system settings (e.g., network, location, and permission) for controlling devices and apps. Even popular, well-tested apps may fail to properly adapt their behaviors to diverse setting changes, thus frustrating their users. However, there exists no effort to systematically investigate such defects. To this end, we conduct thefirstlarge-scale empirical study to understand and characterize thesesystem setting-related defects(in short as “setting defects”), whichreside in apps and are triggered by system setting changes. We devote substantial manual effort (over four person-months) to analyze 1,074 setting defects from 180 popular apps on GitHub. We investigate the impact, root causes, and consequences of these setting defects and their correlations. We find that (1) setting defects have a wide impact on apps’ correctness with diverse root causes, (2) the majority of these defects ($\approx$70.7%) cause non-crashing (logic) failures, and (3) some correlations exist between the setting categories, root causes, and consequences. Motivated and informed by these findings, we propose two bug-finding techniques that can synergistically detect setting defects from both the GUI and code levels. Specifically, at the GUI level, we design and introducesetting-wise metamorphic fuzzing, thefirstautomated dynamic testing technique to detect setting defects (causing crashandnon-crashing failures, respectively) for Android apps. We implement this technique as an end-to-end, automated GUI testing tool namedSetDroid. At the code level, we distill two major fault patterns and implement a static analysis tool namedSetCheckerto identify potential setting defects. We evaluateSetDroidandSetCheckeron 26 popular, open-source Android apps, and they find 48 unique, previously-unknown setting defects. To date, 35 have been confirmed and 21 have been fixed by app developers. We also applySetDroidandSetCheckeron five highly popular industrial apps, namely WeChat, QQMail, TikTok, CapCut, and AlipayHK, all of which each have billions of monthly active users.SetDroidsuccessfully detects 17 previously unknown setting defects in these apps’ latest releases, and all defects have been confirmed and fixed by the app vendors. After that, we collaborate with ByteDance and deploy these two bug-finding techniques internally to stress-test TikTok, one of its major app products. Within a two-month testing campaign,SetDroidsuccessfully finds 53 setting defects, andSetCheckerfinds 22 ones. So far, 59 have been confirmed and 31 have been fixed. All these defects escaped from prior developer testing. By now,SetDroidhas been integrated into ByteDance's official app testing infrastructure namedFastBotfor daily testing. These results demonstrate the strong effectiveness and practicality of our proposed techniques.

Bounded Model Checking (BMC) is so far considered as the best engine for bug-finding in hardware model checking. Given a bound K, BMC can detect if there is a counterexample to a given temporal property within K steps from the initial state, thus performing a global-style search. Recently, a SAT-based model-checking technique called Complementary Approximate Reachability (CAR) was shown to be complementary to BMC, in the sense that frequently they can solve instances that the other technique cannot, within the same time limit. CAR detects a counterexample gradually with the guidance of an over-approximating state sequence, and performs a local-style search. In this paper, we consider three different ways to combine BMC and CAR. Our experiments show that they all outperform BMC and CAR on their own, and solve instances that cannot be solved by these two techniques. Our findings are based on a comprehensive experimental evaluation using the benchmarks of two hardware model checking competitions.

Full face synthesis and partial face manipulation by virtue of the generative adversarial networks (GANs) and its variants have raised wide public concerns. In the multi-media forensics area, detecting and ultimately locating the image forgery has become an imperative task. In this work, we investigate the architecture of existing GAN-based face manipulation methods and observe that the imperfection of upsampling methods therewithin could be served as an important asset for GAN-synthesized fake image detection and forgery localization. Based on this basic observation, we have proposed a novel approach, termedFakeLocator, to obtain high localization accuracy, at full resolution, on manipulated facial images. To the best of our knowledge, this is the very first attempt to solve the GAN-based fake localization problem with a gray-scale fakeness map that preserves more information of fake regions. To improve the universality ofFakeLocatoracross multifarious facial attributes, we introduce an attention mechanism to guide the training of the model. To improve the universality ofFakeLocatoracross different DeepFake methods, we propose partial data augmentation and single sample clustering on the training images. Experimental results on popular FaceForensics++, DFFD datasets and seven different state-of-the-art GAN-based face generation methods have shown the effectiveness of our method. Compared with the baselines, our method performs better on various metrics. Moreover, the proposed method is robust against various real-world facial image degradations such as JPEG compression, low-resolution, noise, and blur.

Mobile apps have become ubiquitous. Ensuring their correctness and reliability is important. However, many apps still suffer from occasional to frequent crashes, weakening their competitive edge. Large-scale, deep analyses of the characteristics of real-world app crashes can provide useful insights to both developers and researchers. However, such studies are difficult and yet to be carried out — this work fills this gap. We collected 16,245 and 8,760 unique exceptions from 2,486 open-source and 3,230 commercial Android apps, respectively, and observed that the exceptions thrown from Android framework (termed“framework-specific exceptions”) account for the majority. With one-year effort, we (1) extensively investigated these framework-specific exceptions, and (2) further conducted an online survey of 135 professional app developers about how they analyze, test, reproduce and fix these exceptions. Specifically, we aim to understand the framework-specific exceptions from several perspectives: (i) their characteristics (e.g., manifestation locations, fault taxonomy), (ii) the developers’ testing practices, (iii) existing bug detection techniques’ effectiveness, (iv) their reproducibility and (v) bug fixes. To enable follow-up research (e.g., bug understanding, detection, localization and repairing), we further systematically constructed,DroidDefects, the first comprehensive and largest benchmark of Android app exception bugs. This benchmark contains 33reproducibleexceptions (with test cases, stack traces, faulty and fixed app versions, bug types, etc.), and 3,696ground-truthexceptions (real faults manifested by automated testing tools), which cover the apps with different complexities and diverse exception types. Based on our findings, we also built two prototype tools: Stoat+, an optimized dynamic testing tool, which quickly uncovered three previously-unknown, fixed crashes in Gmail and Google+; ExLocator, an exception localization tool, which can locate the root causes of specific exception types. Our dataset, benchmark and tools are publicly available onhttps://github.com/tingsu/droiddefects.

We present a new synthesis framework based on the on-the-fly DFA construction for LTL over finite traces (LTLf ). Extant approaches rely heavily on the construction of the complete DFA w.r.t. the input LTLf formula, whose size can be doubly exponential to the size of the formula in the worst case. Under those approaches, the synthesis cannot be conducted unless the whole DFA is completely constructed, which is not only inefficient but also not scalable in practice. Indeed, the DFA construction is the main bottleneck of LTLf synthesis in prior work. To mitigate this challenge, we follow two steps in this paper: Firstly, we present several light-weight pre-processing techniques such that the synthesis result can be obtained even without DFA construction; Secondly, we propose to achieve the synthesis together with the on-the-fly DFA construction such that the synthesis result can be obtained before constructing the whole DFA. The on-the-fly DFA construction is implemented using the SAT-based techniques for automata generation. We compared our new approach with the traditional ones on extensive LTLf synthesis benchmarks. Experimental results showed that the pre-processing techniques have a significant advantage on the synthesis performance in terms of scalability, and the on-the-fly synthesis is able to complement extant approaches on both realizable and unrealizable cases.

We introduce Circuit Structure Mutation, a simple but effective mutation-based testing approach, for testing hardware model checkers. The key idea is to mutate the existing And-Inverter Graph (AIG) circuit by manipulating the relations among the components in the graph while preserving the validity of the mutant. Based on Circuit Structure Mutation, we implemented a feedback-guided testing tool named Hammer. In our evaluation, Hammer shows its effectiveness on finding bugs, increasing test coverage, and finding performance optimization chances, which can help the hardware model checker developers improve the reliability and the performance of their tools.

Android, the most popular mobile system, offers a number of user-configurable system settings (e.g., network, location, and permission) for controlling devices and apps. Even popular, well-tested apps may fail to properly adapt their behaviors to diverse setting changes, thus frustrating their users. However, there exists no effort to systematically investigate such defects. To this end, we conduct the first empirical study to understand the characteristics of these setting-related defects (in short as "setting defects"), which reside in apps and are triggered by system setting changes. We devote substantial manual effort (over three person-months) to analyze 1,074 setting defects from 180 popular apps on GitHub. We investigate their impact, root causes, and consequences. We find that setting defects have a wide, diverse impact on apps' correctness, and the majority of these defects (≈70.7%) cause non-crash (logic) failures, and thus could not be automatically detected by existing app testing techniques due to the lack of strong test oracles. Motivated and guided by our study, we propose setting-wise metamorphic fuzzing, the first automated testing approach to effectively detect setting defects without explicit oracles. Our key insight is that an app's behavior should, in most cases, remain consistent if a given setting is changed and later properly restored, or exhibit expected differences if not restored. We realize our approach in SetDroid, an automated, end-to-end GUI testing tool, for detecting both crash and non-crash setting defects. SetDroid has been evaluated on 26 popular, open-source apps and detected 42 unique, previously unknown setting defects in 24 apps. To date, 33 have been confirmed and 21 fixed. We also apply SetDroid on five highly popular industrial apps, namely WeChat, QQMail, TikTok, CapCut, and AlipayHK, all of which each have billions of monthly active users. SetDroid successfully detects 17 previously unknown setting defects in these apps' latest releases, and all defects have been confirmed and fixed by the app vendors. The majority of SetDroid-detected defects (49 out of 59) cause non-crash failures, which could not be detected by existing testing tools (as our evaluation confirms). These results demonstrate SetDroid's strong effectiveness and practicality.

High-level representation-guided pixel denoising and adversarial training are independent solutions to enhance the robustness of CNNs against adversarial attacks by pre-processing input data and re-training models, respectively. Most recently, adversarial training techniques have been widely studied and improved while the pixel denoising-based method is getting less attractive. However, it is still questionable whether there exists a more advanced pixel denoising-based method and whether the combination of the two solutions benefits each other. To this end, we first comprehensively investigate two kinds of pixel denoising methods for adversarial robustness enhancement (i.e., existing additive-based and unexplored filtering-based methods) under the loss functions of image-level and semantic-level, respectively, showing that pixel-wise filtering can obtain much higher image quality (e.g., higher PSNR) as well as higher robustness (e.g., higher accuracy on adversarial examples) than existing pixel-wise additive-based method. However, we also observe that the robustness results of the filtering-based method rely on the perturbation amplitude of adversarial examples used for training. To address this problem, we propose predictive perturbation-aware & pixel-wise filtering, where dual-perturbation filtering and an uncertainty-aware fusion module are designed and employed to automatically perceive the perturbation amplitude during the training and testing process. The method is termed as AdvFilter. Moreover, we combine adversarial pixel denoising methods with three adversarial training-based methods, hinting that considering data and models jointly is able to achieve more robust CNNs. The experiments conduct on NeurIPS-2017DEV, SVHN and CIFAR10 datasets and show advantages over enhancing CNNs' robustness, high generalization to different models and noise levels.

Requirements-based testing is one of the most commonly used ways to ensure the correctness of software, especially for embedded control software in safety-critical domains such as spacecraft and railway systems. Many industrial standards such as the DO-333 and EN50128 also request rigorous requirements-based software testing. To test embedded control software effectively and efficiently, generating high-quality test cases automatically is extremely important. However, existing methods for generating test cases from requirements require intensive manual efforts and expertise. To address this problem, we proposed an automatic requirements-based software testing method for embedded control software. To obtain automatic test case generation and precise test oracles derivation, requirements specification should be precise and readable for the industrial practitioners. Therefore, we use the light-weight domain-specific formal description language, CASDL (Casco Accurate Specification Description Language) for the industrial practitioners to define software requirements into formal specifications at the first step. Based on the formal specification, we propose an algorithm to automatically generate test inputs that satisfy the MC/DC criteria suggested by typical industrial standards and precise test oracles can be derived by “running” the specification with such test inputs. To this end, we proposed an algorithm for simulating the formal specification to generate the test oracles, i.e., the expected outputs corresponding to the test inputs. To facilitate the application of this method in the industry, we have built a tool that can automatically perform the overall testing process. To validate and evaluate its effectiveness in real industrial projects, we have applied it in testing a real Automatic Train Protection (ATP) system provided by our industrial partner, the Casco Signal Co., Ltd (one of the largest railway control system companies in China). In the case study on ATP requirements, our approach generated test cases for 129 requirement items following MC/DC criteria and caught 40 inconsistencies between Casco’s requirements and implementation.

Android apps are GUI-based event-driven software and have become ubiquitous in recent years. Obviously, functional correctness is critical for an app’s success. However, in addition to crash bugs, non-crashing functional bugs (in short as “non-crashing bugs” in this work) like inadvertent function failures, silent user data lost and incorrect display information are prevalent, even in popular, well-tested apps. These non-crashing functional bugs are usually caused by program logic errors and manifest themselves on the graphic user interfaces (GUIs). In practice, such bugs pose significant challenges in effectively detecting them because (1) current practices heavily rely on expensive, small-scale manual validation ( the lack of automation ); and (2) modern fully automated testing has been limited to crash bugs ( the lack of test oracles ). This paper fills this gap by introducing independent view fuzzing , a novel, fully automated approach for detecting non-crashing functional bugs in Android apps. Inspired by metamorphic testing, our key insight is to leverage the commonly-held independent view property of Android apps to manufacture property-preserving mutant tests from a set of seed tests that validate certain app properties. The mutated tests help exercise the tested apps under additional, adverse conditions. Any property violations indicate likely functional bugs for further manual confirmation. We have realized our approach as an automated, end-to-end functional fuzzing tool, Genie. Given an app, (1) Genie automatically detects non-crashing bugs without requiring human-provided tests and oracles (thus fully automated ); and (2) the detected non-crashing bugs are diverse (thus general and not limited to specific functional properties ), which set Genie apart from prior work. We have evaluated Genie on 12 real-world Android apps and successfully uncovered 34 previously unknown non-crashing bugs in their latest releases — all have been confirmed, and 22 have already been fixed. Most of the detected bugs are nontrivial and have escaped developer (and user) testing for at least one year and affected many app releases, thus clearly demonstrating Genie’s effectiveness. According to our analysis, Genie achieves a reasonable true positive rate of 40.9%, while these 34 non-crashing bugs could not be detected by prior fully automated GUI testing tools (as our evaluation confirms). Thus, our work complements and enhances existing manual testing and fully automated testing for crash bugs.

In synthesis, assumptions are constraints on the environment that rule out certain environment behaviors. A key observation here is that even if we consider systems with LTLƒ goals on finite traces, environment assumptions need to be expressed over infinite traces, since accomplishing the agent goals may require an unbounded number of environment action. To solve synthesis with respect to finite-trace LTLƒ goals under infinite-trace assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLƒ and in LTL have the same worst-case complexity (both 2EXPTIME-complete), the algorithms available for LTL synthesis are much more difficult in practice than those for LTLƒ synthesis. In this work we show that in interesting cases we can avoid such a detour to LTL synthesis and keep the simplicity of LTLƒ synthesis. Specifically, we develop a BDD-based fixpoint-based technique for handling basic forms of fairness and of stability assumptions. We show, empirically, that this technique performs much better than standard LTL synthesis.

In this paper, we consider the automata construction problem for Linear Temporal Logic over finite traces, i.e., LTLf. We propose a SAT-based approach to translate an LTLf formula to both of its equivalent Nondeterministic and Deterministic Finite Automata (NFA and DFA). Notably, the generated automata are transition-based instead of state-based, which may potentially be a better fit for the applications that can be achieved on the fly, e.g. LTLf satisfiability checking and synthesis. Unlike extant approaches to translate LTLf formulas to the equivalent finite automata, which are indirect and have to introduce intermediate procedures, our methodology enables the direct construction from LTLf formulas to the finite automata. We evaluated our NFA construction together with other two LTLf -to-automata approaches implemented in the MONA and SPOT tools, which shows that the performance of our construction is comparable to the other two. We leave the comparison on the DFA construction in the future work.

Uncontrolled memory consumption is a kind of critical software security weaknesses. It can also become a security-critical vulnerability when attackers can take control of the input to consume a large amount of memory and launch a Denial-of-Service attack. However, detecting such vulnerability is challenging, as the state-of-the-art fuzzing techniques focus on the code coverage but not memory consumption. To this end, we propose a memory usage guided fuzzing technique, named MemLock, to generate the excessive memory consumption inputs and trigger uncontrolled memory consumption bugs. The fuzzing process is guided with memory consumption information so that our approach is general and does not require any domain knowledge. We perform a thorough evaluation for MemLock on 14 widely-used real-world programs. Our experiment results show that MemLock substantially outperforms the state-of-the-art fuzzing techniques, including AFL, AFLfast, PerfFuzz, FairFuzz, Angora and QSYM, in discovering memory consumption bugs. During the experiments, we discovered many previously unknown memory consumption bugs and received 15 new CVEs.

The All-SAT (All-SATisfiable) problem focuses on finding all satisfiable assignments of a given propositional formula, whose applications include model checking, automata construction, and logic minimization. A typical ALL-SAT solver is normally based on iteratively computing satisfiable assignments of the given formula. In this work, we introduce BASolver, a backbone-based All-SAT solver for propositional formulas. Compared to the existing approaches, BASolver generates shorter blocking clauses by removing backbone variables from the partial assignments and the blocking clauses. We compare BASolver with 4 existing ALL-SAT solvers, namely MBlocking, BC, BDD, and NBC. Experimental results indicate that although finding all the backbone variables consumes additional computing time, BASolver is still more efficient than the existing solvers because of the shorter blocking clauses and the backbone variables used in it.

At this moment, GAN-based image generation methods are still imperfect, whose upsampling design has limitations in leaving some certain artifact patterns in the synthesized image. Such artifact patterns can be easily exploited (by recent methods) for difference detection of real and GAN-synthesized images. However, the existing detection methods put much emphasis on the artifact patterns, which can become futile if such artifact patterns were reduced.

Formal methods are promising for modeling and analyzing system requirements. However, applying formal methods to large-scale industrial projects is a remaining challenge. The industrial engineers are suffering from the lack of automated engineering methodologies to effectively conduct precise requirement models, and rigorously validate and verify (V&V) the generated models. To tackle this challenge, in this paper, we present a systematic engineering approach, named Formal Requirement Engineering Platform in Aircraft (FREPA), for formal requirement modeling and V&V in the aerospace and aviation control domains. FREPA is an outcome of the seamless collaboration between the academy and industry over the last eight years. The main contributions of this paper include 1) an automated and systematic engineering approach FREPA to construct requirement models, validate and verify systems in the aerospace and aviation control domain, 2) a domain-specific modeling language AASRDL to describe the formal specification, and 3) a practical FREPA-based tool AeroReq which has been used by our industry partners. We have successfully adopted FREPA to seven real aerospace gesture control and two aviation engine control systems. The experimental results show that FREPA and the corresponding tool AeroReq significantly facilitate formal modeling and V&V in the industry. Moreover, we also discuss the experiences and lessons gained from using FREPA in aerospace and aviation projects.

Symbolic execution is an indispensable technique for software testing and program analysis. Path-explosion is one of the key challenges in symbolic execution. To relieve the challenge, this paper leverages the Q-learning algorithm to guide symbolic execution. Our guided symbolic execution technique focuses on generating a test input for triggering a particular statement in the program. In our approach, we first obtain the dominators with respect to a particular statement with static analysis. Such dominators are the statements that have to be visited before reaching the particular statement. Then we start the symbolic execution with the branch choice controlled by the policy in Q-learning. Only when symbolic execution encounters a dominator, it returns a positive reward to Q-learning. Otherwise, it will return a negative reward. And we update the Q-table in Q-learning accordingly. Our initial evaluation results indicate that in average more than 90% of exploration paths and instructions are reduced for reaching the target statement compared with the default search strategy in KLEE, which shows the promise of this work.

We present a SAT-based framework for LTLf (Linear Temporal Logic on Finite Traces) satisfiability checking. We use propositional SAT-solving techniques to construct a transition system for the input LTLf formula; satisfiability checking is then reduced to a path-search problem over this transition system. Furthermore, we introduce CDLSC (Conflict-Driven LTLf Satisfiability Checking), a novel algorithm that leverages information produced by propositional SAT solvers from both satisfiability and unsatisfiability results. Experimental evaluations show that CDLSC outperforms all other existing approaches for LTLf satisfiability checking, by demonstrating an approximate four-fold speed-up compared to the second-best solver.

We present Prema, a tool for Precise Requirement Editing, Modeling and Analysis. It can be used in various fields for describing precise requirements using formal notations and performing rigorous analysis. By parsing the requirements written in formal modeling language, Prema is able to get a model which aptly depicts the requirements. It also provides different rigorous verification and validation techniques to check whether the requirements meet users' expectation and find potential errors. We show that our tool can provide a unified environment for writing and verifying requirements without using tools that are not well inter-related. For experimental demonstration, we use the requirements of the automatic train protection (ATP) system of CASCO signal co. LTD., the largest railway signal control system manufacturer of China. The code of the tool cannot be released here because the project is commercially confidential. However, a demonstration video of the tool is available at https://youtu.be/BX0yv8pRMWs.

Software Model Checking (SMC) is a well-known automatic program verification technique and frequently adopted for checking safety-critical software. Thus, the reliability of SMC tools themselves (i.e., software model checkers) is critical. However, little work exists on validating software model checkers, an important problem that this paper tackles by introducing a practical, automated fuzzing technique. For its simplicity and generality, we focus on control-flow reachability (e.g., whether or how many times a branch is reached) and address two specific challenges for effective fuzzing: oracle and scalability. Given a deterministic program, we (1) leverage its concrete executions to synthesize valid branch reachability properties (thus solving the oracle problem) and (2) fuse such individual properties into a single safety property (thus improving the scalability of fuzzing and reducing manual inspection). We have realized our approach as the MCFuzz tool and applied it to extensively test three state-of-the-art C software model checkers, CPAchecker, CBMC, and SeaHorn. MCFuzz has found 62 unique bugs in all three model checkers -- 58 have been confirmed, and 20 have been fixed. We have further analyzed and categorized these bugs (which are diverse), and summarized several lessons for building reliable and robust model checkers. Our testing effort has been well-appreciated by the model checker developers, and also led to improved tool usability and documentation.

We present a new safety hardware model checker SimpleCAR that serves as a reference implementation for evaluating Complementary Approximate Reachability (CAR), a new SAT-based model checking framework inspired by classical reachability analysis. The tool gives a “bottom-line” performance measure for comparing future extensions to the framework. We demonstrate the performance of SimpleCAR on challenging benchmarks from the Hardware Model Checking Competition. Our experiments indicate that SimpleCAR is particularly suited for unsafety checking, or bug-finding ; it is able to solve 7 unsafe instances within 1 h that are not solvable by any other state-of-the-art techniques, including BMC and IC3/PDR , within 8 h. We also identify a bug (reports safe instead of unsafe) and 48 counterexample generation errors in the tools compared in our analysis.

Mobile apps have become ubiquitous. For app developers, it is a key priority to ensure their apps' correctness and reliability. However, many apps still suffer from occasional to frequent crashes, weakening their competitive edge. Large-scale, deep analyses of the characteristics of real-world app crashes can provide useful insights to guide developers, or help improve testing and analysis tools. However, such studies do not exist --- this paper fills this gap. Over a four-month long effort, we have collected 16,245 unique exception traces from 2,486 open-source Android apps, and observed that framework-specific exceptions account for the majority of these crashes. We then extensively investigated the 8,243 framework-specific exceptions (which took six person-months): (1) identifying their characteristics (e.g., manifestation locations, common fault categories), (2) evaluating their manifestation via state-of-the-art bug detection techniques, and (3) reviewing their fixes. Besides the insights they provide, these findings motivate and enable follow-up research on mobile apps, such as bug detection, fault localization and patch generation. In addition, to demonstrate the utility of our findings, we have optimized Stoat, a dynamic testing tool, and implemented ExLocator, an exception localization tool, for Android apps. Stoat is able to quickly uncover three previously-unknown, confirmed/fixed crashes in Gmail and Google+; ExLocator is capable of precisely locating the root causes of identified exceptions in real-world apps. Our substantial dataset is made publicly available to share with and benefit the community.

Android, the #1 mobile app framework, enforces the single-GUI-thread model, in which a single UI thread manages GUI rendering and event dispatching. Due to this model, it is vital to avoid blocking the UI thread for responsiveness. One common practice is to offload long-running tasks into async threads. To achieve this, Android provides various async programming constructs, and leaves evelopers themselves to obey the rules implied by the model. However, as our study reveals, more than 25% apps violate these rules and introduce hard-to-detect, fail-stop errors, which we term as aysnc programming errors (APEs). To this end, this paper introduces APEChecker, a technique to automatically and efficiently manifest APEs. The key idea is to characterize APEs as specific fault patterns, and synergistically combine static analysis and dynamic UI exploration to detect and verify such errors. Among the 40 real-world Android apps, APEChecker unveils and processes 61 APEs, of which 51 are confirmed (83.6% hit rate). Specifically, APEChecker detects 3X more APEs than the state-of-art testing tools (Monkey, Sapienz and Stoat), and reduces testing time from half an hour to a few minutes. On a specific type of APEs, APEChecker confirms 5X more errors than the data race detection tool, EventRacer, with very few false alarms.

Abstract We propose a novel algorithm for the satisfiability problem for linear temporal logic (LTL). Existing automata-based approaches first transform the LTL formula into a Büchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling to find a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We construct experiments on different pattern formulas, the experimental results show that our approach is superior to other solvers under automata-based framework.

Satisfiability checking for Linear Temporal Logic (LTL) is a fundamental step in checking for possible errors in LTL assertions. Extant LTL satisfiability checkers use a variety of different search procedures. In this paper, we propose an LTL satisfiability-checking framework that is accelerated by leveraging the state-of-the-art Boolean SAT techniques. Our approach is based on the variant of the obligation-set method, which we proposed in earlier work. We describe here heuristics that allow the use of a Boolean SAT solver to analyse the obligations for a given LTL formula. Moreover, we show the heuristics can be also utilized as the preprocessor for every LTL satisfiability solver. The experimental evaluation indicates that the new approach provides a significant performance improvement compared to its previous version, and becomes competitive with other state-of-the-art solvers.

Nowadays, software systems have been more and more complex, which causes great challenges to maintain the availability of the systems. Online failure prediction provides an effective approach to guaranteeing the validity of the systems. Most of the current technologies for online failure prediction require some prior knowledge, such as the model of the system or failure patterns. This paper proposes a new method based on fuzzy rules and time series analysis. Specifically, fuzzy rules are used to model the relationships among different variables, whereas univariate time series analysis is used to describe the evolution of each variable. Thus, for a dependent variable, we have two predicted values: one is from the time series model, and the other is computed from fuzzy rules with fuzzy inference. If the difference between the two values exceeds a threshold, then we declare that there would be a failure in some time period ahead. Different from the existing methods, the proposed method considers not only the evolutionary trend of each variable but also the relationships among different variables. Moreover, we do not need any prior knowledge such as system model or failure patterns. We use a railway transportation system as an example to illustrate our method.

Formal-verification techniques, such as model checking, are becoming popular in hardware design. SAT-based model checking techniques, such as IC3/PDR, have gained a significant success in the hardware industry. In this paper, we present a new framework for SAT-based safety model checking, named Complementary Approximate Reachability (CAR). CAR is based on standard reachability analysis, but instead of maintaining a single sequence of reachable-state sets, CAR maintains two sequences of over- and under-approximate reachable-state sets, checking safety and unsafety at the same time. To construct the two sequences, CAR uses standard Boolean-reasoning algorithms, based on satisfiability solving, one to find a satisfying cube of a satisfiable Boolean formula, and one to provide a minimal unsatisfiable core of an unsatisfiable Boolean formula. We applied CAR to 548 hardware model-checking instances, and compared its performance with IC3/PDR. Our results show that CAR is able to solve 42 instances that cannot be solved by IC3/PDR. When evaluated against a portfolio that includes IC3/PDR and other approaches, CAR is able to solve 21 instances that the other approaches cannot solve. We conclude that CAR should be considered as a valuable member of any algorithmic portfolio for safety model checking.

LTLf synthesis is the process of finding a strategy that satisfies a linear temporal specification over finite traces. An existing solution to this problem relies on a reduction to a DFA game. In this paper, we propose a symbolic framework for LTLf synthesis based on this technique, by performing the computation over a representation of the DFA as a boolean formula rather than as an explicit graph. This approach enables strategy generation by utilizing the mechanism of boolean synthesis. We implement this symbolic synthesis method in a tool called Syft, and demonstrate by experiments on scalable benchmarks that the symbolic approach scales better than the explicit one.

Mobile apps are ubiquitous, operate in complex environments and are developed under the time-to-market pressure. Ensuring their correctness and reliability thus becomes an important challenge. This paper introduces Stoat, a novel guided approach to perform stochastic model-based testing on Android apps. Stoat operates in two phases: (1) Given an app as input, it uses dynamic analysis enhanced by a weighted UI exploration strategy and static analysis to reverse engineer a stochastic model of the app's GUI interactions; and (2) it adapts Gibbs sampling to iteratively mutate/refine the stochastic model and guides test generation from the mutated models toward achieving high code and model coverage and exhibiting diverse sequences. During testing, system-level events are randomly injected to further enhance the testing effectiveness.

Backbone is the common part of each solution in a given propositional formula, which is a key to improving the performance of SAT solving and SAT-based applications, such as model checking and program analysis. In this paper, we propose an optimized approach that combines implication-driven (IDF), conflict-driven (CDF), and unique-driven (UDF) heuristics to improve backbone computing. IDF uses the particular binary structure of the form a ↔ b ∧ c to find more backbone literals. CDF comes from the observation that for a clause ¬a V b, if a is a backbone literal, then b is also a backbone literal. Besides CDF, we are also able to detect new non-backbone literals by UDF. A literal l is not a backbone literal, if there is no clause Φ ϵ Φ that is only satisfied by l. We implemented our approach in a tool named DUCIBone with the above optimizations (IDF+CDF+UDF), and conducted experiments on formulas used in previous work and SAT competitions (2015, 2016). Results demonstrate that DUCIBone solved 4% (507 formulas) more formulas than minibones (minibones-RLD, 490 formulas) does under its best configuration. Among 486 formulas solved by all tools (DUCIBone, minibones-RLD, minibonescb100), DUCIBone reduced 7% (35131 seconds) than minibones (37454 seconds). Experiments indicate that the advantage of DUCIBone is more obvious when the formulas are harder.

Branch-and-bound (B&B) approaches are widely investigated in resource constrained scheduling (RCS). However, due to the lack of approaches that can generate a tight schedule at the beginning of the search, B&B approaches usually start with a large initial search space, which makes the following search of an optimal schedule time-consuming. To address this problem, this paper proposes a parallel two-phase B&B approach that can drastically reduce the overall RCS time. This paper makes three major contributions: i) it proposes three partial-search heuristics that can quickly find a tight schedule to compact the initial search space; ii) it presents a two-phase search framework that supports the efficient parallel search of an optimal schedule; iii) it investigates various bound sharing and speculation techniques among collaborative tasks to further improve the parallel search performance at different search phases. The experimental results based on well-established benchmarks demonstrate the efficacy of our proposed approach.

Branch-and-bound approaches are promising in pruning fruitless search space during the resource constrained scheduling. However, such approaches only compare the estimated upper and lower bounds of an incomplete schedule to the length of the best feasible schedule at that iteration, which does not fully exploit the potential of the pruning during the search. Aiming to improve the performance of resource constrained scheduling, this paper proposes a parallel structure-aware pruning approach that can traverse the search space significantly faster than state-of-the-art branch-and-bound techniques. This paper makes three major contributions: i) it proposes an efficient pruning technique using the structural scheduling information of the obtained best feasible schedules; ii) it investigates how to perform parallel search to enable efficient multi-directional search and generation of effective fences by tuning the operation enumeration order; and iii) it presents a framework that supports the sharing of minimum upper-bound and fence information among different search tasks to enable efficient parallel structure-aware pruning. The experimental results demonstrate that our parallel pruning approach can drastically reduce the overall resource constrained scheduling time under a wide variety of resource constraints.

Pushdown systems with transductions (TrPDSs) are an extension of pushdown systems (PDSs) by associating each transition rule with a transduction, which allows to inspect and modify the stack content at each step of a transition rule. It was shown by Uezato and Minamide that TrPDSs can model PDSs with checkpoint and discrete-timed PDSs. Moreover, TrPDSs can be simulated by PDSs and the predecessor configurations pre^*(C) of a regular set C of configurations can be computed by a saturation procedure when the closure of the transductions in TrPDSs is finite. In this work, we comprehensively investigate the reachability problem of finite TrPDSs. We propose a novel saturation procedure to compute pre^*(C) for finite TrPDSs. Also, we introduce a saturation procedure to compute the successor configurations post^*(C) of a regular set C of configurations for finite TrPDSs. From these two saturation procedures, we present two efficient implementation algorithms to compute pre^*(C) and post^*(C). Finally, we show how the presence of transductions enables the modeling of Boolean programs with call-by-reference parameter passing. The TrPDS model has finite closure of transductions which results in model-checking approach for Boolean programs with call-by-reference parameter passing against safety properties.

This paper presents the formal development of the memory management module of a real time operating system. The interesting feature of this type of memory manager is that its dynamic memory allocation/reallocation mechanism behaves in O(1) (no loops). This brings a serious challenge on the "correct by construction" approach used to build this kind of system. This is due to the necessity to elaborate some delicate algorithms associated with complex data structures. To overcome this challenge, we follow the refinement principles of Event-B: we construct the proved executable code from some initial requirements. This development is interesting because some of the encountered problems are rather necessary to be studied in formal proved developments, among which are a modular encapsulation development, the design pattern of a linked list, and the usage of guarded events to develop pre-conditioned operations. It also gives us the opportunity to study a complex program construction in some general terms going beyond this specific example.

Data flow testing (DFT) focuses on the flow of data through a program. Despite its higher fault-detection ability over other structural testing techniques, practical DFT remains a significant challenge. This paper tackles this challenge by introducing a hybrid DFT framework: (1) The core of our framework is based on dynamic symbolic execution (DSE), enhanced with a novel guided path search to improve testing performance, and (2) we systematically cast the DFT problem as reach ability checking in software model checking to complement our DSE-based approach, yielding a practical hybrid DFT technique that combines the two approaches' respective strengths. Evaluated on both open source and industrial programs, our DSE-based approach improves DFT performance by 60~80% in terms of testing time compared with state-of-the-art search strategies, while our combined technique further reduces 40% testing time and improves data-flow coverage by 20% by eliminating infeasible test objectives. This combined approach also enables the cross-checking of each component for reliable and robust testing results.

Runtime verification is a dynamic verification technique widely used in practice. In this paper we revisit the runtime verification technique with formula progression, which verifies the execution trace step by step by progressing the desired property written in temporal logic. The previous work did not discuss explicitly the bound for the sizes of expanded formulas, while the successive invoking of formula progression is likely to cause divergence. In this paper, we present the convergent formula progression by introducing a novel fix-point reduction technique, and prove it guarantees the sizes of expanded formulas be always convergent. To the best of our knowledge, this is the first work discussing the convergence of formula progression. Furthermore, we implement the new runtime verification framework, and experiments show the efficiency of our proposed strategy.

We consider here Linear Temporal Logic (LTL) formulas interpreted over finite traces. We denote this logic by LTLf. The existing approach for LTLfsatisfiability checking is based on a reduction to standard LTL satisfiability checking. We describe here a novel direct approach to LTLfsatisfiability checking, where we take advantage of the difference in the semantics between LTL and LTLf. While LTL satisfiability checking requires finding a fair cycle in an appropriate transition system, here we need to search only for a finite trace. This enables us to introduce specialized heuristics, where we also exploit recent progress in Boolean SAT solving. We have implemented our approach in a prototype tool and experiments show that our approach outperforms existing approaches.

Google File System (GFS) is a distributed file system developed by Google for massive data-intensive applications which is widely used in industries nowadays. In this paper, we present a formal model of Google File System in terms of Communicating Sequential Processes (CSP#), which precisely describes the underlying read/write behaviours of GFS. Based on the achieved model some properties like deadlock-free, and consistency model of GFS can be analyzed and verified in the further work.

Linear Temporal Logic (LTL) is been widely used nowadays in verification and AI. Checking satisfiability of LTL formulas is a fundamental step in removing possible errors in LTL assertions. We present in this paper Aalta, a new LTL satisfiability checker, which supports satisfiability checking for LTL over both infinite and finite traces. Aalta leverages the power of modern SAT solvers. We have conducted a comprehensive comparison between Aalta and other LTL satisfiability checkers, and the experimental results show that Aalta is very competitive. The tool is available at www.lab205.org/aalta.

Bounded model checking (BMC, for short) is a successful application of SAT technique in model checking. In a broad sense, BMC encoding approaches could be categorised into the syntactic fashion and semantic fashion. In this paper, we present a new BMC encoding approach specially tailored for LTL model checking. The key observation is that syntactic encoding and semantic encoding respectively have the superiority in dealing with "next" operator and "until" operator in the specification. The proposed encoding could be implemented in an "on-the-fly" manner, and finally results in a linear scale blow-up. To justify it, the approach is experimentally evaluated by comparing with some of the best known existing encodings.

We propose a novel algorithm for the satisfiability problem for Linear Temporal Logic (LTL). Existing approaches first transform the LTL formula into a B"uchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling finding a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We report on a prototype implementation, showing that our approach significantly outperforms state-of-the-art tools.

This paper proposes a requirement analysis approach to periodic control systems that are widely used as one of the real time systems. By regulating the initial requirement documents with key words in natural language, we compile the regulated requirement documents into an intermediate model specified by SPARDL language with formal syntax and semantics. To make the requirement executable, a prototype generation technique is proposed to simulate the system behaviors. To analyze the dataflow relations among modules among the same mode or different modes, we introduce module-level and mode-level dataflow analysis techniques to help system engineers to uncover the potential affections on any two modules. The dataflow analysis techniques are useful especially for module reuse when a new version of the system is developed. We have applied the developed tool based on our approach to the Moon-Exploration Spacecraft Project from Beijing Institute of Control Engineering, and the preliminary experiments are encouraging. We have found both the ambiguity and the inconsistency cases in the requirement documents from the project.

SPARDL is a domain-specific modeling language for periodic control systems, which are widely used in embedded systems. Periodic control systems are usually driven by the given period. A periodic control system can be decomposed into different modes or sub-modes, and each mode represents a system state observed from outside. We believe that introducing static checking will extend the power of SPARDL. In this paper, we develop a type system for SPARDL. To make the contributions of this paper convincible and easy to understand, we apply the traditional approaches to construct the type system for SPARDL. An operational semantics is proposed as the basic explanation of SPARDL. And then some type safety theorems are proved under such semantics. We apply the type system to an industrial case from China Academy of Space Technology(CAST) to evaluate the effectiveness of our approach in practice, and then eight type errors are revealed.

In recent years, many Web service composition languages have been proposed. Web service choreography describes collaboration protocols of cooperating Web service participants from a global view. Web service orchestration describes collaboration of the Web services in predefined patterns based on local decision about their interactions with one another at the message/execution level. In this work, we present model-based methods to close the gap between the two views. Building on the strength of model checking techniques, Web service choreography and orchestration are verified against temporal properties or against each other (to show that they are consistent). Specialized optimization techniques are developed to handle large Web service models. Furthermore, we propose a method to mechanically synthesize a prototype Web service orchestration from choreography, by repairing the choreography if necessary and projecting relevant behaviors to each service provider.

The service choreography gives a global view on the collaboration among a collection of services involving multiple different organizations or independent processes. In this paper, a formal model for service choreography based on WS-CDL language is proposed. This model explores the key concepts related to choreography, such as passing channel, fault handling and finalization mechanisms. This study brings us the insights for the analysis, synthesis and verification of service choreography. For instance, the choreography synthesis is discussed based on our trace semantics achieved.

Test data generation is one of the important tasks during software testing. This paper proposes an approach to generating test cases automatically for the unit test of C programs with derived types including pointers, structures and arrays. Our approach combines symbolic execution and concrete execution. The approach captures operations on variables precisely by concrete execution, and thus it is capable of handling derived types. Benefited from symbolic execution, accessing variables as array index can be solved by a substitution strategy. The substitution strategy also translates a path constraint involving variables of derived type to the one containing only primitive variables. An implementation of this approach is integrated into our test case generation tool called CAUT. Experimental results show that our approach is effective to generate test data for derived types.

rCOS, the abbreviation of Refinement Calculus for Object Systems, is designed to present mathematical characterization of essential object-oriented concepts for an object-based language with a rich variety of features including subtypes, inheritance, type casting, dynamic binding and polymorphism. This paper represents an operational semantics for the rCOS language based on labeled transition systems. The result semantics shows the process of how the effects of an rCOS program are produced. It can be a secure guide for the implementation of the rCOS language, which is being carried out by our group. For the purpose of extending verifiability and functionality, a set of auxiliary language features is introduced to the rCOS language. Concurrent execution structure is designed to specify multi-threaded programs. Also the simulation is introduced to specify the observable behaviors of objects, and it can be regarded as the refinement relation defined in denotational domain to some extent.

In this paper, we give a bigraphical model for web services composition. We investigate how to represent scope-based compensation handing mechanism by means of Bigraphical Reactive Systems (13RSs for short), which have been proposed to provide a uniform way to model spatially distributed systems that both compute and communicate. The service composition language we focus on is WSBPEL, which is the standard of web service composition and orchestration. This bigraphical model can be regarded as a unifying semantics of BPEL-like languages with the key concepts related to compensation handling. The rationality of the model is discussed by investigating the relationship between BPEL language and BRSs. Based on the bigraphical model, the algebraic laws for BPEL are proved as well.

This paper presents an approach to validation and verification of the WSCDL specification. In order to validate whether the CDL document is well defined or not, we introduce OCL to precisely describe the constraints which was expressed by natural language, and design a simple validator to check the static properties of the CDL document. The validator is created based on a Java model and the Java model is generated according to the UML diagrams with OCL constraints which is used to describe CDL specification. To verify the dynamic properties of CDL document, we model the behavior of CDL document with Java, so that Java Pathfinder model checker can be applied to check the desired properties. The assert activity is introduced to the CDL specification for describing the logic properties, to facilitate the verification process. A case study is given and it shows that our approach is both effective and practical. Moreover, this approach can check almost every kinds of CDL document, even the documents including exception block or finalize block.

Different from traditional transactions, a compensable transaction relies on compensations to amend partial execution whenever an error occurs. The compensation is preserved on successful completion of its forward transaction for possibly later use. In this paper, we pay attention to the compositional structure of compensable transactions. Except for sequential and parallel compositions, other useful compositional constructs, such as speculative choice, exception handling, alternative forwarding and programmable compensation, are also investigated. All these constructs are not only devised to describe distinct business flow but also used to enhance the capability for dealing with errors, t-calculus is such a transactional language that involves a variety of primitives for composing compensable transactions in a wise way. We present a clear operational semantics for this language and the corresponding concept of bisimulation is defined, which is used to derive equational laws for compensable transactions.

The Web Services Choreography Description Language (WS-CDL) is a newly developed specification for Web services composition to describe the observable behavior across multiple participants from a global perspective. However, this specification does not provide a formal semantics, whose informal description can lead to ambiguous understanding and different implementations. Hence, it causes difficulties for the engineering community to analyze the business behavior and ensure the correctness. In this paper, we present the semantics of WS-CDL in terms of process algebra CSP which has great advantages in designing and verifying concurrent processes. Therefore, all the properties we want to check within a WS-CDL document can be verified automatically in the CSP framework correspondingly. In addition, the exception and compensation handling mechanism, an important concept of long running transactions, is demonstrated clearly through our formalization work.

Referring to the design and implementation of large service oriented systems, two different approaches, choreography and orchestration, need to be concerned and studied. Choreography is a specification protocol defining a global picture of the way services interact with each other. Whereas orchestration is a local view focusing on the behavior of a single service. A critical issue, the so called conformance problem, is to validate whether a specific orchestration can play as a participant whose observable behavior is required by a given choreography. In this paper, we introduce two languages for describing choreography and orchestration respectively. Based on the two languages, we give a definition of endpoint projection which is used for automatic generation of orchestrations. Therefore, conformance validation is reduced to verification of process refinement between two orchestrations. Further, we mention that not all choreography models can be locally implementable. In other words, some global models cannot be translated into sets of orchestrations satisfying the global behavioral rules. To ensure that a choreography model is locally implementable, some conditions are required to be satisfied. As a consequence of our work, the skeleton codes for service implementations can be automatically generated, on the other hand, the interoperability between collaborating services is guaranteed.

We propose a language CDL as a formal model of simplified WS-CDL. The operational semantics of CDL is given, and static validation and verification of choreographies is studied. Some properties of the proposed model are verified using the SPIN model-checker, which illustrates the potential usage and benefits of the formal model

In the paper, we proposed a language called BPEL0 with its formal semantics as the foundations of WSBPEL. In this paper, we follow the way Van der Aalst proposed on pattern analysis in workflow languages (2003), and present the patterns for BPEL0. Moreover, the expressiveness of BPEL0 is also embodied by means of putting these patterns in the program environment composed of other programming operators. Those properties about the patterns with its environment are captured by the algebraic laws, which can be proven in the framework of BPEL0 semantic domain.

Abstract Computer aided hardware/software partitioning is one of the key challenges in hardware/software co-design. This paper describes a new approach to hardware/software partitioning for a synchronous communication model including multiple hardware devices. We transform the partitioning into a reachability problem of timed automata. By means of an optimal reachability algorithm, the optimal solution can be obtained with limited resources in hardware. To relax the initial condition of the partitioning for optimization, two algorithms are designed to explore the dependency relations among processes in the sequential specification. Moreover, we propose a scheduling algorithm to improve the synchronous communication efficiency further after partitioning stage. Some experiments are conducted with the model checker UPPAAL to show our approach is both effective and efficient.

Thesaurus has been widely used in many applications, including information retrieval, natural language processing, and question answering. In this paper, we propose a novel approach to automatically constructing a domain-specific thesaurus from the Web using link structure information. The proposed approach is able to identify new terms and reflect the latest relationship between terms as the Web evolves. First, a set of high quality and representative websites of a specific domain is selected. After filtering out navigational links, link analysis is applied to each website to obtain its content structure. Finally, the thesaurus is constructed by merging the content structures of the selected websites. The experimental results on automatic query expansion based on our constructed thesaurus show 20% improvement in search precision compared to the baseline.