A modular formalization of the branching time temporal logic CTL is presented. Our formalization subsumes prior formalizations of propositional linear temporal logic (PTL) and computation tree logic (CTL). Moreover, the modularity allows to instantiate our formalization for different formal security models. Validity of axioms and soundness of inference rules in axiomatizations of PTL, UB, CTL, and CTL are discussed as well.
We present modular formalizations of the model specification language Reactive Modules and the temporal logic CTL in the proof assistant Coq. In our formalizations, both shallow and deep embeddings of each language are given. The modularity of our formalizations allows proofs and theorems to be reused across different embeddings. We illustrate the advantages of our modular formalizations by proving the mutual exclusion property of the Bakery algorithm in different embeddings.
The heap, where shared mutable data structures are stored, is notoriously hard to analyze. Unlike the stack, the heap involves more issues such as data sharing, pointer aliasing, memory leak, null-pointer dereferencing, dynamic allocation and deallocation, well-formedness of data structures and etc. To ensure correctness of heap manipulations, a sound and easy-to-use foundation is needed. Separation logic is a program logic that could provide such a foundation. To verify whether a separation logic assertion holds, both deductive methods and algorithmic methods may be utilized. Separation logic can be applied in several domains such as shape analysis, concurrent program analysis and so on. Several tools are developed to support verification tasks in these application domains. In this paper, we review the basics of separation logic, techniques for verifying program properties expressed in separation logic, and applications of separation logic.
The state-explosion problem limits the adoption of model checking in large systems. One approach to alleviate this problem is compositional verification, which reduces the verification problem of a large system to the verification problems of smaller components. For carrying out compositional verification, assume/guarantee (A/G) reasoning is one of the most effective techniques. The main obstacle in adopting A/G reasoning is the need of human intervention to find some auxiliary structures. Recently, automatic approaches for finding the auxiliary structures of several A/G reasoning rules have been proposed. Those approaches, however, consider finite computations only. None of the existing literature has discussed about how to extend those approaches to non-terminating reactive systems. This paper reviews A/G reasoning rules, investigates approaches to automate the compositional verification utilizing those rules and provides some perspectives in extending those approaches to infinite computations.
The “state explosion problem” restrains the adoption of model checking in large scale systems. One approach to alleviate this problem is compositional verification, which reduces the verification problem of a large system into the verification problems of smaller components. The assume-guarantee (A/G) reasoning is one of the most effective approach for compositional verification The main obstacle for adopting A/G reasoning is the need of human intervention in designing some auxiliary structures. Recently, automatic approaches for finding the auxiliary structures of several A/G reasoning rules have been proposed. However, those approaches consider finite computations only. No existing literatures discuss about how to extend those approaches to non terminating reactive systems. This paper investigates A/G reasoning rules, their automation and provides
some perspectives about extending those approaches to infinite computations. Also, we provides two possible application categories in software security that A/G reasoning can apply.
The Open Calculus of Constructions [Ste02] is a type theory in the style of the Calculus of Constructions [CH88] incorporating concepts from Rewriting Logic [OM93]. Based on our exposition in [Sch07], we describe a categorical semantics for a subsystem of OCC, which is obtained quite straightforwardly by enriching a D-category based semantics with a 2-category structure. The resulting semantics is sound and conceivably encompasses a wide variety of different models for the calculus; thus it could serve as a basis for further metatheoretical investigations of OCC and perhaps also related systems.
3rd year External Midterm Review Meeting (2009.01.07)
