Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

We present a fully abstract weakest precondition calculus and its integration with symbolic execution. Our assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from a specific implementation of object creation. Objects which are not (yet) created never play any role. The corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and proof rules is illustrated with an example of a linked list reachability property. All proof rules presented are fully implemented in a version of the KeY verification system for Java programs.     

Implementing Coloured Petri Nets Using a Functional Programming Language

Coloured Petri Nets (CPNs) are a graphically oriented modelling language for concurrent systems based on Petri Nets and the functional programming language Standard ML. Petri Nets provide the primitives for modelling concurrency and synchronisation. Standard ML provides the primitives for modelling data manipulation and for creating compact and parameterisable CPN models.Functional programming and Standard ML have played a major role in the development of CPNs and the CPN computer tools supporting modelling, simulation, verification, and performance analysis of concurrent systems. At the modelling language level, Standard ML has extended Petri Nets with the practical expressiveness required for modelling systems of the size and complexity found in typical industrial projects. At the implementation level, Standard ML has been used to implement the formal semantics of CPNs that provide the theoretical foundation of the CPN computer tools.This paper provides an overview of how functional programming and Standard ML are applied in the CPN modelling language and the supporting computer tools. We give a detailed presentation of the key algorithms and techniques used for implementing the formal semantics of CPNs, and we survey a number of case studies where CPNs have been used for the design and analysis of systems. We also demonstrate how the use of a Standard ML programming environment has allowed Petri Nets to be used for the implementation of systems.     

An Introduction to IN CAPS System

INCAPS，a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System,The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program‘s correctness which are supported respectively by the mechanized logics-FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system:the rules,implementation,tactics,forward proof and backward proof.It also gives several typical examples for demonstration of INCAPS‘ working principle.The achievement to data in that we have now accomplished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.     

Formulae Meet Programs Over the Net: A Framework for Correct Network Aware Programming

A general framework for network aware programming is presented that consists of a language for programming mobile applications, a logic for specifying properties of the applications and an automatic tool for verifying such properties. The framework is based on X-KLAIM, eXtended KLAIM, an experimental programming language specifically designed to program distributed systems composed of several components interacting through multiple tuple spaces and mobile code. The proposed logic is a modal logic inspired by Hennessy-Milner logic and is interpreted over the same labelled structures used for the operational semantics of X-KLAIM. The automatic verification tool is based on a complete proof system that has been previously developed for the logic.     

Mechanically verifying concurrent programs with the Boyer-Mooreprover

A proof system suitable for the mechanical verification of concurrent programs is described. This proof system is based on Unity, and may be used to specify and verify both safety and liveness properties. However, it is defined with respect to an operational semantics of the transition system model of concurrency. Proof rules are simply theorems of this operational semantics. This methodology makes a clear distinction between the theorems in the proof system and the logical inference rules and syntax which define the underlying logic. Since this proof system essentially encodes Unity in another sound logic, and this encoding has been mechanically verified, this encoding proves the soundness of this formalization of Unity. This proof system has been mechanically verified by the Boyer-Moore prover. This proof system has been used to mechanically verify the correctness of a distributed algorithm that computes the minimum node value in a tree     

Type theory and concurrency

This paper describes the use of an automated reasoning tool, the Nuprl system, to formalize Milner's Calculus of Communicating Systems (CCS). The goals of this work are two-fold: the first is to investigate the feasibility of using systems like Nuprl to handle the formal detail arising from reasoning about concurrency, while the second is to develop a framework in which various formalisms for reasoning about concurrency may be presented in an automated fashion. To these ends, an implementation in Nuprl of a formal theory of concurrency is described, an implementation of CCS in this mechanized semantic theory presented, and two means of analyzing CCS terms are investigated.     

A Correspondence between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems

In Russell's Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church's simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT.Despite the disappearance of orders which have a strong correlation with predicativity, predicative logic still plays an influential role in Computer Science.An important example is the proof checker Nuprl, which is basedon Martin-Löf's Type Theory which uses type universes. Those type universes,and also degrees of expressions in AUTOMATH, are closely related toorders. In this paper, we show that orders have not disappeared frommodern logic and computer science, rather, orders play a crucial role in understanding the hierarchy of modern systems. In order to achieve our goal, we concentrate on a subsystem of Nuprl.The novelty of our paper lies in: (1) a modest revival of Russell'sorders, (2) the placing of the historical system RTTunderlying the famous Principia Mathematica in a context with a modernsystem of computer mathematics (Nuprl) and modern type theories(Martin-Löf's type theory and PTSs), and (3) the presentation of acomplex type system (Nuprl) as a simple and compact PTS.     

同步数据流语言高阶运算消去的可信翻译

Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.     

NuMDG: A New Tool for Multiway Decision Graphs Construction

Multiway Decision Graphs(MDGs) are a canonical representation of a subset of many-sorted first-order logic. This subset generalizes the logic of equality with abstract types and uninterpreted function symbols.The distinction between abstract and concrete sorts mirrors the hardware distinction between data path and control.Here we consider ways to improve MDGs construction.Efficiency is achieved through the use of the Generalized-If-Then-Else(GITE) commonly operator in Binary Decision Diagram packages.Consequently,we review the main algorithms used for MDGs verification techniques.In particular,Relational Product and Pruning by Subsumption are algorithms defined uniformly through this single GITE operator which will lead to a more efficient implementation.Moreover,we provide their correctness proof.This work can be viewed as a way to accommodate the ROBBD algorithms to the realm of abstract sorts and uninterpreted functions.The new tool,called NuMDG,accepts an extended SMV language,supporting abstract data sorts.Finally,we present experimental results demonstrating the efficiency of the NuMDG tool and evaluating its performance using a set of benchmarks from the SMV package.     

A temporal logic approach to object certification

A brief overview is made of the use of temporal logic formalisms for specifying and verifying concurrent systems in general and information systems in particular. The requirements imposed by object-orientation on such formalisms are examined. A logic is proposed fulfilling those requirements (except concerning non-monotonic features), allowing the uniform treatment of both local and global properties of systems with concurrent, interacting components organized in classes, and supporting specialization. A semantics and a calculus (following an axiomatic, Hilbert style) are presented in detail. The calculus includes rules for the sound inheritance and reflection of theorems between classes. Practical aspects of the usage of such a logic for both specification and verification are considered. To this end a set of metatheorems is provided for expediting the proof of invariants. Finally, the need and availability of automatic theorem proving for systems querying is briefly discussed.     

A methodology for efficient hardware verification

We present a methodology which helps structure the design and verification of hardware circuits. Our methodology supports reusable proofs of hardware components, provides for multiple implementations of the same specification, and allows both bottom up and top down verification styles. We provide mechanical assistance for our methodology in the Nuprl proof development system. Our method exploits Nuprl's rich type theory to encode the specification of a module in the type of the module. This allows us to elegantly describe parameterized hardware modules. The methodology is efficient because: the automated support reduces the amount of information that users must provide and the use of parameterized hardware modules eliminates redundant reasoning among proofs of hardware components. In this paper we explain our methodology and illustrate our approach with several examples of circuit verification.     

Applying Formal Methods to a Certifiably Secure Software System

A major problem in verifying the security of code is that the code's large size makes it much too costly to verify in its entirety. This paper describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, a compact security model containing only information needed to reason about the security properties of interest is constructed and the security properties are represented formally in terms of the model. To reduce the cost of verification, the code to be verified is partitioned into three categories and only the first category, which is less than 10 percent of the code in our application, requires formal verification. The proof of the other two categories is relatively trivial. Our approach was developed to support a common criteria evaluation of the separation kernel of an embedded software system. This paper describes 1) our techniques and theory for verifying the kernel code and 2) the artifacts produced, that is, a top-level specification (TLS), a formal statement of the security property, a mechanized proof that the TLS satisfies the property, the partitioning of the code, and a demonstration that the code conforms to the TLS. This paper also presents the formal basis for the argument that the kernel code conforms to the TLS and consequently satisfies the security property.     

Verifying Contextual Refinement with Ownership Transfer

Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.However,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and clients.In this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer.We also design a program logic to verify contextual refinement of concurrent objects w.r.t.their abstract specifications.We have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.     

Dependent Types for Program Termination Verification

Program termination verification is a challenging research subject of significant practical importance. While there is already a rich body of literature on this subject, it is still undeniably a difficult task to design a termination checker for a realistic programming language that supports general recursion. In this paper, we present an approach to program termination verification that makes use of a form of dependent types developed in Dependent ML (DML), demonstrating a novel application of such dependent types to establishing a liveness property. We design a type system that enables the programmer to supply metrics for verifying program termination and prove that every well-typed program in this type system is terminating. We also provide realistic examples, which are all verified in a prototype implementation, to support the effectiveness of our approach to program termination verification as well as its unobtrusiveness to programming. The main contribution of the paper lies in the design of an approach to program termination verification that smoothly combines types with metrics, yielding a type system capable of guaranteeing program termination that supports a general form of recursion (including mutual recursion), higher-order functions, algebraic datatypes, and polymorphism.     

Metalogical Frameworks II: Developing a Reflected Decision Procedure

Proving theorems is a creative act demanding new combinations of ideas and on occasion new methods of argument. For this reason, theorem proving systems need to be extensible. The provers should also remain correct under extension, so there must be a secure mechanism for doing this. The tactic-style provers pioneered by Edinburgh LCF provide a very effective way to achieve secure extensions, but in such systems, all new methods must be reduced to tactics. This is a drawback because there are other useful proof generating tools such as decision procedures; these include, for example, algorithms which reduce a deduction problem, such as arithmetic provability, to a computation on graphs.The Nuprl system pioneered the combination of fixed decision procedures with tactics, but the issue of securely adding new ones was not solved. In this paper we show how to safely include user- defined decision procedures in theorem provers. The idea is to prove properties of the procedure inside the prover's logic and then invoke a reflection rule to connect the procedure to the system. We also show that using a rich underlying logic permits an abstract account of the approach so that the results carry over to different implementations and other logics.