Compositional verification of sequential programs with procedures

We present a method for algorithmic, compositional verification of control-flow-based safety properties of sequential programs with procedures. The application of the method involves three steps: (1) decomposing the desired global property into local properties of the components, (2) proving the correctness of the property decomposition by using a maximal model construction, and (3) verifying that the component implementations obey their local specifications. We consider safety properties of both the structure and the behaviour of program control flow. Our compositional verification method builds on a technique proposed by Grumberg and Long that uses maximal models to reduce compositional verification of finite-state parallel processes to standard model checking. We present a novel maximal model construction for the fragment of the modal μ-calculus with boxes and greatest fixed points only, and adapt it to control-flow graphs modelling components described in a sequential procedural language. We extend our verification method to programs with private procedures by defining an abstraction, presented as an inlining transformation. All algorithms have been implemented in a tool set automating all required verification steps. We validate our approach on an electronic purse case study.     

Formal verification of concurrent programs with read-write locks

Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms. This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.     

Automatic verification of Java programs with dynamic frames

Framing in the presence of data abstraction is a challenging and important problem in the verification of object-oriented programs Leavens et al. (Formal Aspects Comput (FACS) 19:159–189, 2007). The dynamic frames approach is a promising solution to this problem. However, the approach is formalized in the context of an idealized logical framework. In particular, it is not clear the solution is suitable for use within a program verifier for a Java-like language based on verification condition generation and automated, first-order theorem proving. In this paper, we demonstrate that the dynamic frames approach can be integrated into an automatic verifier based on verification condition generation and automated theorem proving. The approach has been proven sound and has been implemented in a verifier prototype. The prototype has been used to prove correctness of several programming patterns considered challenging in related work.     

Formal verification of concurrent programs with read-write locks

Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms.This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.     

Automatic verification of functional programs

We propose an approach to verification of functional programs based on an example of methods and tools developed in functional programming. The program verification procedures and tools developed in the framework of this approach are described.Translated from Kibernetika, No. 4, pp. 30–39, July–August, 1990.     

Formal verification of Ada programs

The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that one can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy     

Generalised multi-pattern-based verification of programs with linear linked structures

The paper deals with the problem of automatic verification of programs working with extended linear linked dynamic data structures, in particular, pattern-based verification is considered. In this approach, one can abstract memory configurations by abstracting away the exact number of adjacent occurrences of certain memory patterns. With respect to the previous work on the subject the method presented in the paper has been extended to be able to handle multiple patterns, which allows for verification of programs working with more types of structures and/or with structures with irregular shapes. The experimental results obtained from a prototype implementation of the method show that the method is very competitive and offers a big potential for future extensions.     

Towards deductive verification of C programs with shared data

This paper considers the problem of the deductive verification of the Linux kernel code that is concurrent and accesses shared data. The presence of shared data does not allow applying traditional deductive verification techniques, so we consider how to verify such a code by proving its compliance to a given specification of a certain synchronization discipline. The approach is illustrated by the examples of a spinlock specification and a simplified specification of the read-copy-update (RCU) API.     

Contract-based verification of MATLAB-style matrix programs

MATLAB/Simulink is a popular toolset for developing embedded software. The main target of the toolset is numerical computing applications and the tools offer a rich language for manipulating matrices. This paper presents an approach to automatic, modular, contract-based verification of programs written in a subset of the MATLAB programming language. We focus on efficient handling of the built-in matrix manipulation functions commonly used in MATLAB. We restrict ourselves to the subset of MATLAB suitable for code generation, which means matrix types and shapes can be determined statically. We present an approach to static type and shape inference for matrices that is more strict than MATLAB, but aids verification. The type and shape information is then used in the verification. From the programs and contracts we generate verification conditions that are discharged with an off-the-shelf SMT solver. We discuss two approaches to encode matrix functions and evaluate them on a number of examples. We also investigate the use of k-induction to decrease the need for user annotations. We found our approach to be efficient for programs that manipulate relatively small matrices, which are common in embedded applications.     

Relational interprocedural verification of concurrent programs

We propose a general analysis method for recursive, concurrent programs that track effectively procedure calls and return in a concurrent context, even in the presence of unbounded recursion and infinite-state variables like integers. This method generalizes the relational interprocedural analysis of sequential programs to the concurrent case, and extends it to backward or coreachability analysis. We implemented it for programs with scalar variables and experimented with several classical synchronization protocols in order to illustrate the precision of our technique and also to analyze the approximations it performs.     

Modular specification and verification of object-oriented programs

A method for modular specification and verification using the ideas of subtype and normal type is presented. The method corresponds to informal techniques used by object-oriented programmers. The key idea is that objects of a subtype must behave like objects of that type's supertypes. An example program is used to show the reasoning problems that supertype abstraction may cause and how the method resolves them. Subtype polymorphism is addressed, and specification and verification update is discussed. A set of syntactic and semantic constraints on subtype relationships, which formalize the intuition that each object of a subtype must behave like some object of each of its supertypes, is examined. These constraints are the key to the soundness of the method. To state them precisely, a formal model of abstract type specifications is used     

On construction and verification of PLC programs

A review of methods and approaches for programming of “discrete” problems for programmable logic controllers (PLC) based on the example of constructing a program for controlling a code lock. The usability of the analysis of a program correctness by the model checking method with respect to a Cadence SMV automatic verification tool is evaluated for these approaches. Possible PLC program vulnerabilities arising at some approaches for programming of PLC are revealed.     

Region analysis for deductive verification of C programs

This paper presents a memory model with nonoverlapping memory areas (regions) for the deductive verification of C programs. This memory model uses a core language that supports arbitrary nesting of structures, unions, and arrays into other structures and allows reducing the number of user-provided annotations as a result of region analysis. This paper also describes semantics of the core language and normalizing transformations for translating an input annotated C program into a program in the core language. In addition, an encoding is proposed for modeling the memory state of a core-language program with logical formulas as described by the model semantics of the core language. For the model semantics, the soundness and completeness theorems are proved. Additional constraints on the typing context of the core-language terms are described that determine the result of the region analysis enabling the complete modeling of a limited class of programs without using additional annotations. A proof sketch for the theorem stating completeness of the proposed region analysis for a limited class of programs is presented.     

Automated verification of pointer programs in pointer logic

Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic-Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool-plcc was implemented to automatically verify a number of non-trivial pointer programs.     

AutoProof: auto-active functional verification of object-oriented programs

Auto-active verifiers provide a level of automation intermediate between fully automatic and interactive: users supply code with annotations as input while benefiting from a high level of automation in the back-end. This paper presents AutoProof, a state-of-the-art auto-active verifier for object-oriented sequential programs with complex functional specifications. AutoProof fully supports advanced object-oriented features and a powerful methodology for framing and class invariants, which make it applicable in practice to idiomatic object-oriented patterns. The paper focuses on describing AutoProof ’s interface, design, and implementation features, and demonstrates AutoProof ’s performance on a rich collection of benchmark problems. The results attest AutoProof ’s competitiveness among tools in its league on cutting-edge functional verification of object-oriented programs.     

Automated verification of pointer programs in pointer logic

Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic – Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool – plcc was implemented to automatically verify a number of non-trivial pointer programs.     

命令式程序终止性验证方法综述

作为软件完全正确性的重要组成部分,程序终止性受到越来越多的关注。旨在跟踪国内外针对命令式程序的终止性验证方法,调研该领域的最新研究成果,同时提出解决该问题的建议性方法框架,对命令式程序终止性研究提供有意义的帮助。给出了程序终止性问题的定义,介绍了已有的数值程序、堆操作程序终止性验证方法,并分别进行了分析与对比。总结了当前研究中存在的难点与热点问题,给出了一种基于模型检验的C程序终止性验证框架,该框架可以作为研究命令式程序终止性的基本框架。