As neural networks (NNs) are increasingly introduced into safety-critical domains, there is a growing need to formally verify NNs before deployment. In this work we focus on the formal verification problem of NN equivalence which aims to prove that two NNs (e.g. an original and a compressed version) show equivalent behavior. Two approaches have been proposed for this problem: Mixed integer linear programming and interval propagation. While the first approach lacks scalability, the latter is only suitable for structurally similar NNs with small weight changes.The contribution of our paper has four parts. First, we show a theoretical result by proving that the epsilon-equivalence problem is coNP-complete. Secondly, we extend Tran et al.’s single NN geometric path enumeration algorithm to a setting with multiple NNs. In a third step, we implement the extended algorithm for equivalence verification and evaluate optimizations necessary for its practical use. Finally, we perform a comparative evaluation showing use-cases where our approach outperforms the previous state of the art, both, for equivalence verification as well as for counter-example finding.

This paper proposes an approach for a tool-agnostic and heterogeneous static code analysis toolchain in combination with an exchange format. This approach enhances both traceability and comparability of analysis results. State of the art toolchains support features for either test execution and build automation or traceability between tests, requirements and design information. Our approach combines all those features and extends traceability to the source code level, incorporating static code analysis. As part of our approach we introduce the "ASSUME Static Code Analysis tool exchange format" that facilitates the comparability of different static code analysis results. We demonstrate how this approach enhances the usability and efficiency of static code analysis in a development process. On the one hand, our approach enables the exchange of results and evaluations between static code analysis tools. On the other hand, it enables a complete traceability between requirements, designs, implementation, and the results of static code analysis. Within our approach we also propose an OSLC specification for static code analysis tools and an OSLC communication framework.

Automatic heuristic configuration and algorithm selection can tremendously improve performance in industrial use-cases of SAT solving. In contrast to attempting to select the best heuristic for the problem, portfolio approaches in parallel SAT solving run different heuristics and even algorithms in parallel. This kind of diversification can be very successful because different heuristics and heuristic configurations have better runtimes on different problems. However, such approaches often suffer from high memory consumption. We present a parallel portfolio SAT solver that is based on several totally different branching heuristics and configurations. In contrast to similar approaches, our portfolio solver uses a shared clause database. We show how to asynchronously manage concurrent access to a shared clause database in a parallel portfolio of solvers that can also perform inprocessing.

We extract structure from CNF problems using a gate recognition algorithm and perform random simulation on that structure to generate conjectures about literal equivalences and backbone variables. We use these conjectures in two approaches to optimize CDCL SAT solving. In the first approach, we perform under-approximation by adding the conjectures to the original problem, while performing subsequent corrections in a refinement loop. In the second approach, we modify the branching heuristic such that it exploits the conjectures in order to stimulate clause learning. Experimental results show improvements, especially on unsatisfiable circuit-equivalence checking problems.

This paper presents LLBMC, a tool for finding bugs and runtime errors in sequential C/C++ programs. LLBMC employs bounded model checking using an SMT-solver for the theory of bitvectors and arrays and thus achieves precision down to the level of single bits. The two main features of LLBMC that distinguish it from other bounded model checking tools for C/C++ are (i) its bit-precise memory model, which makes it possible to support arbitrary type conversions via stores and loads; and (ii) that it operates on a compiler intermediate representation and not directly on the source code.

Modeling the semantics of programming languages like C for the automated termination analysis of programs is a challenge if complete coverage of all language features should be achieved. On the other hand, low-level intermediate languages that occur during the compilation of C programs to machine code have a much simpler semantics since most of the intricacies of C are taken care of by the compiler frontend. It is thus a promising approach to use these intermediate languages for the automated termination analysis of C programs. In this paper we present the tool KITTeL based on this approach. For this, programs in the compiler intermediate language are translated into term rewrite systems (TRSs), and the termination proof itself is then performed on the automatically generated TRS. An evaluation on a large collection of C programs shows the effectiveness and practicality of KITTeL on "typical" examples.

Bounded model checking-as well as symbolic equivalence checking-are highly successful techniques in the hardware domain. Recently, bit-vector bounded model checkers like CBMC have been developed that are able to check properties of (mostly low-level) software written in C. However, using these tools to check equivalence of software implementations has rarely been pursued. In this case study we tackle the problem of proving the functional equivalence of two implementations of the AES crypto-algorithm using automatic bounded model checking techniques. Cryptographic algorithms heavily rely on bit-level operations, which makes them particularly suitable for bit-precise tools like CBMC. Other software verification tools based on abstraction refinement or static analysis seem to be less appropriate for such software. We could semi-automatically prove equivalence of the first three rounds of the AES encryption routines. Moreover, by conducting a manually assisted inductive proof, we could show equivalence of the full AES encryption process.

Synchronization between component requirements and implementation centric tests remains a challenge that is usually addressed by requirements reviews with testers and traceability policies. The claim of this work is that linking requirements, their scenario-based formalizations, and software verification provides a promising extension to this approach. Formalized scenarios, for example in the form of low-level assume/assert statements in C, are easier to trace to requirements than traditional test sets. For a verification engineer, they offer an opportunity to better participate in requirements changes. Changes in requirements can be more easily propagated because adapting formalized scenarios is often easier than deriving and updating a large set of test cases. The proposed idea is evaluated in a case study encompassing over 50 functional requirements of an automotive software developed at Robert Bosch GmbH. Results indicate that requirement formalization together with formal verification leads to the discovery of implementation problems missed in a traditional testing process.

Abstract Modular software model checking of large real‐world systems is known to require extensive manual effort in environment modelling and preparing source code for model checking. Avinux is a tool chain that facilitates the automatic analysis of Linux and especially of Linux device drivers. The tool chain is implemented as a plugin for the Eclipse IDE, using the source code bounded model checker CBMC as its backend. Avinux supports a verification process for Linux that is built upon specification annotations with SLICx (an extension of the SLIC language), automatic data environment creation, source code transformation and simplification, and the invocation of the verification backend. In this paper technical details of the verification process are presented: Using Avinux on thousands of drivers from various Linux versions led to the discovery of six new errors. In these experiments, Avinux also reduced the immense overhead of manual code preprocessing that other projects incurred. Copyright © 2008 John Wiley & Sons, Ltd.

Configurable software is ubiquitous, and the term software product line (SPL) has been coined for it lately. It remains a challenge, however, how such software can be verified over all variants. Enumerating all variants and analyzing them individually is inefficient, as knowledge cannot be shared between analysis runs. Instead of enumeration we present a new technique called lifting that converts all variants into a meta-program, and thus facilitates the configuration-aware application of verification techniques like static analysis, model checking and deduction-based approaches. As a side-effect, lifting provides a technique for checking software feature models, which describe software variants, for consistency. We demonstrate the feasibility of our approach by checking configuration dependent hazards for the highly configurable Linux kernel which possesses several thousand of configurable features. Using our techniques, two novel bugs in the kernel configuration system were found.

Fully automatic source code analysis tools based on abstract interpretation have become an integral part of the embedded software development process in many companies. And although these tools are of great help in identifying residual errors, they still possess a major drawback: analyzing industrial code comes at the cost of many spurious errors that must be investigated manually. The need for efficient development cycles prohibits extensive manual reviews, however. To overcome this problem, the combination of different software verification techniques has been suggested in the literature. Following this direction, we present a novel approach combining abstract interpretation and source code bounded model checking, where the model checker is used to reduce the number of false error reports. We apply our methodology to source code from the automotive industry written in C, and show that the number of spurious errors emitted by an abstract interpretation product can be reduced considerably.

Storage area networks (SANs) connect storage devices to servers over fast network interconnects. We consider the problem of optimal SAN configuration with the goal of meeting service level agreements (SLAs) for server processes while retaining flexibility for future changes. Our approach proceeds in two stages, by setting up pseudo-Boolean constraint problems and solving them with an off-the-shelf solver. First, we give an algorithm for assigning storage devices to applications running on the SANpsilas hosts. This algorithm tries to balance the workload as evenly as possible over all storage devices. Our second algorithm takes these assignments and computes the interconnections (data paths) that are necessary to achieve the desired configuration while respecting redundancy (safety)requirements in the SLAs. Again, this algorithm tries to balance the workload of all connections and devices in proportion to their capacity. Thus, our network configurations respect all SLAs and provide flexibility for future changes by avoiding bottlenecks on storage devices or switches.

Storage Area Networks (SANs) connect groups of storage devices to servers over fast interconnects. An important challenge lies in managing the complexity of the resulting massive SAN configurations. Policy-based validation using new logical frameworks has been proposed earlier as a solution to this configuration problem. SANchk offers a new solution that uses standard technologies such as SQL, XML, and Java, to implement a rule-based configuration checker. SANchk works as a light-weight extension to the relational databases of storage management systems; current support includes IBM's TPC and the open source Aperi storage manager. Some five dozen best practices rules for SAN configuration are implemented in SANchk, many of them with configurable parameters. Empirical results with several commercial SANs show that the approach is viable in practice.