Role-based Access Control for Boxed (2008)
Adriana Compagnoni, Elsa L. Gunter, Mariangiola Dezani-ciancaglini
Ronchi Della Rocca on the occasion of their sixtieth birthdays Our society is increasingly moving towards richer forms of information exchange where mobility of processes and devices plays a...
Pseudo-Retract Functors for Local Lattices and Bi nte L-Domains (2007)
Recently, a new category of domains used for the mathematical foundations
Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Pamela Zave
requirements, specifications. We define a reference model for applying formal methods to the development of user requirements and their reduction to behavioral specification of a system. The approach...
Interfacing HOL90 with a Functional Database Query Language (2007)
Abstract. We describe a functional database language OR-SML for handling disjunctive information in database queries, its implementation in Standard ML [10], and its interface to HOL90. The core...
Building HOL90 Everywhere Easily (Well Almost) (2007)
Abstract. We describe how to change HOL90 so that it can build under all operating systems for which a full SML compiler exists. We also discuss some eciencies, particularly separate compilation,...
Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, Pamela Zave
Abstract. In this paper we illustrate the use of formal methods in the development of a benchmark application we call the Village Telephone System which is characteristic of a class of network and...
Some Projects in Reasoning About Specifications With Automated Theorem Provers (2007)
The higher order module system was proven to be a conservative extension of the original first order module system. In the static core, the soundness of instantiating of polymorphic terms was proven...
Types for Security in a Mobile World (2005)
Adriana B. Compagnoni, Elsa L. Gunter
Abstract. Our society is increasingly moving towards richer forms of information exchange where mobility of processes and devices plays a prominent role. This tendency has prompted the academic...
Alur, Rajeev, Arney, David, Gunter, Elsa L., Lee, Insup, Lee, Jaime, Nam, Wonhong, ...
Reliability of medical devices such as the CARA Infusion Pump Control System is of extreme importance given that these devices are being used on patients in critical condition. The Infusion Pump...
Compositional message sequence charts (2001)
Elsa L. Gunter, Anca Muscholl, Doron A. Peled
Abstract. Message sequence charts (MSCs) is a standard notation for describing the interaction between communicating objects. It is popular among the designers of communication protocols. MSCs enjoy...
Compositional message sequence charts (2001)
Elsa L. Gunter, Anca Muscholl, Doron A. Peled
Abstract. Message sequence charts (MSCs) is a standard notation for describing the interaction between communicating objects. It is popular among the designers of communication protocols. MSCs enjoy...
Using Functional Languages in Formal Methods: The Pet System (2000)
Elsa L. Gunter, Doron A. Peled
1 Introduction Formal methods are a collection of techniques aimed at increasing the reliability of software and hardware systems. Since the systems under investigation are often quite complex, the...
While verification methods are becoming more frequently integrated into software development projects, software testing is still the main method used to search for programming errors. Software...
Adding external decision procedures to HOL90 securely (1998)
Abstract. This paper describes a modest conservative extension of HOL90 that allows the results from external decision procedures to be used within HOL90 without compromising its logical consistency....
A Reference Model for Requirements and Specifications (1998)
Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Pamela Zave
We define a reference model for applying formal methods to the development of user requirements and their reduction to behavioral specification of a system. The approach is characterized by its focus...
A Reference Model for Requirements and Specifications (1998)
Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Pamela Zave
We define a reference model for applying formal methods to the development of user requirements and their reduction to behavioral specification of a system. The approach is characterized by its focus...
THE VILLAGE TELEPHONE SYSTEM: A Case Study in Formal Software Engineering (1998)
Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, Pamela Zave
. In this paper we illustrate the use of formal methods in the development of a benchmark application we call the Village Telephone System which is characteristic of a class of network and...
OR-SML: A Functional Database Programming Language for Disjunctive Information (1994)
Gunter, Elsa L, Libkin, Leonid
We describe a functional database language OR-SML for handling disjunctive information in database queries, and its implementation on top of Standard ML. The core language has the power of the nested...
A broader class of trees for recursive type definitions for HOL (1994)
Abstract. In this paper we describe the construction in hol of the inductive type of arbitrarily branching labeled trees. Such a type is characterized by an initiality theorem similar to that for...
An Abstract Interpretation For ML Equality Kinds (1991)
Gunter, Carl A, Gunter, Elsa L, MacQueen, David B
The definition of Standard ML provides a form of generic equality which is inferred for certain types, called equality types, on which it is possible to define an equality relation in ML. However,...
Pseudo-Retract Functors for Local Lattices and Bifinite L-Domains (1989)
Recently, a new category of domains used for the mathematical foundations of denotational semantics, that of L-domains, have been under study. In this paper we consider a related category of posets,...
Doing Algebra in Simple Type Theory (1989)
To fully utilize the power of higher-order logic in interactive theorem proving, it is desirable to be able to develop abstract areas of Mathematics such as algebra and topology in an automated...
Extensions to logic programming motivated by the construction of a generic theorem prover (1989)
In this article, we discuss several possible extensions to traditional logic programming languages. The specic extensions proposed here fall into two categories: logical extensions and the addition...