Abstract Requirement defects are a major source of late-stage failures in automotive systems, yet rigorous validation is rarely applied during early development. While formal methods offer strong guarantees, their adoption at the requirements level is limited by high formalization cost and expertise barriers. We present an industry-oriented, shift-left verification approach that integrates Large Language Models (LLMs) with formal methods to enable requirements-level validation. Requirements are classified and decomposed by LLMs, translated into CSP system models and assertions, and refined through a CEGAR-inspired loop using the FDR4 model checker. Validation is decomposed into requirement–assertion pairs supported by natural-language back-translations and confidence scores, preserving expert control without manual formal modeling. Domain knowledge–based validation further leverages historical defect data to identify implicit requirement gaps. We evaluate the approach on three real-world automotive case studies. Results show high automation for small-to-medium systems (80–100% synthesis success for up to $$\sim 60$$ ∼ 60 requirements), effective expert validation guided by LLM confidence estimates, and 100% detection of known historical defects alongside 22 novel gaps. The workflow completes within 10–35 min per project at negligible cost ( $$<8$$ < 8 per project), with limited expert effort. Our results demonstrate that LLM+formal method hybridization can provide scalable, rigorous, and industrially viable requirements-level verification, supporting practical shift-left adoption in automotive systems.

While retrieval-augmented generation systems partially address the hallucination issues in large language models, it also introduces new vulnerabilities to knowledge corruption attacks. Adversaries exploit these vulnerabilities by poisoning documents provided by RAG system to manipulate LLM outputs. To counter this threat, we propose SecureCollaRAG, a Byzantine-tolerant collaborative RAG framework leveraging Multi-source Knowledge Validation Mechanism. Our approach enables agent system to securely verify document provenance through dynamic GNN-based credibility scoring, effectively preventing stealthy knowledge corruption attacks while preserving essential domain knowledge integrity. Through extensive evaluations and formal analysis, we demonstrate that SecureCollaRAG maintains robustness against attackers under non-IID data distributions.

Smart contracts are highly susceptible to manipulation attacks due to the leakage of sensitive information. Addressing manipulation vulnerabilities is particularly challenging because they stem from inherent data confidentiality issues rather than straightforward implementation bugs. To tackle this by preventing sensitive information leakage, we present PARTITIONGPT, the first LLM-driven approach that combines static analysis with the in-context learning capabilities of large language models (LLMs) to partition smart contracts into critical (privileged) and normal codebases, guided by a few annotated sensitive data variables. We evaluated PARTITIONGPT on 18 annotated smart contracts containing 99 sensitive functions. The results demonstrate that PARTITIONGPT successfully generatescompilable, andverifiedpartitions, achieving a precision of 80% while reducing more than 26% code compared to functionlevel partitioning approach. Furthermore, we evaluated PARTITIONGPT on nine real-world manipulation attacks that led to a total loss of 25 million dollars, PARTITIONGPT effectively prevents eight cases, highlighting its potential for broad applicability and the necessity for secure program partitioning during smart contract development to diminish manipulation vulnerabilities.

In the software development process, formal program specifications play a crucial role in various stages, including requirement analysis, software testing, and verification. However, manually crafting formal program specifications is rather difficult, making the job time-consuming and labor-intensive. Moreover, it is even more challenging to write specifications that correctly and comprehensively describe the semantics of complex programs. To reduce the burden on software developers, automated specification generation methods have emerged. However, existing methods usually rely on predefined templates or grammar, making them struggle to accurately describe the behavior and functionality of complex real-world programs. To tackle this challenge, we introduce SpecGen, a novel technique for formal program specification generation based on Large Language Models (LLMs). Our key insight is to overcome the limitations of existing methods by leveraging the code comprehension capability of LLMs. The process of SpecGen consists of two phases. The first phase employs a conversational approach that guides the LLM in generating appropriate specifications for a given program, aiming to utilize the ability of LLM to generate high-quality specifications. The second phase, designed for where the LLM fails to generate correct specifications, applies four mutation operators to the model-generated specifications and selects verifiable specifications from the mutated ones through a novel heuristic selection strategy by assigning different weights of variants in an efficient manner. We evaluate SpecGen on two datasets, including the SV-COMP Java category benchmark and a manually constructed dataset containing 120 programs. Experimental results demonstrate that SpecGen succeeds in generating verifiable specifications for 279 out of 385 programs, outperforming the existing LLM-based approaches and conventional specification generation tools like Houdini and Daikon. Further investigations on the quality of generated specifications indicate that SpecGen can comprehensively articulate the behaviors of the input program.

Binary Code Similarity Detection (BCSD), essential for binary-code related tasks like vulnerability detection, has attracted increasing attention in recent years. However, existing methods frequently fall short of achieving both high precision and recall at scale, and their results often lack interpretability due to the neglect of function context and reliance on purely similarity-driven outputs. Our key insights are twofold: 1) Binary functions are not self-contained; they depend on other code and data beyond their content to fulfill their functionalities. 2) Large language models (LLMs) excel not only at analyzing code but also at generating reasonable explanations. Motivated by these insights, we propose a general BCSD framework, Co2F uLL. We first systematically select stable and representative code and data features, along with their corresponding dependencies on the functions, to construct the function context. Then, by fusing function context with content similarities computed by the existing BCSD approach, we substantially narrow down the search space. Ultimately, we employ LLMs with a carefully designed prompt to verify the remaining candidates and produce clear, human-readable explanations. We conduct comprehensive experiments on a large function pool under varying compilation settings and after binary stripping. The results show that Co2F uLL based on HermesSim and DeepSeek-V3 achieves 80.5% precision and 94.4% recall, improving the baseline HermesSim by 142.5% and 42.2%, respectively, providing an accurate and interpretable solution for BCSD.

Phishing attacks in Web3 ecosystems are increasingly sophisticated, exploiting deceptive contract logic, malicious frontend scripts, and token approval patterns. We present DeepTx, a real-time transaction analysis system that detects such threats before user confirmation. DeepTx simulates pending transactions, extracts behavior, context, and UI features, and uses multiple large language models (LLMs) to reason about transaction intent. A consensus mechanism with self-reflection ensures robust and explainable decisions. Evaluated on our phishing dataset, DeepTx achieves high precision and recall (demo video: https://youtu.be/4OfK9KCEXUM).

Automated Program Repair (APR) plays a critical role in enhancing the quality and reliability of software systems. While substantial progress has been made in Java-based APR, largely facilitated by benchmarks like Defects4J, there remains a significant gap in research on C/C++ program repair, despite the widespread use of C/C++ and the prevalence of associated vulnerabilities. This gap is primarily due to the lack of high-quality, open-source benchmarks tailored for C/C++.To address this issue, we introduce Defects4C, a comprehensive and executable benchmark specifically designed for C/C++ program repair. Our dataset is constructed from real-world C/C++ repositories and includes a large collection of bug-relevant commits (9M in total), 248 high-quality buggy functions, and 102 vulnerable functions, all paired with test cases for reproduction. These resources enable rigorous evaluation of repair techniques and support the retraining of learning-based approaches for enhanced performance.Using Defects4C, we conduct a comprehensive empirical study evaluating the effectiveness of 24 state-of-the-art large language models (LLMs) in repairing C/C++ faults. Our findings offer valuable insights into the strengths and limitations of current LLM-based APR techniques in this domain, highlighting both the need for more robust methods and the critical role of Defects4C in advancing future research.

DeFi (Decentralized Finance) is one of the most important applications of today’s cryptocurrencies and smart contracts. It manages hundreds of billions in Total Value Locked (TVL) on-chain, yet it remains susceptible to common DeFi price manipulation attacks. Despite state-of-the-art (SOTA) systems like DeFiRanger and DeFort, we found that they are less effective to non-standard price models in custom DeFi protocols, which account for 44.2% of the 95 DeFi price manipulation attacks reported over the past three years.In this paper, we introduce the first LLM-based approach, DeFiScope, for detecting DeFi price manipulation attacks in both standard and custom price models. Our insight is that large language models (LLMs) have certain intelligence to abstract price calculation from smart contract source code and infer the trend of token price changes based on the extracted price models. To further strengthen LLMs in this aspect, we leverage Foundry to synthesize on-chain data and use it to fine-tune a DeFi price-specific LLM. Together with the high-level DeFi operations recovered from low-level transaction data, DeFiScope detects various DeFi price manipulations according to systematically mined patterns. Experimental results show that DeFiScope achieves a high recall of 80% on real-world attacks, a precision of 96% on suspicious transactions, and zero false alarms on benign transactions, significantly outperforming SOTA approaches. Moreover, we evaluate DeFiScope’s cost-effectiveness and demonstrate its practicality by helping our industry partner confirm 147 real-world price manipulation attacks, including discovering 81 previously unknown historical incidents.

The complexity of the Ethereum smart contracts makes it challenging to avoid security flaws. This problem led to many code analysis tools, which detect potential flaws and report them textually. However, the lack of context and visual information in these reports hinders the stakeholders' under-standing of the detailed information. Visualization can assist a developer in grasping such context, but current state-of-the-art visualization tools provide only fixed and limited visualization types. To this end, we present Contract Viz, based on the versatile platform Eclipse Trace Compass (TC), which supports various views and analyses in parallel. Our contribution enables TC to visualize Ethereum transaction traces using flame charts and gas consumption plots. This reveals information on account activities and provides insights into the correct or possibly flawed behaviors. GitHub repo-https://github.com/AisXiaolinlContractViz You Tube video-https://aisxiaolin.github.io/VideoDemo/

Smart contracts are computer programs running on blockchains to implement Decentralized Applications. The absence of contract specifications hinders routine tasks, such as contract understanding and testing. In this work, we propose a specification mining approach to infer contract specifications from past transaction histories. Our approach derives high-level behavioral automata of function invocations, accompanied by program invariants statistically inferred from the transaction histories. We implemented our approach as tool SMCON and evaluated it on eleven well-studied Azure benchmark smart contracts and six popular real-world DApp smart contracts. The experiments show that SMCON mines reasonably accurate specifications that can be used to enhance symbolic analysis of smart contracts achieving higher code coverage and up to 56 % speedup, and facilitate DApp developers in maintaining high-quality documentation and test suites.

Despite extensive in-house testing, bugs often escape to deployed software. Whenever a failure occurs in production software, it is desirable to collect as much execution information as possible so as to help developers reproduce, diagnose and fix the bug. To reconcile the tension between trace capability, runtime overhead, and trace scale, we propose continuous tail tracing for production use. Instead of capturing only crash stacks, we produce the complete sequence of function calls and returns. Importantly, to avoid the overwhelming stress to I/O, storage, and network transfer caused by the tremendous amount of trace data, we only retain the final segment of trace. To accomplish it, we design a novel trace decoder to support precise tail trace decoding, and an effective path-based instrumentation-site selection algorithm to reduce overhead. We implemented our approach as a tool called TailTracer on top of LLVM, and conducted the evaluations over the SPEC CPU 2017 benchmark suite, the open-source database system, and real-world bugs. The experimental results validate that TailTracer achieves low-overhead tail tracing, while providing more informative trace data than the baseline.

Smart contracts are computer programs running on blockchains to automate the transaction execution between users. The absence of contract specifications poses a real challenge to the correctness verification of smart contracts. Program invariants are properties that are always preserved throughout the execution, which characterize an important aspect of the program behaviors. In this paper, we propose a novel invariant generation framework, INVCON+, for Solidity smart contracts. INVCON+ extends the existing invariant detector, InvCon, to automatically produce verified contract invariants based on both dynamic inference and static verification. Unlike INVCON+, InvCon only produces likely invariants, which have a high probability to hold, yet are still not verified against the contract code. Particularly, INVCON+ is able to infer more expressive invariants that capture richer semantic relations of contract code. We evaluate INVCON+ on 361 ERC20 and 10 ERC721 real-world contracts, as well as common ERC20 vulnerability benchmarks. The experimental results indicate that INVCON+ efficiently produces high-quality invariant specifications, achieving a recall of 80%, which can be used to secure smart contracts from 17 types of common vulnerabilities.

Carbon neutrality has become a global priority, and high spatio-temporal resolution data on the column-average dry-air mole fraction carbon dioxide (XCO2) is essential for tracking progress and guiding policy adjustments. However, satellite-derived XCO2exhibits significant temporal and spatial gaps due to influences such as orbital dynamics and cloud cover. Additionally, the low spatial resolution of CarbonTracker (CT) is insufficient to meet the current demands for fine-scale monitoring. Current XCO2assessment methods often rely solely on single-pixel data, overlooking the spatio-temporal correlations. In this article, we introduce a deep learning-based spatio-temporal model (DSTM) that extracts features from multiple data sources related to atmospheric transport, carbon emissions, and carbon sinks, enabling fine-scale XCO2assessments. Additionally, XCO2data from the Orbiting Carbon Observatory-2 (OCO-2) and CT were fused at a 0.1° spatial resolution to generate training labels with broader coverage and more samples, serving as fitting labels. Our approach produced daily, full-coverage 0.1° resolution XCO2maps for China from 2015 to 2020, and analyzed changes in XCO2growth trends over this period. Numerical results show that our model outperforms traditional deep learning methods. Model validation using data from four ground-based observation sites of the Total Carbon Column Observing Network (TCCON) achieved an average R² of 0.86 and an RMSE of 2.67 ppm. The extraction and fusion of spatio-temporal features from multiple data sources provide a novel approach for reconstructing missing XCO2data.

Interoperability is a fundamental challenge for longenvisioned blockchain applications. A mainstream approach is using Trusted Execution Environment (TEE) to support interoperable off-chain execution. However, this incurs multiple TEE configured with non-trivial storage capabilities running on fragile concurrent processing environments, rendering current strategies based on TEE far from being practical. This paper aims to fill this gap and design a practical interoperability mechanism with simplified TEE as the underlying architecture. Specifically, we present IvyCross, a TEE-based framework that achieves lowcost, privacy-preserving, and race-free blockchain interoperability. IvyCross allows running arbitrary smart contracts across heterogeneous blockchains atop two distributed TEE-powered hosts. We design an incentive scheme based on smart contracts to stimulate the honest behavior of two hosts, bypassing the requirement of the number of TEE and large memory need. We examine the conditions to guarantee the uniqueness of Nash Equilibrium via Game Theory. Furthermore, an extended optimistic concurrency control protocol is designed to ensure the correctness of concurrent contracts execution. We formally prove the security of IvyCross in the Universal Composability (UC) framework and implement a prototype atop Bitcoin, Ethereum, and FISCO BOCS. Extensive experimental results on end-to-end performance and concurrency control demonstrate the efficiency and practicality of IvyCross.

Decentralized Finance (DeFi) is a prominent application of smart contracts, representing a novel financial paradigm in contrast to centralized finance. While DeFi applications are rapidly emerging on mainstream blockchain platforms, their quality varies greatly, presenting numerous challenges, particularly in terms of their governance mechanisms. In this paper, we present a comprehensive study of governance issues in DeFi applications. Initially, we collected 3,165 academic papers and numerous industry reports. After thorough screening, we selected 44 academic papers and 11 industry reports for detailed analysis. Drawing upon insights from industry reports and academic research articles, we develop a taxonomy to categorize these governance issues. We collect and build a dataset of 4,446 audit reports from seventeen Web3 security companies, categorizing their governance issues according to our constructed taxonomy. We conducted a thorough analysis of governance issues and identified vulnerabilities in the governance design and implementation, e.g., voting sybil attack and proposal front-running. Our statistical analysis indicates that a significant portion (35.48%) of governance-related issues is classified as severe. Within these, ownership-related problems constitute the largest share (65.38%). Despite DeFi governance being essential for the long-term success of DeFi projects, our data shows that both auditors and development teams have not fully grasped its significance. Based on audit reports, we also analyzed common vulnerabilities and issues in the governance domain. Our research identifies two primary categories of DeFi governance issues: technology-centric and human-centric. Technology-centric issues can be addressed through technology updates and iterations, whereas human-centric issues are influenced not only by the development team's technical skills but also by their understanding of DeFi governance. Data analysis reveals that design and implementation issues are frequently overlooked; although not directly associated with vulnerabilities, these issues can impact the equitable distribution of project benefits. Furthermore, our analysis of 104 projects’ tokenomics configurations, including 15 collected from DeFi platforms, uncovered 27 inconsistent configurations, with only two projects exhibiting no issues. This suggests that such issues are relatively common. We therefore advise project teams to ensure consistency between their tokenomics design and the actual code. Our study culminates in providing several key practical implications for various DeFi stakeholders, including developers, users, researchers, and regulators, aiming to deepen the understanding of DeFi governance issues and contribute to the robust growth of DeFi systems.

Sharding is a prevailing solution to enhance the scalability of current blockchain systems. However, the cross-shard commit protocols adopted in these systems to commit cross-shard transactions commonly incur multi-round shard-to-shard communication, leading to low performance. Furthermore, most solutions only focus on simple transfer transactions without supporting complex smart contracts, preventing sharding from widespread applications. In this paper, we propose LightCross, a novel sharding blockchain system that enables efficient execution of complex cross-shard smart contracts. First, LightCross offloads the execution of cross-shard transactions into off-chain executors equipped with the TEE hardware, which can accommodate execution for arbitrarily complex contracts. Second, we design a lightweight cross-shard commit protocol to commit cross-shard transactions without multi-round shard-to-shard communication between shards. Last, LightCross lowers the cross-shard transaction ratio by dynamically changing the distribution of contracts according to historical transactions. We implemented the LightCross prototype based on the FISCO-BCOS project and evaluated it in real-world blockchain environments, showing that LightCross can achieve 2.6× more throughput than state-of-the-art sharding systems.

Automated Program Repair (APR) presents the promising momentum of releasing developers from the burden of manual debugging tasks by automatically fixing bugs in various ways. Recent advances in deep learning inspire many works in employing deep learning techniques to fixing buggy programs. However, several challenges remain unaddressed: (1) state-of-the-art fault localization techniques often require additional artifacts, such as bug-triggering test cases or bug reports. These artifacts are not always available in the early development phases; (2) Sequence-to-Sequence model-based APR often requires additional contexts with high quality to generate patches. Yet, it is challenging to identify high-quality contexts that are not common in programs.In this paper, with the redundancy assumption in program repair, we propose a dual deep learning-based APR tool, RATCHET, for localizing (RATCHET-FL) and repairing (Ratchet-PG) buggy programs. Ratchet-FL localizes buggy statements based on the feature learned by a simple BiLSTM model from the code, without any bug-triggering test cases or bug reports. Ratchet-PG relies on our proposed retrieval augmented transformer to learn the historical patches and generate patches for fixing bugs. We evaluate the effectiveness of Ratchet with in-the-lab DrRepair dataset and in-the-wild dataset Ratchet-DS (curated in this work). Our experimental results show that Ratchet outperforms state-of-the-art deep learning approaches on fault localization with 39.8-96.4% accuracy and patch generation with 18.4-46.4% repair accuracy.

Smart contracts, self-executing programs on the blockchain, facilitate reliable value exchanges without centralized oversight. Despite the recent focus on dynamic analysis of their transaction histories in both industry and academia, no open-source tool currently offers comprehensive tracking of complete transaction information to extract user-desired data such as invariant-related data. This paper introduces OpenTracer, designed to address this gap. OpenTracer guarantees comprehensive tracking of every execution step, providing complete transaction information. OpenTracer has been employed to analyze 350,800 Ethereum transactions, successfully inferring 23 different types of invariant from predefined templates. The tool is fully open-sourced, serving as a valuable resource for developers and researchers aiming to extract or validate new invariants from transaction traces. A demonstration video of OpenTracer is available at https://youtu.be/vTdmjWdYd30. The source code of OpenTracer is available at https://github.com/jeffchen006/OpenTracer.

As various optimizations being proposed recently, the performance of blockchains is no longer limited by the consensus protocols, successfully scaling to thousands of transactions per second. To further improve blockchains' throughput, exploiting the parallelism in smart contract executions becomes a clear solution to resolve the new performance bottleneck. The existing techniques perform concurrency control on smart contract transactions based on pre-determined read/write sets, which can hardly be calculated precisely. As a result, many parallelization opportunities are missed in order to maintain the correctness of transaction executions. In this paper, we propose a novel execution scheduling framework, DMVCC, to further increase the parallelism in smart contract executions, via more fine-grained control on state accesses. DMVCC improves over existing techniques with two key features: (1) write versioning, eliminating the write-write conflicts between transactions, and (2) early-write visibility, enabling other transactions to read the writes from a transaction earlier, before it being committed. We integrated DMVCC into the Ethereum Virtual Machine, to evaluate its performance in real-world blockchain environments. The experimental results show that DMVCC doubles the parallel speedup achievable to a 20 x overall speedup, compared with the serial execution baseline, approaching the theoretical optimum.

Numerous program slicing approaches aim to help developers troubleshoot regression failures - one of the most time-consuming development tasks. The main idea behind these approaches is to identify a subset of interdependent program statements relevant to the failure, minimizing the amount of code developers need to inspect. Accuracy and reduction rate achieved by slicing are the key considerations toward their applicability in practice: inspecting only the statements in a slice should be faster and more efficient than inspecting the code in full. In this paper, we report on our experiment applying one of the most recent and accurate slicing approaches, dual slicing, to the task of troubleshooting regression failures. As subjects, we use projects from the popular Defects4J benchmark and a systematically-collected set of eight large, open-source client-library project pairs with at least one library upgrade failure, which we refer to as LibRench. The results of our experiments show that the produced slices, while effective in reducing the scope of manual inspection, are still very large to be comfortably analyzed by a human. When inspecting these slices, we observe that most statements in a slice deal with the propagation of information between changed code blocks; these statements are essential for obtaining the necessary context for the changes but are not responsible for the failure directly. Motivated by this insight, we propose a novel approach, implemented in a tool named INPRESS, for further reducing the size of a slice by accurately identifying and summarizing the propagation-related code blocks. Our evaluation of INPRESS shows that it is able to produce slices that are 76% shorter than the original ones (207 vs. 2,007 execution statements, on average), thus, reducing the amount of information developers need to inspect without losing the necessary contextual information.

Modern software systems heavily rely on external libraries developed by third-parties to ensure efficient development. However, frequent library upgrades can lead to compatibility issues between the libraries and their client systems. In this paper, we introduce Compsuite, a dataset that includes 123 real-world Java client-library pairs where upgrading the library causes an incompatibility issue in the corresponding client. Each incompatibility issue in Compsuite is associated with a test case authored by the developers, which can be used to reproduce the issue. The dataset also provides a command-line interface that simplifies the execution and validation of each issue. With this infrastructure, users can perform an inspection of any incompatibility issue with the push of a button, or reproduce an issue step-by-step for a more detailed investigation. We make Compsuite publicly available to promote open science. We believe that various software analysis techniques, such as compatibility checking, debugging, and regression test selection, can benefit from Compsuite. The demonstration video of Compsuite is available at https://www.youtube.com/watch?v=7DQGsGs_65s.

Detecting non-termination is crucial for ensuring program correctness and security, such as preventing denial-of-service attacks. While termination analysis has been studied for many years, existing methods have limited scalability and are only effective on small programs. To address this issue, we propose a practical termination checking technique, called EndWatch, for detecting non-termination caused by infinite loops through testing. Specifically, we introduce two methods to generate non-termination oracles based on checking state revisits, i.e., if the program returns to a previously visited state at the same program location, it does not terminate. The non-termination oracles can be incorporated into testing tools (e.g., AFL used in this paper) to detect non-termination in large programs. For linear loops, we perform symbolic execution on individual loops to infer State Revisit Conditions (SRCs) and instrument SRCs into target loops. For non-linear loops, we instrument target loops for checking concrete state revisits during execution. We evaluated EndWatch on standard benchmarks with small-sized programs and real-world projects with large-sized programs. The evaluation results show that EndWatch is more effective than the state-of-the-art tools on standard benchmarks (detecting 87% of non-terminating programs while the best baseline detects only 67%), and useful in detecting non-termination in real-world projects (detecting 90% of known non-termination CVEs and 4 unknown bugs).

Intentions are fundamental in software engineering, but they are typically only implicitly considered through different abstractions, such as requirements, use cases, features, or issues. Specifically, software engineers develop and evolve (i.e., change) a software system based on such abstractions of a stakeholder’s intention—something a stakeholder wants the system to be able to do. Unfortunately, existing abstractions are (inherently) limited when it comes to representing stakeholder intentions and are mostly used for documenting only. So, whether a change in a system fulfills its underlying intention (and only this one) is an essential problem in practice that motivates many research areas (e.g., testing to ensure intended behavior, untangling intentions in commits). We argue that none of the existing abstractions is ideal for capturing intentions and controlling software evolution, which is why intentions are often vague and must be recovered, untangled, or understood in retrospect. In this paper, we reflect on the role of intentions (represented by changes) in software engineering and sketch how improving their management may support developers. Particularly, we argue that continuously managing and controlling intentions as well as their fulfillment has the potential to improve the reasoning about which stakeholder requests have been addressed, avoid misunderstandings, and prevent expensive retrospective analyses. To guide future research for achieving such benefits for researchers and practitioners, we discuss the relationships between different abstractions and intentions, and propose steps towards managing intentions.

Modern software systems are complex, and they heavily rely on external libraries developed by different teams and organizations. Such systems suffer from higher instability due to incompatibility issues caused by library upgrades. In this article, we address the problem by investigating the impact of a library upgrade on the behaviors of its clients. We developed CompCheck , an automated upgrade compatibility checking framework that generates incompatibility-revealing tests based on previous examples. CompCheck first establishes an offline knowledge base of incompatibility issues by mining from open source projects and their upgrades. It then discovers incompatibilities for a specific client project, by searching for similar library usages in the knowledge base and generating tests to reveal the problems. We evaluated CompCheck on 202 call sites of 37 open source projects and the results show that CompCheck successfully revealed incompatibility issues on 76 call sites, 72.7% and 94.9% more than two existing techniques, confirming CompCheck ’s applicability and effectiveness.

Over the past few years, SMT string solvers have found their applications in an increasing number of domains, such as program analyses in mobile and Web applications, which require the ability to reason about string values. A series of research has been carried out to find quality issues of string solvers in terms of its correctness and performance. Yet, none of them has considered the performance regressions happening across multiple versions of a string solver. To fill this gap, in this paper, we focus on solver performance regressions (SPRs), i.e., unintended slowdowns introduced during the evolution of string solvers. To this end, we developSPRFinderto not only generate test cases demonstrating SPRs, but also localize the probable causes of them, in terms of commits. We evaluated the effectiveness ofSPRFinderon three state-of-the-art string solvers, i.e., Z3Seq, Z3Str3, and CVC4. The results demonstrate thatSPRFinderis effective in generating SPR-inducing test cases and also able to accurately locate the responsible commits. Specifically, the average running time on the target versions is 13.2× slower than that of the reference versions. Besides, we also conducted the first empirical study to peek into the characteristics of SPRs, including the impact of random seed configuration for SPR detection, understanding the root causes of SPRs, and characterizing the regression test cases through case studies. Finally, we highlight that 149 unique SPR-inducing commits were discovered in total bySPRFinder, and 27of them have been confirmed by the corresponding developers.

Smart contracts deployed on permissionless blockchains, such as Ethereum, are accessible to any user in a trustless environment. Therefore, most smart contract applications implement access control policies to protect their valuable assets from unauthorized accesses. A difficulty in validating the conformance to such policies, i.e., whether the contract implementation adheres to the expected behaviors, is the lack of policy specifications. In this paper, we mine past transactions of a contract to recover a likely access control model, which can then be checked against various information flow policies and identify potential bugs related to user permissions. We implement our role mining and security policy validation in tool SPCon. The experimental evaluation on labeled smart contract role mining benchmark demonstrates that SPCon effectively mines more accurate user roles compared to the state-of-the-art role mining tools. Moreover, the experimental evaluation on real-world smart contract benchmark and access control CVEs indicates SPCon effectively detects potential permission bugs while having better scalability and lower false-positive rate compared to the state-of-the-art security tools, finding 11 previously unknown bugs and detecting six CVEs that no other tool can find.

Smart contracts are gaining popularity as a means to support transparent, traceable, and self-executing decentralized applications, which enable the exchange of value in a trustless environment. Developers of smart contracts rely on various libraries, such as OpenZeppelin for Solidity contracts, to improve application quality and reduce development costs. The API documentations of these libraries are important sources of information for developers who are unfamiliar with the APIs. Yet, maintaining high-quality documentations is non-trivial, and errors in documentations may place barriers for developers to learn the correct usages of APIs. In this paper, we propose a technique, DocCon, to detect inconsistencies between documentations and the corresponding code for Solidity smart contract libraries. Our fact-based approach allows inconsistencies of different severity levels to be queried, from a database containing precomputed facts about the API code and documentations. DocCon successfully detected high-priority API documentation errors in popular smart contract libraries, including mismatching parameters, missing requirements, outdated descriptions, etc. Our experiment result shows that DocCon achieves good precision and is applicable to different libraries: 29 and 22 out of our reported 40 errors have been confirmed and fixed by library developers so far.

Smart contracts are self-executing computer programs deployed on blockchain to enable trustworthy exchange of value without the need of a central authority. With the absence of documentation and specifications, routine tasks such as program understanding, maintenance, verification, and validation, remain challenging for smart contracts. In this paper, we propose a dynamic invariant detection tool, InvCon, for Ethereum smart contracts to mitigate this issue. The detected invariants can be used to not only support the reverse engineering of contract specifications, but also enable standard-compliance checking for contract implementations. InvCon provides a Web-based interface and a demonstration video of it is available at: https://youtu.be/Y1QBHjDSMYk.

Third-party libraries (TPLs) are frequently reused in software to reduce development cost and the time to market. However, external library dependencies may introduce vulnerabilities into host applications. The issue of library dependency has received considerable critical attention. Many package managers, such as Maven, Pip, and NPM, are proposed to manage TPLs. Moreover, a significant amount of effort has been put into studying dependencies in language ecosystems like Java, Python, and JavaScript except C/C++. Due to the lack of a unified package manager for C/C++, existing research has only few understanding of TPL dependencies in the C/C++ ecosystem, especially at large scale.

Programming errors enable security attacks on smart contracts, which are used to manage large sums of financial assets. Automated program repair (APR) techniques aim to reduce developers’ burden of manually fixing bugs by automatically generating patches for a given issue. Existing APR tools for smart contracts focus on mitigating typical smart contract vulnerabilities rather than violations of functional specification. However, in decentralized financial (DeFi) smart contracts, the inconsistency between intended behavior and implementation translates into the deviation from the underlying financial model, resulting in monetary losses for the application and its users. In this work, we propose DeFinery—a technique for automated repair of a smart contract that does not satisfy a user-defined correctness property. To explore a larger set of diverse patches while providing formal correctness guarantees w.r.t. the intended behavior, we combine search-based patch generation with semantic analysis of an original program for inferring its specification. Our experiments in repairing 9 real-world and benchmark smart contracts prove that DeFinery efficiently generates high-quality patches that cannot be found by other existing tools.

Despite achieving superior performance in human-level control problems, unlike humans, deep reinforcement learning (DRL) lacks high-order intelligence (e.g., logic deduction and reuse), thus it behaves ineffectively than humans regarding learning and generalization in complex problems. Previous works attempt to directly synthesize a white-box logic program as the DRL policy, manifesting logic-driven behaviors. However, most synthesis methods are built on imperative or declarative programming, and each has a distinct limitation, respectively. The former ignores the cause-effect logic during synthesis, resulting in low generalizability across tasks. The latter is strictly proof-based, thus failing to synthesize programs with complex hierarchical logic. In this paper, we combine the above two paradigms together and propose a novel Generalizable Logic Synthesis (GALOIS) framework to synthesize hierarchical and strict cause-effect logic programs. GALOIS leverages the program sketch and defines a new sketch-based hybrid program language for guiding the synthesis. Based on that, GALOIS proposes a sketch-based program synthesis method to automatically generate white-box programs with generalizable and interpretable cause-effect logic. Extensive evaluations on various decision-making tasks with complex logic demonstrate the superiority of GALOIS over mainstream baselines regarding the asymptotic performance, generalizability, and great knowledge reusability across different environments.

Most of the existing smart contract symbolic execution tools perform analysis on bytecode, which loses high-level semantic information presented in source code. This makes interactive analysis tasks—such as visualization and debugging—extremely challenging, and significantly limits the tool usability. In this paper, we present SolSEE, a source-level symbolic execution engine for Solidity smart contracts. We describe the design of SolSEE, highlight its key features, and demonstrate its usages through a Web-based user interface. SolSEE demonstrates advantages over other existing source-level analysis tools in the advanced Solidity language features it supports and analysis flexibility. A demonstration video is available at: https://sites.google.com/view/solsee/.

Termination is a crucial program property. Non-termination bugs can be subtle to detect and may remain hidden for long before they take effect. Many real-world programs still suffer from vast consequences (e.g., no response) caused by non-termination bugs. As a classic problem, termination proving has been studied for many years. Many termination checking tools and techniques have been developed and demonstrated effectiveness on existing well-established benchmarks. However, the capability of these tools in finding practical non-termination bugs has yet to be tested on real-world projects. To fill in this gap, in this paper, we conducted the first large-scale empirical study of non-termination bugs in real-world OSS projects. Specifically, we first devoted substantial manual efforts in collecting and analyzing 445 non-termination bugs from 3,142 GitHub commits and provided a systematic classifi-cation of the bugs based on their root causes. We constructed a new benchmark set characterizing the real-world bugs with simplified programs, including a non-termination dataset with 56 real and reproducible non-termination bugs and a termination dataset with 58 fixed programs. With the constructed benchmark, we evaluated five state-of-the-art termination analysis tools. The results show that the capabilities of the tested tools to make correct verdicts have obviously dropped compared with the existing benchmarks. Meanwhile, we identified the challenges and limitations that these tools face by analyzing the root causes of their unhandled bugs. Fi-nally, we summarized the challenges and future research directions for detecting non-termination bugs in real-world projects.

Despite the high stakes involved in smart contracts, they are often developed in an undisciplined manner, leaving the security and reliability of blockchain transactions at risk. In this article, we introduce ContraMaster—an oracle-supported dynamic exploit generation framework for smart contracts. Existing approaches mutate only single transactions; ContraMaster exceeds these by mutating the transaction sequences. ContraMaster uses data-flow, control-flow, and the dynamic contract state to guide its mutations. It then monitors the executions of target contract programs, and validates the results against a general-purpose semantic test oracle to discover vulnerabilities. Being a dynamic technique, it guarantees that each discovered vulnerability is a violation of the test oracle and is able to generate the attack script to exploit this vulnerability. In contrast to rule-based approaches, ContraMaster has not shown any false positives, and it easily generalizes to unknown types of vulnerabilities (e.g., logic errors). We evaluate ContraMaster on 218 vulnerable smart contracts. The experimental results confirm its practical applicability and advantages over the state-of-the-art techniques, and also reveal three new types of attacks.

Managing large and fast-evolving software systems can be a challenging task. Numerous solutions have been developed to assist in this process, enhancing software quality and reducing development costs. These techniques—e.g., regression test selection and change impact analysis—are often built as standalone tools, unable to share or reuse information among them. In this paper, we introduce a software evolution management engine, EvoMe, to streamline and simplify the development of such tools, allowing them to be easily prototyped using an intuitive query language and quickly deployed for different types of projects. EvoMe is based on differential factbase, a uniform exchangeable representation of evolving software artifacts, and can be accessed directly through a Web interface. We demonstrate the usage and key features of EvoMe on real open-source software projects. The demonstration video can be found at: http://youtu.be/6mMgu6rfnjY.

Equivalence checking techniques help establish whether two versions of a program exhibit the same behavior. The majority of popular techniques for formally proving/refuting equivalence are evaluated on small and simplistic benchmarks, omitting "difficult" programming constructs, such as non-linear arithmetic, loops, floating-point arithmetic, and string and array manipulation. This hinders efficient evaluation of these techniques and the ability to establish their practical applicability in real scenarios. This paper addresses this gap by contributing EqBench - the largest and most comprehensive benchmark for equivalence checking analysis, which contains 147 equivalent and 125 non-equivalent cases, in both C and Java languages. We believe EqBench can facilitate a more realistic evaluation of equivalence checking techniques, assessing their individual strength and weaknesses. EqBench is publicly available at: https://osf.io/93s5b/.

Numerous tools and techniques have been developed to extract and analyze information from software development artifacts. Yet, there is a lack of effective method to process, store, and exchange information among different analyses. In this paper, we propose differential factbase, a uniform exchangeable representation supporting efficient querying and manipulation, based on the existing concept of program facts. We consider program changes as first-class objects, which establish links between intra-version facts of single program snapshots and provide insights on how certain artifacts evolve over time via inter-version facts. We implement a series of differential fact extractors supporting different programming languages and platforms, and demonstrate with usage scenarios the benefits of adopting differential facts in supporting software evolution management.

Existing coverage-based fuzzers usually use the individual control flow graph (CFG) edge coverage to guide the fuzzing process, which has shown great potential in finding vulnerabilities. However, CFG edge coverage is not effective in discovering vulnerabilities such as use-after-free (UaF). This is because, to trigger UaF vulnerabilities, one needs not only to cover individual edges, but also to traverse some (long) sequence of edges in a particular order, which is challenging for existing fuzzers. To this end, we propose to model UaF vulnerabilities as typestate properties, and develop a typestate-guided fuzzer, named UAFL, for discovering vulnerabilities violating typestate properties. Given a typestate property, we first perform a static typestate analysis to find operation sequences potentially violating the property. Our fuzzing process is then guided by the operation sequences in order to progressively generate test cases triggering property violations. In addition, we also employ an information flow analysis to improve the efficiency of the fuzzing process. We have performed a thorough evaluation of UAFL on 14 widely-used real-world programs. The experiment results show that UAFL substantially outperforms the state-of-the-art fuzzers, including AFL, AFLFast, FairFuzz, MOpt, Angora and QSYM, in terms of the time taken to discover vulnerabilities. We have discovered 10 previously unknown vulnerabilities, and received 5 new CVEs.

Semantic history slicing addresses the problem of identifying changes related to a particular high-level functionality from the software change histories. Existing solutions are either imprecise, resulting in larger-than-necessary history slices, or inefficient, taking a long time to execute. In this paper, we develop a generalized history slicing framework, named GenSlice, which overcomes the aforementioned limitations. GenSlice abstracts existing history slicing techniques and change history management operations (such as splitting commits into fine-grained changes) as history transformation operators, making it possible to apply them sequentially in various orders. We study and prove properties of various orders of operators and devise a systematic approach for efficiently producing history slices that are optimal for practical purposes. We report on an empirical evaluation of our framework, demonstrating its effectiveness on a set of real-world case studies.

State-of-the-art deep learning (DL) systems are vulnerable to adversarial examples, which hinders their potential adoption in safety-and security-critical scenarios. While some recent progress has been made in analyzing the robustness of feed-forward neural networks, the robustness analysis for stateful DL systems, such as recurrent neural networks (RNNs), still remains largely uncharted. In this paper, we propose Marble, a model-based approach for quantitative robustness analysis of real-world RNN-based DL systems. Marble builds a probabilistic model to compactly characterize the robustness of RNNs through abstraction. Furthermore, we propose an iterative refinement algorithm to derive a precise abstraction, which enables accurate quantification of the robustness measurement. We evaluate the effectiveness of Marble on both LSTM and GRU models trained separately with three popular natural language datasets. The results demonstrate that (1) our refinement algorithm is more efficient in deriving an accurate abstraction than the random strategy, and (2) Marble enables quantitative robustness analysis, in rendering better efficiency, accuracy, and scalability than the state-of-the-art techniques.

Deep learning (DL) has been applied widely, and the quality of DL system becomes crucial, especially for safety-critical applications. Existing work mainly focuses on the quality analysis of DL models, but lacks attention to the underlying frameworks on which all DL models depend. In this work, we propose Audee, a novel approach for testing DL frameworks and localizing bugs. Audee adopts a search-based approach and implements three different mutation strategies to generate diverse test cases by exploring combinations of model structures, parameters, weights and inputs. Audee is able to detect three types of bugs: logical bugs, crashes and Not-a-Number (NaN) errors. In particular, for logical bugs, Audee adopts a cross-reference check to detect behavioural inconsistencies across multiple frameworks (e.g., TensorFlow and PyTorch), which may indicate potential bugs in their implementations. For NaN errors, Audee adopts a heuristic-based approach to generate DNNs that tend to output outliers (i.e., too large or small values), and these values are likely to produce NaN. Furthermore, Audee leverages a causal-testing based technique to localize layers as well as parameters that cause inconsistencies or bugs. To evaluate the effectiveness of our approach, we applied Audee on testing four DL frameworks, i.e., TensorFlow, PyTorch, CNTK, and Theano. We generate a large number of DNNs which cover 25 widely-used APIs in the four frameworks. The results demonstrate that Audee is effective in detecting inconsistencies, crashes and NaN errors. In total, 26 unique unknown bugs were discovered, and 7 of them have already been confirmed or fixed by the developers.

Equivalence checking techniques help establish whether two versions of a program exhibit the same behavior. The majority of popular techniques for formally proving/refuting equivalence relies on symbolic execution – a static analysis approach that reasons about program behaviors in terms of symbolic input variables. Yet, symbolic execution is difficult to scale in practice due to complex programming constructs, such as loops and non-linear arithmetic.

Smart contracts are computer programs allowing users to define and execute transactions automatically on top of the blockchain platform. Many of such smart contracts can be viewed as games. A game-like contract accepts inputs from multiple participants, and upon ending, automatically derives an outcome while distributing assets according to some predefined rules. Without clear understanding of the game rules, participants may suffer from fraudulent advertisements and financial losses. In this paper, we present a framework to perform (semi-)automated verification of smart contract fairness, whose results can be used to refute false claims with concrete examples or certify contract implementations with respect to desired fairness properties. We implement FairCon, which is able to check fairness properties including truthfulness, efficiency, optimality, and collusion-freeness for Ethereum smart contracts. We evaluate FairCon on a set of real-world benchmarks and the experiment result indicates that FairCon is effective in detecting property violations and able to prove fairness for common types of contracts.

Unlike those on public permissionless blockchains, smart contracts on enterprise permissioned blockchains are not limited by resource constraints, and therefore often larger and more complex. Current testing and analysis tools lack support for such contracts, which demonstrate stateful behaviors and require special treatment in quality assurance. In this paper, we present a model-based testing platform, called ModCon, relying on user-specified models to define test oracles, guide test generation, and measure test adequacy. ModCon is Web-based and supports both permissionless and permissioned blockchain platforms. We demonstrate the usage and key features of ModCon on real enterprise smart contract applications.

Recurrent neural network (RNN) has achieved great success in processing sequential inputs for applications such as automatic speech recognition, natural language processing and machine translation. However, quality and reliability issues of RNNs make them vulnerable to adversarial attacks and hinder their deployment in real-world applications. In this paper, we propose a quantitative analysis framework - DeepStellar - to pave the way for effective quality and security analysis of software systems powered by RNNs. DeepStellar is generic to handle various RNN architectures, including LSTM and GRU, scalable to work on industrial-grade RNN models, and extensible to develop customized analyzers and tools. We demonstrated that, with DeepStellar, users are able to design efficient test generation tools, and develop effective adversarial sample detectors. We tested the developed applications on three real RNN models, including speech recognition and image classification. DeepStellar outperforms existing approaches three hundred times in generating defect-triggering tests and achieves 97% accuracy in detecting adversarial attacks. A video demonstration which shows the main features of DeepStellar is available at: https://sites.google.com/view/deepstellar/tool-demo.

Deep neural network (DNN) has been widely applied to safety-critical scenarios such as autonomous vehicle, security surveillance, and cyber-physical control systems. Yet, the incorrect behaviors of DNNs can lead to severe accidents and tremendous losses due to hidden defects. In this paper, we present DeepHunter, a general-purpose fuzzing framework for detecting defects of DNNs. DeepHunter is inspired by traditional grey-box fuzzing and aims to increase the overall test coverage by applying adaptive heuristics according to runtime feedback. Specifically, DeepHunter provides a series of seed selection strategies, metamorphic mutation strategies, and testing criteria customized to DNN testing; all these components support multiple built-in configurations which are easy to extend. We evaluated DeepHunter on two popular datasets and the results demonstrate the effectiveness of DeepHunter in achieving coverage increase and detecting real defects. A video demonstration which showcases the main features of DeepHunter can be found at https://youtu.be/s5DfLErcgrc.

Deep Learning (DL) has achieved tremendous success in many cutting-edge applications. However, the state-of-the-art DL systems still suffer from quality issues. While some recent progress has been made on the analysis of feed-forward DL systems, little study has been done on the Recurrent Neural Network (RNN)-based stateful DL systems, which are widely used in audio, natural languages and video processing, etc. In this paper, we initiate the very first step towards the quantitative analysis of RNN-based DL systems. We model RNN as an abstract state transition system to characterize its internal behaviors. Based on the abstract model, we design two trace similarity metrics and five coverage criteria which enable the quantitative analysis of RNNs. We further propose two algorithms powered by the quantitative measures for adversarial sample detection and coverage-guided test generation. We evaluate DeepStellar on four RNN-based systems covering image classification and automated speech recognition. The results demonstrate that the abstract model is useful in capturing the internal behaviors of RNNs, and confirm that (1) the similarity metrics could effectively capture the differences between samples even with very small perturbations (achieving 97% accuracy for detecting adversarial samples) and (2) the coverage criteria are useful in revealing erroneous behaviors (generating three times more adversarial samples than random testing and hundreds times more than the unrolling approach).

Software is often built by integrating components created by different teams or even different organizations. With little understanding of changes in dependent components, it is challenging to maintain correctness and robustness of the entire system. In this paper, we investigate the effect of component changes on the behavior of their clients. We observe that changes in a component are often irrelevant to a particular client and thus can be adopted without any delays or negative effects. Following this observation, we formulate the notion of client-specific equivalence checking (CSE) and develop an automated technique optimized for checking such equivalence. We evaluate our technique on a set of benchmarks, including those from the existing literature on equivalence checking, and show its applicability and effectiveness.

Software developers often need to transfer functionality, e.g., a set of commits implementing a new feature or a bug fix, from one branch of a configuration management system to another. That can be a challenging task as the existing configuration management tools lack support for matching high-level, semantic functionality with low-level version histories. The developer thus has to either manually identify the exact set of semantically-related commits implementing the functionality of interest or sequentially port a segment of the change history, “inheriting” additional, unwanted functionality. In this paper, we tackle this problem by providing automated support for identifying the set of semantically-related commits implementing a particular functionality, which is defined by a set of tests. We formally define the semantic slicing problem, provide an algorithm for identifying a set of commits that constitute a slice, and propose techniques to minimize the produced slice. We then instantiate the overall approach, CSlicer, in a specific implementation for Java projects managed in Git and evaluate its correctness and effectiveness on a set of open-source software repositories. We show that it allows to identify subsets of change histories that maintain the functionality of interest but are substantially smaller than the original ones.

Software change histories are results of incremental updates made by developers. As a side-effect of the software development process, version history is a surprisingly useful source of information for understanding, maintaining and reusing software. However, traditional commit-based sequential organization of version histories lacks semantic structure and thus are insufficient for many development tasks that require high-level, semantic understanding of program functionality, such as locating feature implementations and porting hot fixes. In this work, we propose to use well-organized unit tests as identifiers for corresponding software functionalities. We then present a family of automated techniques which analyze the semantics of historical changes and assist developers in many everyday practical settings. For validation, we evaluate our approaches on a benchmark of developer-annotated version history instances obtained from real-world open source software projects on GitHub.

Over the last few years, researchers proposed several semantic history slicing approaches that identify the set of semantically-related commits implementing a particular software functionality. However, there is no comprehensive benchmark for evaluating these approaches, making it difficult to assess their capabilities. This paper presents a dataset of 81 semantic change data collected from 8 real-world projects. The dataset is created for benchmarking semantic history slicing techniques. We provide details on the data collection process and the storage format. We also discuss usage and possible extensions of the dataset.

Semantic history slicing solves the problem of extracting changes related to a particular high-level functionality from the software version histories. State-of-the-art techniques combine static program analysis and dynamic execution tracing to infer an over-approximated set of changes that can preserve the functional behaviors captured by a test suite. However, due to the conservative nature of such techniques, the sliced histories may contain irrelevant changes. In this paper, we propose a divide-and-conquer-style partitioning approach enhanced by dynamic delta refinement to produce minimal semantic history slices. We utilize deltas in dynamic invariants generated from successive test executions to learn significance of changes with respect to the target functionality. Empirical results indicate that these measurements accurately rank changes according to their relevance to the desired test behaviors and thus partition history slices in an efficient and effective manner.

The latest Federal Communications Commission (FCC) ruling has enforced database-driven cognitive radio networks (CRNs), in which all secondary users (SUs) can query a database to obtain spectrum availability information (SAI). Database-driven CRNs are regarded as a promising approach for dynamic and highly efficient spectrum management paradigm for large-scale Internet of Things (IoT). However, as a typical location-based service (LBS), before providing services to the user, there is no verification of the queried location, which is very vulnerable to location spoofing attack. A malicious user can report a fake location to the database and access the channels that may not be available for its location. This will introduce serious interference to the primary users (PUs). In this study, we identify a new kind of attack coined as location cheating attack, which allows an attacker to spoof other users to another location and make them query the database with wrong location, or allows a malicious user to forge location arbitrarily and query the database for services. To thwart this attack, we propose a novel infrastructure-based approach that relies on the existing WiFi or cellular network access points (or AP) to provide privacy-preserving location proof. With the proposed solution, the database can verify the locations without knowing the user's accurate location. We perform comprehensive experiments to evaluate the performance of the proposed approach. Experimental results show that our approach, besides providing location proofs effectively, can significantly improve the user's location privacy.

Database-driven Cognitive Radio Network (CRN) has been proposed to replace the requirement of spectrum sensing of terminal devices so that the operation of users is simplified. However, location privacy issues introduce a big challenge for securing database-driven CRN due to spectrum availability information. The existing works consider either PU or SU's location privacy while not the both. In this study, we identify a unified attack framework in which a curious user could infer a target's location based on the spectrum availability/utilization information. Further, we propose a location privacy protection mechanism, which allows both SU and PU to protect their location privacy by adopting a series of countermeasures. The location privacy and spectrum utility are the trade-off. In the countermeasures of location privacy preserving spectrum query process, both SU and database aim to maximize the location privacy with constraints of spectrum utility. Thus, they can obtain higher location privacy level with sacrifice of spectrum utility as long as the spectrum utility meets the requirements. We evaluate the unified attack and defence approaches based on simulation and demonstrate the effectiveness of the proposed location privacy preserving approaches.

Software developers often need to transfer func-tionality, e.g., a set of commits implementing a new feature or a bug fix, from one branch of a configuration management system to another. That can be a challenging task as the existing configuration management tools lack support for matching high-level semantic functionality with low-level version histories. The developer thus has to either manually identify the exact set of semantically-related commits implementing the functionality of interest or sequentially port a specific subset of the change history, "inheriting" additional, unwanted functionality. In this paper, we tackle this problem by providing automated support for identifying the set of semantically-related commits implementing a particular functionality, which is defined by a set of tests. We refer to our approach, CSLICER, as semantic slicing of version histories. We formally define the semantic slicing problem, provide an algorithm for identifying a set of commits that constitute a slice, and instantiate it in a specific implementation for Java projects managed in Git. We evaluate the correctness and effectiveness of our approach on a set of open-source software repositories. We show that it allows to identify subsets of change histories that maintain the functionality of interest but are substantially smaller than the original ones.

The rise in efficiency of Satisfiability Modulo Theories (SMT) solvers has created numerous uses for them in software verification, program synthesis, functional programming, refinement types, etc. In all of these applications, SMT solvers are used for generating satisfying assignments (e.g., a witness for a bug) or proving unsatisfiability/validity(e.g., proving that a subtyping relation holds). We are often interested in finding not just an arbitrary satisfying assignment, but one that optimizes (minimizes/maximizes) certain criteria. For example, we might be interested in detecting program executions that maximize energy usage (performance bugs), or synthesizing short programs that do not make expensive API calls. Unfortunately, none of the available SMT solvers offer such optimization capabilities.

Model checking provides a way to automatically verify hardware and software systems, whereas the goal of planning is to produce a sequence of actions that leads from the initial state to the desired goal states. Recently research indicates that there is a strong connection between model checking and planning problem solving. In this paper, we investigate the feasibility of using different model checking tools and techniques for solving classic planning problems. To achieve this, we carried out a number of experiments on different planning domains in order to compare the performance and capabilities of various tools. Our experimental results indicate that the performance of some model checkers is comparable to that of state-of-theart planners for certain categories of problems. In particular, a new planning module with specifically designed searching algorithm is implemented on top of the established model checking framework, Process Analysis Toolkit (PAT), to serve as a planning solution provider for upper layer applications. A case study on a public transportation management system has been developed to demonstrate the idea of using the PAT model checker as a planning service.