Visible to the public Biblio

Filters: Keyword is scalable verification  [Clear All Filters]
Das, Arnab, Briggs, Ian, Gopalakrishnan, Ganesh, Krishnamoorthy, Sriram, Panchekha, Pavel.  2020.  Scalable yet Rigorous Floating-Point Error Analysis. SC20: International Conference for High Performance Computing, Networking, Storage and Analysis. :1–14.
Automated techniques for rigorous floating-point round-off error analysis are a prerequisite to placing important activities in HPC such as precision allocation, verification, and code optimization on a formal footing. Yet existing techniques cannot provide tight bounds for expressions beyond a few dozen operators-barely enough for HPC. In this work, we offer an approach embedded in a new tool called SATIHE that scales error analysis by four orders of magnitude compared to today's best-of-class tools. We explain how three key ideas underlying SATIHE helps it attain such scale: path strength reduction, bound optimization, and abstraction. SATIHE provides tight bounds and rigorous guarantees on significantly larger expressions with well over a hundred thousand operators, covering important examples including FFT, matrix multiplication, and PDE stencils.
Naik, Nikhil, Nuzzo, Pierluigi.  2020.  Robustness Contracts for Scalable Verification of Neural Network-Enabled Cyber-Physical Systems. 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). :1–12.
The proliferation of artificial intelligence based systems in all walks of life raises concerns about their safety and robustness, especially for cyber-physical systems including multiple machine learning components. In this paper, we introduce robustness contracts as a framework for compositional specification and reasoning about the robustness of cyber-physical systems based on neural network (NN) components. Robustness contracts can encompass and generalize a variety of notions of robustness which were previously proposed in the literature. They can seamlessly apply to NN-based perception as well as deep reinforcement learning (RL)-enabled control applications. We present a sound and complete algorithm that can efficiently verify the satisfaction of a class of robustness contracts on NNs by leveraging notions from Lagrangian duality to identify system configurations that violate the contracts. We illustrate the effectiveness of our approach on the verification of NN-based perception systems and deep RL-based control systems.
Herber, Paula, Liebrenz, Timm.  2020.  Dependence Analysis and Automated Partitioning for Scalable Formal Analysis of SystemC Designs. 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). :1–6.
Embedded systems often consist of deeply intertwined hardware and software components. At the same time, they are often used in safety-critical applications, where an error may result in enormous costs or even loss of human lives. Existing verification techniques that show the absence of errors do not scale well for complex integrated HW/SW systems. In this paper, we present a dependence analysis and automated partitioning approach for the formal analysis of HW/SW codesigns that are modeled in SystemC. The key idea of our approach is threefold: first, we partition a given system into loosely coupled submodels. Second, we analyze the dependences between these submodels and compute an abstract verification interface for each of them, which captures all possible influences of all other submodels. Third, we verify global properties of the overall system by verifying them separately for each subsystem. We demonstrate that our approach significantly reduces verification times and increases scalability with results for an anti-lock braking system.
Sharma, Mohit, Strathman, Hunter J., Walker, Ross M..  2020.  Verification of a Rapidly Multiplexed Circuit for Scalable Action Potential Recording. 2020 IEEE International Symposium on Circuits and Systems (ISCAS). :1–1.
This report presents characterizations of in vivo neural recordings performed with a CMOS multichannel chip that uses rapid multiplexing directly at the electrodes, without any pre-amplification or buffering. Neural recordings were taken from a 16-channel microwire array implanted in rodent cortex, with comparison to a gold-standard commercial bench-top recording system. We were able to record well-isolated threshold crossings from 10 multiplexed electrodes and typical local field potential waveforms from 16, with strong agreement with the standard system (average SNR = 2.59 and 3.07 respectively). For 10 electrodes, the circuit achieves an effective area per channel of 0.0077 mm2, which is \textbackslashtextgreater5× smaller than typical multichannel chips. Extensive characterizations of noise and signal quality are presented and compared to fundamental theory, as well as results from in vivo and in vitro experiments. By demonstrating the validation of rapid multiplexing directly at the electrodes, this report confirms it as a promising approach for reducing circuit area in massively-multichannel neural recording systems, which is crucial for scaling recording site density and achieving large-scale sensing of brain activity with high spatiotemporal resolution.
Adelt, Peer, Koppelmann, Bastian, Mueller, Wolfgang, Scheytt, Christoph.  2020.  A Scalable Platform for QEMU Based Fault Effect Analysis for RISC-V Hardware Architectures. MBMV 2020 - Methods and Description Languages for Modelling and Verification of Circuits and Systems; GMM/ITG/GI-Workshop. :1–8.
Fault effect simulation is a well-established technique for the qualification of robust embedded software and hardware as required by different safety standards. Our article introduces a Virtual Prototype based approach for the fault analysis and fast simulation of a set of automatically generated and target compiled software programs. The approach scales to different RISC-V ISA standard subset configurations and is based on an instruction and hardware register coverage for automatic fault injections of permanent and transient bitflips. The analysis of each software binary evaluates its opcode type and register access coverage including the addressed memory space. Based on this information dedicated sets of fault injected hardware models, i.e., mutants, are generated. The simulation of all mutants conducted with the different binaries finally identifies the cases with a normal termination though executed on a faulty hardware model. They are identified as a subject for further investigations and improvements by the implementation of additional hardware or software safety countermeasures. Our final evaluation results with automatic C code generation, compilation, analysis, and simulation show that QEMU provides an adequate efficient platform, which also scales to more complex scenarios.
Shen, Shen, Tedrake, Russ.  2020.  Sampling Quotient-Ring Sum-of-Squares Programs for Scalable Verification of Nonlinear Systems. 2020 59th IEEE Conference on Decision and Control (CDC). :2535–2542.
This paper presents a novel method, combining new formulations and sampling, to improve the scalability of sum-of-squares (SOS) programming-based system verification. Region-of-attraction approximation problems are considered for polynomial, polynomial with generalized Lur'e uncertainty, and rational trigonometric multi-rigid-body systems. Our method starts by identifying that Lagrange multipliers, traditionally heavily used for S-procedures, are a major culprit of creating bloated SOS programs. In light of this, we exploit inherent system properties-continuity, convexity, and implicit algebraic structure-and reformulate the problems as quotient-ring SOS programs, thereby eliminating all the multipliers. These new programs are smaller, sparser, less constrained, yet less conservative. Their computation is further improved by leveraging a recent result on sampling algebraic varieties. Remarkably, solution correctness is guaranteed with just a finite (in practice, very small) number of samples. Altogether, the proposed method can verify systems well beyond the reach of existing SOS-based approaches (32 states); on smaller problems where a baseline is available, it computes tighter solution 2-3 orders of magnitude faster.
Wu, Shanglun, Yuan, Yujie, Kar, Pushpendu.  2020.  Lightweight Verification and Fine-grained Access Control in Named Data Networking Based on Schnorr Signature and Hash Functions. 2020 IEEE 20th International Conference on Communication Technology (ICCT). :1561–1566.
Named Data Networking (NDN) is a new kind of architecture for future Internet, which is exactly satisfied with the rapidly increasing mobile requirement and information-depended applications that dominate today's Internet. However, the current verification-data accessed system is not safe enough to prevent data leakage because no strongly method to resist any device or user to access it. We bring up a lightweight verification based on hash functions and a fine-grained access control based on Schnorr Signature to address the issue seamlessly. The proposed scheme is scalable and protect data confidentiality in a NDN network.
Paulsen, Brandon, Wang, Jingbo, Wang, Jiawei, Wang, Chao.  2020.  NEURODIFF: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation. 2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE). :784–796.
As neural networks make their way into safety-critical systems, where misbehavior can lead to catastrophes, there is a growing interest in certifying the equivalence of two structurally similar neural networks - a problem known as differential verification. For example, compression techniques are often used in practice for deploying trained neural networks on computationally- and energy-constrained devices, which raises the question of how faithfully the compressed network mimics the original network. Unfortunately, existing methods either focus on verifying a single network or rely on loose approximations to prove the equivalence of two networks. Due to overly conservative approximation, differential verification lacks scalability in terms of both accuracy and computational cost. To overcome these problems, we propose NEURODIFF, a symbolic and fine-grained approximation technique that drastically increases the accuracy of differential verification on feed-forward ReLU networks while achieving many orders-of-magnitude speedup. NEURODIFF has two key contributions. The first one is new convex approximations that more accurately bound the difference of two networks under all possible inputs. The second one is judicious use of symbolic variables to represent neurons whose difference bounds have accumulated significant error. We find that these two techniques are complementary, i.e., when combined, the benefit is greater than the sum of their individual benefits. We have evaluated NEURODIFF on a variety of differential verification tasks. Our results show that NEURODIFF is up to 1000X faster and 5X more accurate than the state-of-the-art tool.
Zalasiński, Marcin, Cpałka, Krzysztof, Łapa, Krystian.  2020.  An interpretable fuzzy system in the on-line signature scalable verification. 2020 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE). :1–9.
This paper proposes new original solutions for the use of interpretable flexible fuzzy systems for identity verification based on an on-line signature. Such solutions must be scalable because the verification of the identity of each user must be carried out independently of one another. In addition, a large number of system users limit the possibilities of iterative system learning. An important issue is the ability to interpret the system rules because it explains how the similarity of test signatures to reference signature templates is assessed. In this paper, we propose an approach that meets all of the above requirements and works effectively for the on-line signatures' database used in the simulations.
Takita, Yutaka, Miyabe, Masatake, Tomonaga, Hiroshi, Oguchi, Naoki.  2020.  Scalable Impact Range Detection against Newly Added Rules for Smart Network Verification. 2020 IEEE 44th Annual Computers, Software, and Applications Conference (COMPSAC). :1471–1476.
Technological progress in cloud networking, 5G networks, and the IoT (Internet of Things) are remarkable. In addition, demands for flexible construction of SoEs (Systems on Engagement) for various type of businesses are increasing. In such environments, dynamic changes of network rules, such as access control (AC) or packet forwarding, are required to ensure function and security in networks. On the other hand, it is becoming increasingly difficult to grasp the exact situation in such networks by utilizing current well-known network verification technologies since a huge number of network rules are complexly intertwined. To mitigate these issues, we have proposed a scalable network verification approach utilizing the concept of "Packet Equivalence Class (PEC)," which enable precise network function verification by strictly recognizing the impact range of each network rule. However, this approach is still not scalable for very large-scale networks which consist of tens of thousands of routers. In this paper, we enhanced our impact range detection algorithm for practical large-scale networks. Through evaluation in the network with more than 80,000 AC rules, we confirmed that our enhanced algorithm can achieve precise impact range detection in under 600 seconds.
Le, Son N., Srinivasan, Sudarshan K., Smith, Scott C..  2020.  Exploiting Dual-Rail Register Invariants for Equivalence Verification of NCL Circuits. 2020 IEEE 63rd International Midwest Symposium on Circuits and Systems (MWSCAS). :21–24.
Equivalence checking is one of the most scalable and useful verification techniques in industry. NULL Convention Logic (NCL) circuits utilize dual-rail signals (i.e., two wires to represent one bit of DATA), where the wires are inverses of each other during a DATA wavefront. In this paper, a technique that exploits this invariant at NCL register boundaries is proposed to improve the efficiency of equivalence verification of NCL circuits.
Nguyen-Van, Thanh, Nguyen-Anh, Tuan, Le, Tien-Dat, Nguyen-Ho, Minh-Phuoc, Nguyen-Van, Tuong, Le, Nhat-Quang, Nguyen-An, Khuong.  2019.  Scalable Distributed Random Number Generation Based on Homomorphic Encryption. 2019 IEEE International Conference on Blockchain (Blockchain). :572–579.

Generating a secure source of publicly-verifiable randomness could be the single most fundamental technical challenge on a distributed network, especially in the blockchain context. Many current proposals face serious problems of scalability and security issues. We present a protocol which can be implemented on a blockchain that ensures unpredictable, tamper-resistant, scalable and publicly-verifiable outcomes. The main building blocks of our protocol are homomorphic encryption (HE) and verifiable random functions (VRF). The use of homomorphic encryption enables mathematical operations to be performed on encrypted data, to ensure no one knows the outcome prior to being generated. The protocol requires O(n) elliptic curve multiplications and additions as well as O(n) signature signing and verification operations, which permits great scalability. We present a comparison between recent approaches to the generation of random beacons.

White, Ruffin, Caiazza, Gianluca, Jiang, Chenxu, Ou, Xinyue, Yang, Zhiyue, Cortesi, Agostino, Christensen, Henrik.  2019.  Network Reconnaissance and Vulnerability Excavation of Secure DDS Systems. 2019 IEEE European Symposium on Security and Privacy Workshops (EuroS PW). :57–66.

Data Distribution Service (DDS) is a realtime peer-to-peer protocol that serves as a scalable middleware between distributed networked systems found in many Industrial IoT domains such as automotive, medical, energy, and defense. Since the initial ratification of the standard, specifications have introduced a Security Model and Service Plugin Interface (SPI) architecture, facilitating authenticated encryption and data centric access control while preserving interoperable data exchange. However, as Secure DDS v1.1, the default plugin specifications presently exchanges digitally signed capability lists of both participants in the clear during the crypto handshake for permission attestation; thus breaching confidentiality of the context of the connection. In this work, we present an attacker model that makes use of network reconnaissance afforded by this leaked context in conjunction with formal verification and model checking to arbitrarily reason about the underlying topology and reachability of information flow, enabling targeted attacks such as selective denial of service, adversarial partitioning of the data bus, or vulnerability excavation of vendor implementations.

Chau, Cuong, Hunt, Warren A., Kaufmann, Matt, Roncken, Marly, Sutherland, Ivan.  2019.  A Hierarchical Approach to Self-Timed Circuit Verification. 2019 25th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC). :105–113.
Self-timed circuits can be modeled in a link-joint style using a formally defined hardware description language. It has previously been shown how functional properties of these models can be formally verified with the ACL2 theorem prover using a scalable, hierarchical method. Here we extend that method to parameterized circuit families that may have loops and non-deterministic outputs. We illustrate this extension with iterative self-timed circuits that calculate the greatest common divisor of two natural numbers, with circuits that perform arbitrated merges non-deterministically, and with circuits that combine both of these.
Tan, Jiatong, Feng, Jianhua, Lyu, Yinxuan.  2019.  Stealthy Trojan Detection Based on Feature Analysis of Circuit Structure. 2019 IEEE International Conference on Electron Devices and Solid-State Circuits (EDSSC). :1–3.
The design methods and the detection methods for Hardware Trojan develop rapidly. Existing trustiness verification methods are effective to obviously malicious HT but no effect on Stealthy Trojan. Stealthy Trojan is an advanced attack form and hard to be detected. In this paper, we analyze the characteristic of stealthy Trojan and propose a static detection method based on feature analysis. The results on ISCAS benchmarks show that the proposed method can detect the Stealthy Trojan node and is convenient to be implanted into other scalable verification framework.
Tahat, Amer, Joshi, Sarang, Goswami, Pronnoy, Ravindran, Binoy.  2019.  Scalable Translation Validation of Unverified Legacy OS Code. 2019 Formal Methods in Computer Aided Design (FMCAD). :1–9.

Formally verifying functional and security properties of a large-scale production operating system is highly desirable. However, it is challenging as such OSes are often written in multiple source languages that have no formal semantics - a prerequisite for formal reasoning. To avoid expensive formalization of the semantics of multiple high-level source languages, we present a lightweight and rigorous verification toolchain that verifies OS code at the binary level, targeting ARM machines. To reason about ARM instructions, we first translate the ARM Specification Language that describes the semantics of the ARMv8 ISA into the PVS7 theorem prover and verify the translation. We leverage the radare2 reverse engineering tool to decode ARM binaries into PVS7 and verify the translation. Our translation verification methodology is a lightweight formal validation technique that generates large-scale instruction emulation test lemmas whose proof obligations are automatically discharged. To demonstrate our verification methodology, we apply the technique on two OSes: Google's Zircon and a subset of Linux. We extract a set of 370 functions from these OSes, translate them into PVS7, and verify the correctness of the translation by automatically discharging hundreds of thousands of proof obligations and tests. This took 27.5 person-months to develop.

Chondamrongkul, Nacha, Sun, Jing, Wei, Bingyang, Warren, Ian.  2019.  Parallel Verification of Software Architecture Design. 2019 IEEE 19th International Symposium on High Assurance Systems Engineering (HASE). :50–57.
In the component-based software system, certain behaviours of components and their composition may affect system reliability at runtime. This problem can be early detected through the automated verification of software architecture design, by which model checking is one of the techniques to achieve this. However, its practicality and performance issue remain challenges. This paper presents a scalable approach for the software architecture verification. The modelling is proposed to manifest the behaviours in the software component, in order to detect problematic behaviours, such as circular dependency and performance bottleneck. The outcome of the verification identifies the problem and the scenarios that cause it. In order to mitigate the verification performance issue, the parallelism is applied to the verification process so that multiple decomposed models can be simultaneously verified on a multi-threaded environment. As some software systems are designed as the monolithic architecture, we present a method that helps to automatically decompose a large monolithic model into a set of smaller sub-models. Our approach was evaluated and proved to enhance the performance of the verification process for the large-scale complex software systems.
Noori-Hosseini, Mona, Lennartson, Bengt.  2019.  Incremental Abstraction for Diagnosability Verification of Modular Systems. 2019 24th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA). :393–399.
In a diagnosability verifier with polynomial complexity, a non-diagnosable system generates uncertain loops. Such forbidden loops are in this paper transformed to forbidden states by simple detector automata. The forbidden state problem is trivially transformed to a nonblocking problem by considering all states except the forbidden ones as marked states. This transformation is combined with one of the most efficient abstractions for modular systems called conflict equivalence, where nonblocking properties are preserved. In the resulting abstraction, local events are hidden and more local events are achieved when subsystems are synchronized. This incremental abstraction is applied to a scalable production system, including parallel lines where buffers and machines in each line include some typical failures and feedback flows. For this modular system, the proposed diagnosability algorithm shows great results, where diagnosability of systems including millions of states is analyzed in less than a second.
Goli, Mehran, Drechsler, Rolf.  2019.  Scalable Simulation-Based Verification of SystemC-Based Virtual Prototypes. 2019 22nd Euromicro Conference on Digital System Design (DSD). :522–529.
Virtual Prototypes (VPs) at the Electronic System Level (ESL) written in SystemC language using its Transaction Level Modeling (TLM) framework are increasingly adopted by the semiconductor industry. The main reason is that VPs are much earlier available, and their simulation is orders of magnitude faster in comparison to the hardware models implemented at lower levels of abstraction (e.g. RTL). This leads designers to use VPs as reference models for an early design verification. Hence, the correctness assurance of these reference models (VPs) is critical as undetected faults may propagate to less abstract levels in the design process, increasing the fixing cost and effort. In this paper, we propose a novel simulation-based verification approach to automatically validate the simulation behavior of a given SystemC VP against both the TLM-2.0 rules and its specifications (i.e. functional and timing behavior of communications in the VP). The scalability and the efficiency of the proposed approach are demonstrated using an extensive set of experiments including a real-word VP.
Gajavelly, Raj Kumar, Baumgartner, Jason, Ivrii, Alexander, Kanzelman, Robert L., Ghosh, Shiladitya.  2019.  Input Elimination Transformations for Scalable Verification and Trace Reconstruction. 2019 Formal Methods in Computer Aided Design (FMCAD). :10–18.
We present two novel sound and complete netlist transformations, which substantially improve verification scalability while enabling very efficient trace reconstruction. First, we present a 2QBF variant of input reparameterization, capable of eliminating inputs without introducing new logic and without complete range computation. While weaker in reduction potential, it yields up to 4 orders of magnitude speedup to trace reconstruction when used as a fast-and-lossy preprocess to traditional reparameterization. Second, we present a novel scalable approach to leverage sequential unateness to merge selective inputs, in cases greatly reducing netlist size and verification complexity. Extensive benchmarking demonstrates the utility of these techniques. Connectivity verification particularly benefits from these reductions, up to 99.8%.
Gulzar, Muhammad Ali.  2018.  Interactive and Automated Debugging for Big Data Analytics. Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings. :509-511.

An abundance of data in many disciplines of science, engineering, national security, health care, and business has led to the emerging field of Big Data Analytics that run in a cloud computing environment. To process massive quantities of data in the cloud, developers leverage Data-Intensive Scalable Computing (DISC) systems such as Google's MapReduce, Hadoop, and Spark. Currently, developers do not have easy means to debug DISC applications. The use of cloud computing makes application development feel more like batch jobs and the nature of debugging is therefore post-mortem. Developers of big data applications write code that implements a data processing pipeline and test it on their local workstation with a small sample data, downloaded from a TB-scale data warehouse. They cross fingers and hope that the program works in the expensive production cloud. When a job fails or they get a suspicious result, data scientists spend hours guessing at the source of the error, digging through post-mortem logs. In such cases, the data scientists may want to pinpoint the root cause of errors by investigating a subset of corresponding input records. The vision of my work is to provide interactive, real-time and automated debugging services for big data processing programs in modern DISC systems with minimum performance impact. My work investigates the following research questions in the context of big data analytics: (1) What are the necessary debugging primitives for interactive big data processing? (2) What scalable fault localization algorithms are needed to help the user to localize and characterize the root causes of errors? (3) How can we improve testing efficiency during iterative development of DISC applications by reasoning the semantics of dataflow operators and user-defined functions used inside dataflow operators in tandem? To answer these questions, we synthesize and innovate ideas from software engineering, big data systems, and program analysis, and coordinate innovations across the software stack from the user-facing API all the way down to the systems infrastructure.

Hazari, S. S., Mahmoud, Q. H..  2019.  A Parallel Proof of Work to Improve Transaction Speed and Scalability in Blockchain Systems. 2019 IEEE 9th Annual Computing and Communication Workshop and Conference (CCWC). :0916-0921.

A blockchain is a distributed ledger forming a distributed consensus on a history of transactions, and is the underlying technology for the Bitcoin cryptocurrency. However, its applications are far beyond the financial sector. The transaction verification process for cryptocurrencies is much slower than traditional digital transaction systems. One approach to increase transaction speed and scalability is to identify a solution that offers faster Proof of Work. In this paper, we propose a method for accelerating the process of Proof of Work based on parallel mining rather than solo mining. The goal is to ensure that no more than two or more miners put the same effort into solving a specific block. The proposed method includes a process for selection of a manager, distribution of work and a reward system. This method has been implemented in a test environment that contains all the characteristics needed to perform Proof of Work for Bitcoin and has been tested, using a variety of case scenarios, by varying the difficulty level and number of validators. Preliminary results show improvement in the scalability of Proof of Work up to 34% compared to the current system.

Kulik, T., Tran-Jørgensen, P. W. V., Boudjadar, J., Schultz, C..  2018.  A Framework for Threat-Driven Cyber Security Verification of IoT Systems. 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). :89-97.

Industrial control systems are changing from monolithic to distributed and interconnected architectures, entering the era of industrial IoT. One fundamental issue is that security properties of such distributed control systems are typically only verified empirically, during development and after system deployment. We propose a novel modelling framework for the security verification of distributed industrial control systems, with the goal of moving towards early design stage formal verification. In our framework we model industrial IoT infrastructures, attack patterns, and mitigation strategies for countering attacks. We conduct model checking-based formal analysis of system security through scenario execution, where the analysed system is exposed to attacks and implement mitigation strategies. We study the applicability of our framework for large systems using a scalability analysis.

Plasencia-Balabarca, F., Mitacc-Meza, E., Raffo-Jara, M., Silva-Cárdenas, C..  2018.  Robust Functional Verification Framework Based in UVM Applied to an AES Encryption Module. 2018 New Generation of CAS (NGCAS). :194-197.

This Since the past century, the digital design industry has performed an outstanding role in the development of electronics. Hence, a great variety of designs are developed daily, these designs must be submitted to high standards of verification in order to ensure the 100% of reliability and the achievement of all design requirements. The Universal Verification Methodology (UVM) is the current standard at the industry for the verification process due to its reusability, scalability, time-efficiency and feasibility of handling high-level designs. This research proposes a functional verification framework using UVM for an AES encryption module based on a very detailed and robust verification plan. This document describes the complete verification process as done in the industry for a popular module used in information-security applications in the field of cryptography, defining the basis for future projects. The overall results show the achievement of the high verification standards required in industry applications and highlight the advantages of UVM against System Verilog-based functional verification and direct verification methodologies previously developed for the AES module.

Chen, G., Wang, D., Li, T., Zhang, C., Gu, M., Sun, J..  2018.  Scalable Verification Framework for C Program. 2018 25th Asia-Pacific Software Engineering Conference (APSEC). :129-138.

Software verification has been well applied in safety critical areas and has shown the ability to provide better quality assurance for modern software. However, as lines of code and complexity of software systems increase, the scalability of verification becomes a challenge. In this paper, we present an automatic software verification framework TSV to address the scalability issues: (i) the extended structural abstraction and property-guided program slicing to solve large-scale program verification problem, saving time and memory without losing accuracy; (ii) automatically select different verification methods according to the program and property context to improve the verification efficiency. For evaluation, we compare TSV's different configurations with existing C program verifiers based on open benchmarks. We found that TSV with auto-selection performs better than with bounded model checking only or with extended structural abstraction only. Compared to existing tools such as CMBC and CPAChecker, it acquires 10%-20% improvement of accuracy and 50%-90% improvement of memory consumption.