This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this description into formulae evaluated with satisfiability modulo theories (SMT) solvers. The proposed approach was realized with the efficient SMT-based bounded model checker (ESBMC), which resulted in a tool called ESBMC-Python, the first BMC-based Python-code verifier. Experimental results, with a test suite specifically developed for this purpose, showed its effectiveness, where successful and failed tests were correctly evaluated. Moreover, it found a real problem in the Ethereum Consensus Specification.

Witness validation is a formal verification method to independently verify software verification tool results, with two main categories: violation and correctness witness validators. Validators for violation witnesses in Java include Wit4Java and GWIT, but no dedicated correctness witness validators exist. To address this gap, this paper presents the Java Correctness-Witness Validator (JCWIT), the first tool to validate correctness witnesses in Java programs. JCWIT accepts an original program, a specification, and a correctness witness as inputs. Then, it uses invariants of each witness’s execution state as conditions to be incorporated into the original program in the form of assertions, thus instrumenting it. Next, JCWIT employs an established tool, Java Bounded Model Checker (JBMC), to verify the transformed program, hence examining the reproducibility of correct witness results. We evaluated JCWIT in the SV-COMP ReachSafety benchmark, and the results show that JCWIT can correctly validate the correctness witnesses generated by Java verifiers.

Deploying Neural networks (NNs) in low-resource domains is challenging because of their high computing, memory, and power requirements. For this reason, NNs are often quantized before deployment, but such an approach degrades their accuracy. Thus, we propose the counterexample guided neural network quantization refinement (CEG4N) framework, which combines search-based quantization and equivalence checking. The former minimizes computational requirements, while the latter guarantees that the behavior of an NN does not change after quantization. We evaluate CEG4N on a diverse set of benchmarks, including large and small NNs. Our technique successfully quantizes the networks in the chosen evaluation set, while producing models with up to 163% better accuracy than state-of-the-art techniques.

Abstract Digital TV (DTV) receivers are usually submitted to testing systems for conformity and robustness assessment, and their approval implies correct operation under a given DTV specification protocol. However, many broadcasters inadvertently misconfigure their devices and transmit the wrong information concerning data structures and protocol format. Since most receivers were not designed to operate under such conditions, malfunction and incorrect behaviour may be noticed, often recognized as field problems, thus compromising a given system's operation. Moreover, the way those problems are usually introduced in DTV signals presents some randomness, but with known restrictions given by the underlying transport protocols used in DTV systems, which resembles fuzzing techniques. Indeed, everything may happen since any deviation can incur problems, depending on each specific implementation. This error scenario is addressed here, and a novel receiver robustness evaluation methodology based on non‐compliance tests using grammar‐based guided fuzzing is proposed. In particular, devices are submitted to unforeseen conditions and incorrect configuration. They are created with guided fuzzing based on real problems, protocol structure, and system architecture to provide resources for handling them, thus ensuring correct operation. Experiments using such a fuzzing scheme have shown its efficacy and provided opportunities to improve robustness regarding commercial DTV platforms.

Abstract DepthK is a source-to-source transformation tool that employs bounded model checking (BMC) to verify and falsify safety properties in single- and multi-threaded C programs, without manual annotation of loop invariants. Here, we describe and evaluate a proof-by-induction algorithm that combines k-induction with invariant inference to prove and refute safety properties. We apply two invariant generators to produce program invariants and feed these into a k-induction-based verification algorithm implemented in DepthK, which uses the efficient SMT-based context-bounded model checker (ESBMC) as sequential verification back-end. A set of C benchmarks from the International Competition on Software Verification (SV-COMP) and embedded-system applications extracted from the available literature are used to evaluate the effectiveness of the proposed approach. Experimental results show that k-induction with invariants can handle a wide variety of safety properties, in typical programs with loops and embedded software applications from the telecommunications, control systems, and medical domains. The results of our comparative evaluation extend the knowledge about approaches that rely on both BMC and k-induction for software verification, in the following ways. (1) The proposed method outperforms the existing implementations that use k-induction with an interval-invariant generator (e.g., 2LS and ESBMC), in the category ConcurrencySafety, and overcame, in others categories, such as SoftwareSystems, other software verifiers that use plain BMC (e.g., CBMC). Also, (2) it is more precise than other verifiers based on the property-directed reachability (PDR) algorithm (i.e., SeaHorn, Vvt and CPAchecker-CTIGAR). This way, our methodology demonstrated improvement over existing BMC and k-induction-based approaches.

This work proposes an abstraction of the Qt framework, named as Qt Operational Model (QtOM), which is integrated into two different verification approaches: explicit-state model checking and symbolic (bounded) model checking. The proposed methodology is the first one to formally verify Qt-based applications, which has the potential to devise new directions for software verification of portable code. The full version of this paper is published in Software Testing, Verification and Reliability, on 02 March 2017 and it is available at https://doi.org/10.1002/stvr.1632.

During the last decades, model checking techniques have been applied to improve overall system reliability, in unmanned aerial vehicle (UAV) approaches. Nonetheless, there is little effort focused on applying those methods to the control-system domain, especially when it comes to the investigation of low-level implementation errors, which are related to digital controllers and hardware compatibility. The present study addresses the mentioned problems and proposes the application of a bounded model checking tool, named as Digital System Verifier (DSVerifier), to the verification of digital-system implementation issues, in order to investigate problems that emerge in digital controllers designed for UAV attitude systems. A verification methodology to search for implementation errors related to finite word-length effects (e.g., arithmetic overflows and limit cycles), in UAV attitude controllers, is presented, along with its evaluation, which aims to ensure correct-by-design systems. Experimental results show that low-level failures in UAV attitude control software used in aerial surveillance are identified by DSVerifier, which can also be used for developing sound and correct implementations, through its integration into development processes. Finally, given that the proposed approach handles C code and takes into account hardware specifications, it is suitable for verifying final controller implementations, which is a more practical scenario.

A MATLAB toolbox is presented, with the goal of checking occurrences of design errors typically found in fixed-point digital systems, considering finite word-length effects. In particular, the present toolbox works as a front-end to a recently introduced verification tool, known as Digital-System Verifier (DSVerifier), and checks overflow, limit cycle, quantization, stability, and minimum phase errors in digital systems represented by transfer-function and state-space equations. It provides a command-line version with simplified access to specific functionality and a graphical-user interface, which was developed as a MATLAB application. The resulting toolbox enables application of verification to real-world systems by control engineers.

Summary The software development process for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, technology companies tend to invest in fast and automatic verification mechanisms, to create robust systems and reduce product recall rates. In addition, further development‐time reduction and system robustness can be achieved through cross‐platform frameworks, such as Qt, which favor the reliable port of software stacks to different devices. Based on that, the present paper proposes a simplified version of the Qt framework, which is integrated into a checker based on satisfiability modulo theories (SMT), known as the Efficient SMT‐based Context‐Bounded Model Checker, for verifying actual Qt‐based applications, with a success rate of 89%, for the developed benchmark suite. Furthermore, the simplified version of the Qt framework, named as Qt Operational Model, was also evaluated using other state‐of‐the‐art verifiers for C++ programs. In fact, Qt Operational Model was combined with 2 different verification approaches: explicit‐state model checking and also symbolic (bounded) model checking, during the experimental evaluation, which highlights its flexibility. The proposed methodology is the first one to formally verify Qt‐based applications, which has the potential to devise new directions for software verification of portable code.

In this work, we further develop the multidimensional multiscale parser (MMP) algorithm, a recently proposed universal lossy compression method which has been successfully applied to images as well as other types of data, as video and ECG signals. The MMP is based on approximate multiscale pattern matching, encoding blocks of an input signal using expanded and contracted versions of patterns stored in a dictionary. The dictionary is updated using expanded and contracted versions of concatenations of previously encoded blocks. This implies that MMP builds its own dictionary while the input data is being encoded, using segments of the input itself, which lends it a universal flavor. It presents a flexible structure, which allows for easily adding data-specific extensions to the base algorithm. Often, the signals to be encoded belong to a narrow class, as the one of smooth images. In these cases, one expects that some improvement can be achieved by introducing some knowledge about the source to be encoded. In this paper, we use the assumption about the smoothness of the source in order to create good context models for the probability of blocks in the dictionary. Such probability models are estimated by considering smoothness constraints around causal block boundaries. In addition, we refine the obtained probability models by also exploiting the existing knowledge about the original scale of the included blocks during the dictionary updating process. Simulation results have shown that these developments allow significant improvements over the original MMP for smooth images, while keeping its state-of-the-art performance for more complex, less smooth ones, thus improving MMP's universal character.

Mobile wireless broadband access networks are now becoming a reality, thanks to the emerging IEEE 802.16e standard. This kind of network offers different challenges when compared to the fixed ones, as power consumption becomes a major concern. In this standard, a strict organization of the downlink bursts is not guaranteed in the OFDMA frame and this may lead to extra power consumption for the receiver, decreasing the device's lifetime. In the present paper, we introduce an optimization algorithm capable of reducing the activity of each receiver in the system for decoding its addressed bursts, thanks to a better time-frequency organization of the bursts. We first work on fitting bursts within the smallest frame, and show that the minimal number of OFDM symbols is enough in 70 to 80% of the cases, while one extra is needed otherwise. Using a binary tree implementation of an exhaustive burst placement search, we also show that we can gain 20 to 30% in duty-cycling of the receivers by selecting the best configuration, hence gaining the corresponding energy. This holds for receivers decoding either their bursts only or all the bursts from the beginning of the frame up to their own bursts before sleeping, depending on the scenario. The full search is sustainable for up to 8 user bursts per frame.

Recently, the multidimensional multiscale parser (MMP), an algorithm based on multiscale recurrent patterns, has been used to successfully compress data from ECG signals. Their quasi-periodic nature makes them natural candidates for the use of recurrent patterns. However, as many diagnostic relevant signals are far from periodic, the characteristics of MMP are not fully exploited. We have dealt with this problem by interpolating the ECG signal so that the interval between successive heart beats becomes constant. Following that, the algorithm subtracts the average period from the interpolated signal. Simulation results show that these modifications increase the rate-distortion performance.

The recently proposed method for image compression based on multi-scale recurrent patterns, the MMP (multidimensional multiscale parser) has been shown to perform well for a large class of images, specially for those containing text or graphics. However, its performance for coding smooth, gray scale images is still distant from the state of the art. In this paper we propose an extension for it, the SM-MMP (side-match MMP). In this method, as in MMP, a multidimensional signal is recursively segmented into variable-length blocks, and each segment is encoded using expansions and contractions of vectors in a dictionary. The dictionary is updated while the data is being encoded, using concatenations of expanded and contracted versions of previously encoded blocks. However, unlike MMP, in SM-MMP the dictionaries are built considering smoothness constraints around block boundaries, similar to the side-match vector quantization methods. This allows it to perform better than the MMP when the images are smooth, without sacrificing its performance for images containing text or graphics. Indeed, our simulation results show that the proposed method is effective, yielding improvements of the order of 1.5 dB over the original MMP for grayscale images, while preserving the high performance of the original MMP for graphics, text and mixed images.