Fusion is an indispensable tool in the arsenal of techniques for program derivation. Less well-known, but equally valuable is type fusion, which states conditions for fusing an application of a functor with an initial algebra to form another initial algebra. We provide a novel proof of type fusion based on adjoint folds and discuss several applications: type firstification, type specialisation and tabulation.
A tool for performance evaluation will be presented in this paper. The tool is named BAL and is based on the timed process algebra BTC incorporating resources as well. BAL begins by first making the syntactic analysis of the system specification, and then draws up its relevant transition graph by applying the rules of the operational semantics and solves a performance optimization problem relevant to optimize of the maximum throughout. Usage of BAL tool is illustrated on a Flexible Manufacturing Systems (FMS) to find a suitable number of resources/machines to maximize system throughput.
Maude modules can be understood as models that can be formally analyzed and verified with respect to different properties expressing various formal requirements. However, Maude lacks the formal tools to perform some of these analyses and thus they can only be done by hand. The Heterogeneous Tool Set Hets is an institution-based combination of different logics and corresponding rewriting, model checking and proof tools. We present in this paper an integration of Maude into Hets that allows to use the logics and tools already integrated in Hets with Maude specifications. To achieve such integration we have defined an institution for Maude based on preordered algebras and a comorphism between Maude and CASL, the central logic in HETS.
Visibly pushdown Kleene algebra is an algebraic system using only propositional reasoning while still being able to represent well-known constructs of programming languages (sequences, alternatives, loops and code blocks) in a natural way. In this paper, this system is used to verify the following interprocedural compiler optimizations: interprocedural dead code elimination, inlining of functions, tail-recursion elimination, procedure reordering and function cloning. The proofs are equational and machine-verifiable.
We present a declarative debugger for Maude specifications that allows to debug wrong answers (a wrong result is obtained) and missing answers (a correct but incomplete result is obtained) due to both wrong and missing statements and wrong search conditions. The debugger builds a tree representing the computation and guides the user through it to find the bug. We present the debugger’s latest commands and features, illustrating its use with several examples.
This paper presents a theoretical framework for the integration of the cooperative constraint solving of several algebraic domains into higher-order functional and logic programming on λ-abstractions, using an instance of a generic Constraint Functional Logic Programming (CFLP) scheme over a so-called higher-order coordination domain. We provide this framework as a powerful computational model for the higherorder cooperation of algebraic constraint domains over real numbers and integers, which has been useful in practical applications involving the hybrid combination of its components, so that more declarative and efficient solutions can be promoted. Our proposal of computational model has been proved sound and complete with respect to the declarative semantics provided by the CFLP scheme, and enriched with new mechanisms for modeling the intended cooperation among the algebraic domains and a novel higher-order constraint domain equipped with a sound and complete constraint solver for solving higher-order equations. We argue the applicability of our approach describing a prototype implementation on top of the constraint functional logic system TOY
We present an assume-guarantee method for the verification of quantified array assertions based on a program transformation. A quantified array assertion expresses a property over an array segment such as "all elements of an array are sorted". Given a program Pn annotated with assertion ϕn, our method rewrites Pn to either P n -1; C or C ; P n -1 where C is a code fragment. The validity of the assertion is then proven by induction: assuming that ϕ n -1 holds for P n -1 and proving that ϕ n holds for P n . The program transformation allows to reduce the complexity of the code as well as the assertion to be verified. Experimental results on both text book and real life examples taken from system code show performance improvement compared to our previous approach for checking quantified assertions. Moreover, this new technique enables us to verify challenging programs which are not handled by our previous method and many exiting tools as well.
We develop an algebraic modal logic that combines epistemic and dynamic modalities with a view to modelling information acquisition (learning) by automated agents in a changing world. Unlike most treatments of dynamic epistemic logic, we have transitions that "change the state" of the underlying system and not just the state of knowledge of the agents. The key novel feature that emerges is the need to have a way of "inverting transitions" and distinguishing between transitions that "really happen" and transitions that are possible. Our approach is algebraic, rather than being based on a Kripke-style semantics. The semantics are given in terms of quantales. We study a class of quantales with the appropriate inverse operations and prove properties of the setting. We illustrate the ideas with toy robot-navigation problems. These illustrate how an agent learns information by taking actions.
The paper shows how to refine large-scale or even infinite transition systems so as to ensure certain desired properties. First, a given system is reduced into a smallish, finite bisimulation quotient. Second, the reduced system is refined in order to ensure a given property, using any known finite-state method. Third, the refined reduced system is expanded back into an adequate refinement of the system given initially. The proposed method is based on a Galois connection between systems and their quotients. It is applicable to various models and bisimulations and is illustrated with a few qualitative and quantitative properties.
This paper introduces matching logic, a novel framework for defining axiomatic semantics for programming languages, inspired from operational semantics. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called patterns. Program configurations satisfy patterns iff they match their algebraic structure and satisfy their constraints. Using a simple imperative language (IMP), it is shown that a restricted use of the matching logic proof system is equivalent to IMP's Hoare logic proof system, in that any proof derived using either can be turned into a proof using the other. Extensions to IMP including a heap with dynamic memory allocation and pointer arithmetic are given, requiring no extension of the underlying first-order logic; moreover, heap patterns such as lists, trees, queues, graphs, etc., are given algebraically using fist-order constraints over patterns.
MU-TERM is a tool which can be used to verify a number of termination properties of (variants of) Term Rewriting Systems (TRSs): termination of rewriting, termination of innermost rewriting, termination of order-sorted rewriting, termination of context-sensitive rewriting, termination of innermost context-sensitive rewriting and termination of rewriting modulo specific axioms. Such termination properties are essential to prove termination of programs in sophisticated rewriting-based programming languages. Specific methods have been developed and implemented in mu-term in order to efficiently deal with most of them. In this paper, we report on these new features of the tool.
Program calculation, being a programming technique that derives programs from specification by means of formula manipulation, is a challenging activity. It requires human insights and creativity, and needs systems to help human to focus on clever parts of the derivation by automating tedious ones and verifying correctness of transformations. Different from many existing systems, we show in this paper that Coq, a popular theorem prover, provides a cheap way to implement a powerful system to support program calculation, which has not been recognized so far. We design and implement a set of tactics for the Coq proof assistant to help the user to derive programs by program calculation and to write proofs in calculational form. The use of these tactics is demonstrated through program calculations in Coq based on the theory of lists.
We investigate the expressiveness of two classical distributed paradigms by defining the first encoding of the pure mobile ambient calculus into the synchronous π-calculus. Our encoding, whose correctness has been proved by relying on the notion of operational correspondence , shows how the hierarchical ambient structure can be reformulated within a flat channel interconnection amongst independent processes, without centralised control. To easily handle the computation for simulating a capability, we introduce the notions of simulating trace (representing the computation that a π-calculus process has to execute to mimic a capability) and of aborting trace (representing the computation that a π-calculus process executes when the simulation of a capability cannot succeed). Thus, the encoding may introduce loops, but, as it will be shown, the number of steps of any trace, therefore of any aborting trace, is limited, and the number of states of the transition system of the encoding processes still remains finite. In particular, an aborting trace makes a sort of backtracking, leaving the involved sub-processes in the same starting configurations. We also discuss two run-time support methods to make these loops harmless at execution time. Our work defines a relatively simple, direct, and precise translation that reproduces the ambient structure by means of channel links, and keeps track of the dissolving of an ambient.
Stochastic process algebra models have been successfully used in the area of performance modelling for the last twenty years, and more recently have been adopted for modelling biochemical processes in systems biology. Most research on these modelling formalisms has been on quantitative analysis, particularly the derivation of quantified dynamic information about the system modelled in the face of the state space explosion problem. In this paper we instead consider qualitative analysis, looking at how recent developments to tackle state space explosion in quantified analysis can be also harnessed to establish properties such as freedom from deadlock in an efficient manner.
We present a static analysis technique for modeling and approximating the long-run resource usage of programs. The approach is based on a quantitative semantic framework where programs are represented as linear operators over dioids. We provide abstraction techniques for such linear operators which make it feasible to compute safe over-approximations of the long-run cost of a program. A theorem is proved stating that such abstractions yield correct approximations of the program’s long-run cost. These approximations are effectively computed as the eigenvalue of the matrix representation of the abstract semantics. The theoretical developments are illustrated on a concrete example taken from the analysis of the cache behaviour of a simple bytecode language.
In this paper, we present a novel approach that establishes a synergy between static and dynamic analyses for detecting memory errors in C code. We extend the standard C type system with effect, region, and host annotations that are relevant to memory management. We define static memory checks to detect memory errors using these annotations. The statically undecidable checks are delegated to dynamic code instrumentation to secure program executions. The static analysis guides its dynamic counterpart by locating instrumentation points and their execution paths. Our dynamic analysis instruments programs with in-lined monitors that observe program executions and ensure safe-fail when encountering memory errors. We prototype our approach by extending the GCC compiler with our type system, a dynamic monitoring library, and code instrumentation capabilities.
Variants of causal functions on streams are defined, and the interplay between them is studied from different perspectives with attention to coalgebraic considerations. We prove that the sets of causal and bicausal functions, respectively, are closed under a certain natural coinductive construction. This closure property paves the way to constructing new final stream coalgebras over finite alphabets. This result is used to show that the 2-adic version of the Collatz function yields a final bit-stream coalgebra.
The real world is inherently concurrent and temporal. For simulating physical phenomena of the real world, one prefers frameworks which easily express concurrency and account for the passage of time. We propose Orc, a structured concurrent calculus, as a framework for writing simulations. Orc provides constructs to orchestrate the concurrent invocation of services while managing time-outs, priorities, and failures of services or communication. Orc's treatment of time is of particular interest in simulation. We propose an abstract notion of time and show its utility in coding simulations. We also show how Orc's structure allows us to compute statistics from a simulation.
This paper gives a correctness proof for the on-chip COMA cache coherence protocol that supports the Microgrid of microthreaded architecture, a multi-core architecture capable of integrating hundreds to hundreds of thousands of processors on single silicon chip. We use the Abstract State Machine (ASM) as a theoretical framework for the specification of the on-chip COMA cache coherence protocol. We show that the protocol obeys the Location Consistency model proposed by Gao and Sakar.
