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.     

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.     

A fuzzy logic system based on Schweizer-Sklar t-norm

In recent years, the basic research of fuzzy logic and fuzzy reasoning is growing ac- tively day by day, such as the basic logic system BL proposed by Hajek[1]; fuzzy logic system MTL proposed by Esteva and Godo[2]; fuzzy reasoning, implication operators …     

Partiality and Nondeterminacy in Program Proofs

Specifications and programs make much use of nondeterministic and/or partial expressions, i.e. expressions which may yield several or no outcomes for some values of their free variables. Traditional 2-valued logics do not comfortably accommodate reasoning about undefined expressions, and do not cater at all for nondeterministic expressions. We seek to rectify this with a 4-valued typed logic E4 which classifies formulae as either “true”, “false”, “neither true nor false”, or “possibly true, possibly false”. The logic is derived in part from the 2-valued logic E and the 3-valued LPF, and preserves most of the theorems of E. Indeed, the main result is that nondeterminacy can be added to a logic covering partiality at little cost. Received July 1996 / Accepted in revised form April 1998     

A Compositional Natural Semantics and Hoare Logic for Low-Level Languages

The advent of proof-carrying code has generated significant interest in reasoning about low-level languages. It is widely believed that low-level languages with jumps must be difficult to reason about by being inherently non-modular. We argue that this is untrue. We take it seriously that, differently from statements of a high-level language, pieces of low-level code are multiple-entry and multiple-exit. And we define a piece of code to consist of either a single labelled instruction or a finite union of pieces of code. Thus we obtain a compositional natural semantics and a matching Hoare logic for a basic low-level language with jumps. By their simplicity and intuitiveness, these are comparable to the standard natural semantics and Hoare logic of While. The Hoare logic is sound and complete wrt. the semantics and allows for compilation of proofs of the Hoare logic of While.     

A low-level memory model and an accompanying reachability predicate

Reasoning about program heap, especially if it involves handling unbounded, dynamically heap-allocated data structures such as linked lists and arrays, is challenging. Furthermore, sound analysis that precisely models heap becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software. The reachability predicate has already proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. In this paper, we present a memory model suitable for reasoning about low-level pointer operations that is accompanied by a formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present our experience with a prototype verifier on a set of illustrative C benchmarks.     

Mantaining Dynamic Matrices for Fully Dynamic Transitive Closure

In this paper we introduce a general framework for casting fully dynamic transitive closure into the problem of reevaluating polynomials over matrices. With this technique, we improve the best known bounds for fully dynamic transitive closure. In particular, we devise a deterministic algorithm for general directed graphs that achieves O(n ²) amortized time for updates, while preserving unit worst-case cost for queries. In case of deletions only, our algorithm performs updates faster in O(n) amortized time. We observe that fully dynamic transitive closure algorithms with O(1) query time maintain explicitly the transitive closure of the input graph, in order to answer each query with exactly one lookup (on its adjacency matrix). Since an update may change as many as Ω(n ²) entries of this matrix, no better bounds are possible for this class of algorithms. This work has been partially supported by the Sixth Framework Programme of the EU under contract number 507613 (Network of Excellence “EuroNGI: Designing and Engineering of the Next Generation Internet”), and number 001907 (“DELIS: Dynamically Evolving, Large Scale Information Systems”), and by the Italian Ministry of University and Research (Project “ALGO-NEXT: Algorithms for the Next Generation Internet and Web: Methodologies, Design and Experiments”). Portions of this paper have been presented at the 41st Annual Symp. on Foundations of Computer Science, 2000.     

Occlusion Boundaries from Motion: Low-Level Detection and?Mid-Level Reasoning

The boundaries of objects in an image are often considered a nuisance to be “handled” due to the occlusion they exhibit. Since most, if not all, computer vision techniques aggregate information spatially within a scene, information spanning these boundaries, and therefore from different physical surfaces, is invariably and erroneously considered together. In addition, these boundaries convey important perceptual information about 3D scene structure and shape. Consequently, their identification can benefit many different computer vision pursuits, from low-level processing techniques to high-level reasoning tasks. While much focus in computer vision is placed on the processing of individual, static images, many applications actually offer video, or sequences of images, as input. The extra temporal dimension of the data allows the motion of the camera or the scene to be used in processing. In this paper, we focus on the exploitation of subtle relative-motion cues present at occlusion boundaries. When combined with more standard appearance information, we demonstrate these cues’ utility in detecting occlusion boundaries locally. We also present a novel, mid-level model for reasoning more globally about object boundaries and propagating such local information to extract improved, extended boundaries.     

Connecting Polygonizations via Stretches and Twangs

We show that the space of polygonizations of a fixed planar point set S of n points is connected by O(n ²) “moves” between simple polygons. Each move is composed of a sequence of atomic moves called “stretches” and “twangs,” which walk between weakly simple “polygonal wraps” of S. These moves show promise to serve as a basis for generating random polygons.     

Bounded underapproximations

We show a new and constructive proof of the following language-theoretic result: for every context-free language L, there is a bounded context-free language L′⊆L which has the same Parikh (commutative) image as L. Bounded languages, introduced by Ginsburg and Spanier, are subsets of regular languages of the form w₁^*w₂^*?w_m^*w_{1}^{*}w_{2}^{*}\cdots w_{m}^{*} for some w ₁,…,w _m ∈Σ ^∗. In particular bounded context-free languages have nice structural and decidability properties. Our proof proceeds in two parts. First, we give a new construction that shows that each context free language L has a subset L _N that has the same Parikh image as L and that can be represented as a sequence of substitutions on a linear language. Second, we inductively construct a Parikh-equivalent bounded context-free subset of L _N .     

ISO/IEC standardization of identity management and privacy technologies

To cover projects in the area of identity management, privacy, and biometrics ISO/IEC JTC 1/ SC 27 “IT Security techniques” in 2006 established Working Group 5 “Identity Management and Privacy Technologies”. This text describes the reasoning to have this Working Group within SC 27 and introduces WG 5 and its projects.     

The completeness and applications of the formal system ℒ<Superscript>*</Superscript>

Since the formal deductive system ℒ^* was built up in 1997, in has played important roles in the theoretical and applied research of fuzzy logic and fuzzy reasoning. But, up to now, the completeness problem of the system ℒ^* is still an open problem. In this paper, the properties and structure ofR ₀ algebras are further studied, and it is shown that every tautology on theR ₀ interval [0,1] is also a tautology on anyR ₀ algebra. Furthermore, based on the particular structure of ℒ^*-Lindenbaum algebra, the completeness and strong completeness of the system ℒ^* are proved. Some applications of the system ℒ^* in fuzzy reasoning are also discussed, and the obtained results and examples show that the system ℒ^* is suprior to some other important fuzzy logic systems.     

Proving Resource Consumption of Low-level Programs Using Automated Theorem Provers

In this paper we use a program logic and automatic theorem provers to certify resource usage of low-level bytecode programs equipped with annotations describing resource consumption for methods. We have adapted an existing resource counting logic [Aspinall, D., L. Beringer, M. Hofmann, H.-W. Loidl and A. Momigliano, A program logic for resource verification, in: Proceedings of 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004), Lecture Notes in Computer Science 3223 (2004), pp. 34–49] to fit the first-order setting, implemented a verification condition generator, and tested our approach on programs that contain recursion and deal with recursive data structures. We have successfully applied our framework to programs that did not involve any updates to recursive data structures. But mutation is more tricky because of aliasing of heap. We discuss problems related to this and suggest techniques to solve them.     

Hume box calculus: robust system development through software transformation

Hume is a contemporary programming language oriented to systems with strong resource bounds, based on autonomous concurrent “boxes” interacting across “wires”. Hume’s design reflects the explicit separation of coordination and computation aspects of multi-process systems, which greatly eases establishing resource bounds for programs. However, coordination and computation are necessarily tightly coupled in reasoning about Hume programs. Furthermore, in Hume, local changes to coordination or computation, while preserving input/output correctness, can have profound and unforeseen effects on other aspects of programs such as timing of events and scheduling of processes. Thus, traditional program calculi prove inappropriate as they tend to focus exclusively either on the coordination of interacting processes or on computation within individual processes.     

Input-to-State Stability for Nonlinear Time-Varying Systems via Averaging

 We introduce two definitions of an averaged system for a time-varying ordinary differential equation with exogenous disturbances (“strong average” and “weak average”). The class of systems for which the strong average exists is shown to be strictly smaller than the class of systems for which the weak average exists. It is shown that input-to-state stability (ISS) of the strong average of a system implies uniform semi-global practical ISS of the actual system. This result generalizes the result of [TPA] which states that global asymptotic stability of the averaged system implies uniform semi-global practical stability of the actual system. On the other hand, we illustrate by an example that ISS of the weak average of a system does not necessarily imply uniform semi-global practical ISS of the actual system. However, ISS of the weak average of a system does imply a weaker semi-global practical “ISS-like” property for the actual system when the disturbances w are absolutely continuous and . ISS of the weak average of a system is shown to be useful in a stability analysis of time-varying cascaded systems. Date received: April 6, 1999. Date revised: April 11, 2000.     

Heap-Bounded Assembly Language

We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of different types. Linear typing ensures the single pointer property, disallowing aliasing but allowing safe, in-place-update compilation of programming languages. We prove that HBAL is sound for a low-level untyped model of the machine, using a satisfiability relation that captures when a location correctly models a value of some type. This interpretation is closer to the machine than previous abstract machines used for typed assembly language models, and we separate typing of the store from an untyped operational semantics of programs, as would be required for proof-carrying code. Our ultimate aim is to design a family of assembly languages that have high-level typing features for expressing resource-bound constraints. We want to link the assembly-level with high-level languages expressing similar constraints, to provide end-to-end guarantees and a viable framework for proof-carrying code. HBAL is a first exemplifying step in this direction. It is designed as a target low-level language for Hofmann's LFPL language. Programs written in LFPL run in a bounded amount of heap space, and this property carries over when they are compiled to HBAL: the resulting program does not allocate store or assume an external garbage collector. Following LFPL, we include a special diamond resource type that stands for a unit of heap space of uncommitted type.     

Proving the shalls

Incomplete, inaccurate, ambiguous, and vola-tile requirements have plagued the software industry since its inception. The convergence of model-based development and formal methods offers developers of safety-critical systems a powerful new approach to the early validation of requirements. This paper describes an exercise conducted to determine if formal methods could be used to validate system requirements early in the lifecycle at reasonable cost. Several hundred functional and safety requirements for the mode logic of a typical flight guidance system were captured as natural language “shall” statements. A formal model of the mode logic was written in the RSML^−e language and translated into the NuSMV model checker and the PVS theorem prover using translators developed as part of the project. Each “shall” statement was manually translated into a NuSMV or PVS property and proven using these tools. Numerous errors were found in both the original requirements and the RSML^−e model. This demonstrates that formal models can be written for realistic systems and that formal analysis tools have matured to the point where they can be effectively used to find errors before implementation. This project was partially funded by the NASA Langley Research Center under contract NCC1-01001 of the Aviation Safety Program.     

A compositional natural semantics and Hoare logic for low-level languages

The advent of proof-carrying code has generated significant interest in reasoning about low-level languages. It is widely believed that low-level languages with jumps must be difficult to reason about because of being inherently non-modular. We argue that this is untrue. We take it seriously that, unlike statements of a high-level language, pieces of low-level code are multiple-entry and multiple-exit. And we define a piece of code as consisting of either a single labelled instruction or a finite union of pieces of code. Thus we obtain a compositional natural semantics and a matching Hoare logic for a basic low-level language with jumps. By their simplicity and intuitiveness, these are comparable to the standard natural semantics and Hoare logic of While. The Hoare logic is sound and complete wrt the semantics and allows for compilation of proofs of the Hoare logic of While.