Satisfiability Modulo Theories (SMT) plays a critical role in various software engineering applications, including program verification, symbolic execution, and automated test generation. Over the years, a wide range of SMT solvers has been developed, typically designed for general purposes or tailored to specific background theories, such as bit-vectors or nonlinear arithmetic. Due to the diversity and complexity of SMT instances, no single solver consistently outperforms others across all problem domains. This motivates the need for algorithm selection strategies that can adaptively choose solvers based on the characteristics of the instances.To overcome the limitations of single-solver selection, solving SMT as a scheduling problem, enabling a more fault-tolerant and effective use of multiple solvers in sequence. We model algorithm scheduling as a hyperparameter optimization problem, enabling efficient black-box search over solver sequences while treating the dataset as a whole, thus achieving globally optimized and robust scheduling strategies. The resulting scheduler called SMTgazer. To further enhance scheduling efficiency and solver performance, we propose two optimizations: leveraging unsupervised X-means clustering to create semantically coherent instance groups for localized model training, and augmenting the Bayesian optimization surrogate with boosting and bagging ensembles to improve generalization and mitigate overfitting, thereby yielding more reliable performance predictions for the sequential portfolio scheduler.Extensive experiments are conducted to evaluate the performance of SMTgazer, utilizing six SMT benchmarks derived from real-world applications. It shows that our approach consistently outperforms current state-of-the-art methods. Particularly, SMTgazer achieves a 44.65% reduction in PAR-2 score and 69.11% decrease in the number of unsolved instances, compared to the strongest competitor, Sibyl, demonstrating the effectiveness of formulating SMT algorithm scheduling as a hyperparameter optimization problem. We further analyze the generated scheduling sequences to uncover the design principles that explain the success of our method. Finally, we also empirically show that our approach is both robust and generalizable, and the proposed strategies are effective.

Automatic and accurate classification of cholangiocarcinoma (CCA) using optical coherence tomography (OCT) images is critical for confirming infiltration margins. Considering that the morphological representations in pathology stains can be implicitly captured in OCT imaging, we introduce the optical attenuation coefficient (OAC) and generalized visual-language information to focus on the optical properties of diseased tissue and exploit its inherent textured features. Maintaining the data within the appropriate working range during OCT scanning is crucial for reliable diagnosis. To this end, we propose an autonomous scanning method integrated with novel deep learning architecture to construct an efficient computer-aided system. We develop a cross-modal complementarity model, the language and attenuation-driven network (LA-OCT Net), designed to enhance the interaction between OAC and OCT information and leverage generalized image-text alignment for refined feature representation. The model incorporates a disentangled attenuation selection-based adversarial correlation loss to magnify the discrepancy between cross-modal features while maintaining discriminative consistency. The proposed robot-assisted pipeline ensures precise repositioning of the diseased cross-sectional location, allowing consistent measurements to treatment and precise tumor margin detection. Extensive experiments on a comprehensive clinical dataset demonstrate the effectiveness and superiority of our method. Specifically, our approach not only improves accuracy by 6% compared to state-of-the-art techniques, while also providing new insights into the potential of optical biopsy.

To meet the increasing demand for customized software, highly configurable systems become essential in practice. Such systems offer many options to configure, and ensuring the reliability of these systems is critical. A widely used evaluation metric for testing these systems is \(t\) -wise coverage, where \(t\) represents testing strength, and its value typically ranges from 2 to 6. It is crucial to design effective and efficient methods for generating test suites that achieve high \(t\) -wise coverage. However, current state-of-the-art methods need to generate large test suites for achieving high \(t\) -wise coverage. In this work, we propose a novel method called LS-Sampling-Plus that can efficiently generate test suites with high \(t\) -wise coverage for \(2\leq t\leq 6\) while being smaller in size compared to existing state-of-the-art methods. LS-Sampling-Plus incorporates many core algorithmic techniques, including two novel scoring functions, a dynamic mechanism for updating sampling probabilities, and a validity-guaranteed systematic search method. Our experiments on various practical benchmarks show that LS-Sampling-Plus can achieve higher \(t\) -wise coverage than current state-of-the-art methods, through building a test suite of the same size. Moreover, our evaluations indicate the effectiveness of all core algorithmic techniques of LS-Sampling-Plus . Furthermore, LS-Sampling-Plus exhibits better scalability and fault detection capability than existing state-of-the-art methods.

Unlike wired networks, the configuration and the behavior of wireless networks are heavily dependent on many environmental factors. While this makes it more difficult to build a wireless network testbed whose behavior is controllable, it also makes the availability of such a testbed all the more desirable. Indeed, the difficulties in building a good wireless mesh testbed belie the fact that most research work on mesh network performance is backed up only by computer simulations. In this paper, we present a practical design philosophy in which a realistic and controllable wireless mesh network testbed is built with a relatively small deployment of physical equipments by exploiting the idea of a virtual network. Specifically, we simulate a virtual network within the testbed and use one physical wireless transceiver to simulate multiple virtual devices. An observer who only reads the transmitted wireless messages will not be able to tell the difference from a real wireless mesh. Our approach has been adopted in a recent industry-standard testing suite, namely, Wi-HTest. In this paper, we shall discuss our experience in building Wi-HTest by applying the virtual network approach.

WirelessHART was released in September 2007 and is the first open wireless communication standard specifically designed for real-time process control applications. It is designed to the same standards as its wired counterpart for reliability and interoperability. To ensure the compliance with the HART Communication Protocol and the adherence to its strict timing requirements, all WirelessHART devices must be thoroughly tested and registered with the HART Communication Foundation (HCF). In this paper, we present Wi-HTest, the test suite designed to exercise WirelessHART devices, thus facilitating compliance assessment. We discuss the detailed architecture of Wi-HTest and highlight several critical features like packet handling with accurate timing control and fault data injection. We also describe a sniffer called Wi-Analys for capturing WirelessHART packets along with their timing information and a post process suite for analyzing the packets. These three tools together provide the complete compliance verification environment for WirelessHART. Based on the test specification developed by HCF, a representative test case is conducted for the purpose of demonstration. This test case in turn shows that Wi-HTest is a novel and efficient test suite for verifying the compliance of real-time WirelessHART devices.

WirelessHART is an emerging wireless communication standard that is targeted at the real-time process control industry.An example application of wireless communication in an industrial process control plant is the location of field engineers. The capability to locate personnel is a safety critical issue in process control plants because of high risks posed by toxic chemicals and other hazards. This paper presents the design, implementation and evaluation of a location-aware application built upon WirelessHART. The aim of this application is to locate a mobile device (and thus the person carrying the device) via the deployed WirelessHART network. The application is a software-based - no device modifications are required. Consequently, it is applicable to any WirelessHART network. In this application, both the mobile device (a handheld device or a badge carried by a worker) and field devices (attached to the plant process) periodically send health reports of their neighbors to the network manager. The network manager analyzes these reports and discards the untrustworthy pairs through comparison. Next, the network manager feeds the average received signal indications to a well-trained radio propagation model to derive the location. To evaluation our solution, several preliminary experiments are carried out and the results are very promising, with a median error less than 4 meters, which is good enough for the industrial requirement. To the best of our knowledge, this is the first attempt to develop location-aware application in WirelessHART networks.

Wireless technology has been regarded as a paradigm shifter in the process industry. The first open wireless communication standard specifically designed for process measurement and control applications, WirelessHART was officially released in September 2007 (as a part of the HART 7 Specification). WirelessHART is a secure and TDMA-based wireless mesh networking technology operating in the 2.4GHz ISM radio band. In this paper, we give an introduction to the architecture of WirelessHART and share our first-hand experience in building a prototype for this specification. We describe several challenges we had to tackle during the implementation, such as the design of the timer, network wide synchronization, communication security, reliable mesh networking, and the central network manager. For each challenge, we provide a detailed analysis and propose our solution. Based on the prototype implementation, a simple WirelessHART network has been built for the purpose of demonstration. The demonstration network in turn validates our design. To the best of our knowledge, this is the first reported effort to build a WirelessHART protocol stack.

WirelessHART was released in September 2007 and is the first open wireless communication standard specifically designed for process control applications. As an optional part of the HART® Communication Protocol, WirelessHART is designed to the same standards for reliability and interoperability. To ensure the compliance and adherence to the high level of interoperability defined by the HART Communication Foundation (HCF), all WirelessHART devices must be thoroughly tested and registered with the HCF. In this paper, we present Wi-HTest, the test engine designed to exercise WirelessHART devices, thus facilitating compliance assessment. We discuss the detailed architecture of Wi-HTest and highlight several critical features like virtual devices and fault data injection.

WirelessHART is the first open wireless standard for the process control industry. Previously we demonstrated a three-node prototype network based on an early release of the protocol stack. In this demonstration we build a fully operational WirelessHART sensor network of multiple nodes. We show the creation of the network and the execution of process monitoring applications on the network. This new demonstration network serves as a proof of concept for the revised WirelessHART standard and as a platform for our future research and experiments.

Wireless sensor networks have been a very active research field in the past few years. However, most of extant research has focused on wireless sensing, such as environmental and habitat monitoring [6]. In this paper, we investigate the feasibility of applying wireless technologies in industrial real-time process control systems. We define a minimum set of assumptions about the underlying sensor networks in order to achieve realtime support for process control. These assumptions are necessary and practical from an industrial perspective. We formulate the modeling of a wireless process control configuration as a multi-processor scheduling problem. The resulting scheduling problem is solved by the scheduler synthesis tool MSP.RTL [7] to produce a valid configuration for deployment. The deployment, because of the way it is derived, will provide real-time wireless support for the controlled processes. Simulation results on data from real plant configurations show that this approach can also drastically reduce potential interferences between wireless transfers.