Abstract Dynamic Symbolic Execution (DSE) is an important method for the testing of programs. The major advantage of DSE is its path-by-path exploration of the program execution space. However, this often leads to the path explosion problem. To address this issue, a method of abstraction learning has been used. The key step here is the computation of an interpolant to represent the learned abstraction. In Test-Comp 2024, we use two different approaches of interpolant generation viz., Deletion Interpolation and Weakest Precondition Interpolation. The former is our more stable and mature system and briefly discussed in [8]. In this paper, we present the latter approach which is the heart of TracerX. In general, the Weakest Precondition (WP) is the ideal (most general) interpolant. However, WP is intractable to compute and is exponentially disjunctive. A major challenge is to obtain a conjunctive approximation of the WP. Therefore, we generate an approximation of the WP.

Validation of Android apps via testing is difficult owing to the presence of flaky tests. Due to non-deterministic execution environments, a sequence of events (a test) may lead to success or failure in unpredictable ways. In this work, we present an approach and tool FlakeScanner for detecting flaky tests through exploration of event orders. Our key observation is that for a test in a mobile app, there is a testing framework thread which creates the test events, a main User-Interface (UI) thread processing these events, and there may be several other background threads running asynchronously. For any event e whose execution involves potential non-determinism, we localize the earliest (latest) event after (before) which e must happen. We then efficiently explore the schedules between the upper/lower bound events while grouping events within a single statement, to find whether the test outcome is flaky. We also create a suite of subject programs called FlakyAppRepo (containing 33 widely-used Android projects) to study flaky tests in Android apps. Our experiments on the subject-suite FlakyAppRepo show FlakeScanner detected 45 out of 52 known flaky tests as well as 245 previously unknown flaky tests among 1444 tests.

Smart contracts are automated or self-enforcing contracts that can be used to exchange assets without having to place trust in third parties. Many commercial transactions use smart contracts due to their potential benefits in terms of secure peer-to-peer transactions independent of external parties. Experience shows that many commonly used smart contracts are vulnerable to serious malicious attacks, which may enable attackers to steal valuable assets of involving parties. There is, therefore, a need to apply analysis and automated repair techniques to detect and repair bugs in smart contracts before being deployed. In this work, we present the first general-purpose automated smart contract repair approach that is also gas-aware. Our repair method is search-based and searches among mutations of the buggy contract. Our method also considers the gas usage of the candidate patches by leveraging our novel notion of gas dominance relationship . We have made our smart contract repair tool SCRepair available open-source, for investigation by the wider community.

It is a challenge to ensure data integrity for cloud-based Internet of Things (IoT) applications because of the inherently dynamic nature of IoT data. The available frameworks of data integrity verification with public auditability cannot avoid the Third Party Auditors (TPAs). However, in a dynamic environment, such as the IoT, the reliability of the TPA-based frameworks is far from being satisfactory. In this paper, we propose a blockchain-based framework for Data Integrity Service. Under such framework, a more reliable data integrity verification can be provided for both the Data Owners and the Data Consumers, without relying on any Third Party Auditor (TPA). In this paper, the relevant protocols and a subsequent prototype system, which is implemented to evaluate the feasibility of our proposals, are presented. The performance evaluation of the implemented prototype system is conducted, and the test results are discussed. The work lays a foundation for our future work on dynamic data integrity verification in a fully decentralized environment.