This volume contains papers selected from the contributionsto the 4th International workshop on Graph Grammars andTheir Application to Computer Science. It is intended toprovide a rich source of information on t...
详细信息
ISBN:
(数字)9783540383956
ISBN:
(纸本)9783540544784
This volume contains papers selected from the contributions
to the 4th International workshop on Graph Grammars and
Their Application to Computer Science. It is intended to
provide a rich source of information on the stateof the art
and newest trends to researchers active in the area and for
scientists who would like to know more about graph grammars.
The topics of the papers range from foundations through
algorithmic and implemental aspects to various issues that
arise in application areas like concurrent computing,
functional and logicprogramming, software engineering,
computer graphics, artificial intelligence and biology. The
contributing authors are F.-J. Brandenburg, H. Bunke, T.C.
Chen, M. Chytil, B. Courcelle, J. Engelfriet, H. G|ttler, A.
Habel, D. Janssens, C. Lautemann, B. Mayoh, U. Montanari,
M. Nagl, F. Parisi-Presicci, A. Paz, P. Prusinkiewics, M.R.
Sleep, A. Rosenfeld, J. Winkowski and others.
The theory of institutions formalizes the intuitive notion of a "logical system." Institutions were introduced (1) to support as much computer science as possible independently of the underlying logical syst...
详细信息
ISBN:
(纸本)9783540171621
The theory of institutions formalizes the intuitive notion of a "logical system." Institutions were introduced (1) to support as much computer science as possible independently of the underlying logical system, (2) to facilitate the transfer of results (and artifacts such as theorem provers) from one logical system to another, and (3) to permit combining a number of different logical systems. In particular, programming-in-the-large (in the style of the Clear specification language) is available for any specification or "logical" programming language based upon a suitable institution. Available features include generic modules, module hierarchies, "data constraints" (for data abstraction), and "multiplex" institutions (for combining multiple logical systems). The basic components of an institution are: a category of signatures (which generally provide symbols for constructing sentences);a set (or category) of Σ-sentences for each signature Σ;a category (or set) of Σ-models for each Σ;and a Σ-satisfaction relation, between Σ-sentences and Σ-models, for each Σ. The intuition of the basic axiom for institutions is that truth (i.e., satisfaction) is invariant under change of notation. This paper enriches institutions with sentence morphisms to model proofs, and uses this to explicate the notion of a logical programming language. To ease constructing institutions, and to clarify various notions, this paper introduces two further concepts. A charter consists of an adjunction, a "base" functor, and a "ground" object;we show that "chartering" is a convenient way to "found" institutions. Parchments provide a notion of sentential syntax, and a simple way to "write" charters and thus get institutions. Parchments capture the insight that the syntax of logic is an initial algebra. Everything is illustrated with the many-sorted equational institution. Parchments also explicate the sense of finitude that is appropriate for specifications. Finally, we introduce generalized instituti
Abstract interpretation is a compile-time technique which is used to gain information about a program that may then be used to optimise the execution of the program. A particular use of abstract interpretation is in s...
详细信息
The Extended ML specification language provides a framework for the formal stepwise development of modular programs in the Standard ML programming language from specifications. The object of this paper is to equip Ext...
详细信息
We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a λ-calculus equi...
详细信息
We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a λ-calculus equipped with refinement types for expressing pre- and post-conditions within first-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates verification conditions that are passed to an SMT solver. We describe a series of checked examples. This is the first tool to verify authentication properties of cryptographic protocols by typechecking their source code.
Methods for proving that concurrent software does not leak its secrets has remained an active topic of research for at least the past four decades. Despite an impressive array of work, the present situation remains hi...
详细信息
ISBN:
(数字)9781728165721
ISBN:
(纸本)9781728165738
Methods for proving that concurrent software does not leak its secrets has remained an active topic of research for at least the past four decades. Despite an impressive array of work, the present situation remains highly unsatisfactory. With contemporary compositional proof methods one is forced to choose between expressiveness (the ability to reason about a wide variety of security policies), on the one hand, and precision (the ability to reason about complex thread interactions and program behaviours), on the other. Achieving both is essential and, we argue, requires a new style of compositional reasoning. We present VERONICA, the first program logic for proving concurrent programs information flow secure that supports compositional, high-precision reasoning about a wide range of security policies and program behaviours (e.g. expressive declassification, value-dependent classification, secret-dependent branching). Just as importantly, VERONICA embodies a new approach for engineering such logics that can be re-used elsewhere, called decoupled functional correctness (DFC). DFC leads to a simple and clean logic, even while achieving this unprecedented combination of features. We demonstrate the virtues and versatility of VERONICA by verifying a range of example programs, beyond the reach of prior methods.
暂无评论