VLISP: A verified implementation of Scheme

The VLISP project showed how to produce a comprehensively verified implementation for a programming language, namely Scheme. This paper introduces two more detailed studies on VLISP [13, 21]. It summarizes the basic techniques that were used repeatedly throughout the effort. It presents scientific conclusions about the applicability of the these techniques as well as engineering conclusions about the crucial choices that allowed the verification to succeed.The work reported here was carried out as part of The MITRE Corporation's Technology Program, under funding from Rome Laboratory, Electronic Systems Command, United States Air Force, through contract F19628-89-C-0001. Preparation of this paper was generously supported by The MITRE Corporation. Mitchell Wand's participation was partly supported by NSF and DARPA under NSF grants CCR-9002253 and CCR-9014603.     

The VLISP verified Scheme system

The VLISP project has produced a rigorously verified compiler from Scheme to byte codes, and a verified interpreter for the resulting byte codes. The official denotational semantics for Scheme provides the main criterion of correctness. The Wand-Clinger technique was used to prove correctness of the primary compiler step. Then a state machine operational semantics is proved to be faithful to the denotational semantics. The remainder of the implementation is verified by a succession of state machine refinement proofs. These include proofs that garbage collection is a sound implementation strategy, and that a particular garbage collection algorithm is correct.The work reported here was carried out as part of The MITRE Corporation's Technology Program, under funding from Rome Laboratory, Electronic Systems Command, United States Air Force, through contract F19628-89-C-0001. Preparation of this paper was generously supported by The MITRE Corporation.     

Enveloping sophisticated tools into process-centered environments

We present a tool integration strategy based on enveloping pre-existing tools without source code modifications or recompilation, and without assuming an extension language, application programming interface, or any other special capabilities on the part of the tool. This Black Box enveloping (or wrapping) idea has existed for a long time, but was previously restricted to relatively simple tools. We describe the design and implementation of, and experimentation with, a new Black Box enveloping facility intended for sophisticated tools—with particular concern for the emerging class of groupware applications.This work was conducted while Mr. Valetto was a graduate student at Columbia University. Prof. Kaiser was supported in part by Advanced Research Project Agency Order B128 monitored by Air Force Rome Lab F30602-94-C-0197, in part by National Science Foundation CCR-9301092, in part by the New York State Science and Technology Foundation Center for Advanced Technology in High Performance Computing and Communications in Healthcare 94013, and in part by grants from AT&T Foundation, Bull HN Information Systems and IBM Canada Ltd. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the US or NYS governments, ARPA, Air Force, NSF, NYSSTF, AT&T, Bull, IBM or Xerox.     

Measuring the cost of storage management

We study the cost of storage management for garbage-collected programs compiled with the Standard ML of New Jersey compiler. We show that the cost of storage management is not the same as the time spent garbage collecting. For many of the programs, the time spent garbage collecting is less than the time spent doing other storage-management tasks.This research was sponsored by the Defense Advanced Research Projects Agency, DoD, through ARPA Order 8313, and monitored by ESD/AVS under contract F19628-91-C-0168. Views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the United States Government. David Tarditi was also supported by an AT&T PhD Scholarship. Amer Diwan was also supported by National Science Foundation Grant CCR-9211272.     

Proof rules for the programming language Euclid

Summary In the spirit of the previous axiomatixation of the programming language Pascal, this paper describes Hoare-style proof rules for Euclid, a programming language intended for the expression of system programs which are to be verified. All constructs of Euclid are covered except for storage allocation and machine dependencies.Supported by the Defense Advanced Research Projects Agency under contract DAHC-15-72-C-0308Supported in part by the National Science Foundation under grant MCS-76-86089 and the Joint Services Electronics Program monitored by the Air Force Office of Scientific Research under contract F44620-76-C-0061Supported in part by a Research Leave Grant from the University of Toronto and a grant from the National Research Council of Canada.Supported in part by the Defense Advanced Research Projects Agency under contract DAHC 73-C-0368. The views expressed are those of the authors     

Automated Analysis of Fault-Tolerance in Distributed Systems

A method for automated analysis of fault-tolerance of distributed systems is presented. It is based on a stream (or data-flow) model of distributed computation. Temporal (ordering) relationships between messages received by a component on different channels are not captured by this model. This makes the analysis more efficient and forces the use of conservative approximations in analysis of systems whose behavior depends on such inter-channel orderings. To further support efficient analysis, our framework includes abstractions for the contents, number, and ordering of messages sent on each channel. Analysis of a reliable broadcast protocol illustrates the method.Supported in part by NSF under Grant CCR-9876058 and ONR under Grants N00014-99-1-0358, N00014-01-1-0109, and N00014-02-1-0363.Supported in part by ARPA/RADC grant F30602-96-1-0317, AFOSR grant F49620-00-1-0198, Defense Advanced Research Projects Agency (DARPA) and Air Force Research Laboratory Air Force Material Command USAF under agreement number F30602-99-1-0533, National Science Foundation Grant 9703470, and a grant from Intel Corporation. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of these organizations or the U.S. Government.Some of the material contained herein previously appeared in [32]     

Local decomposition of gray-scale morphological templates

Template decomposition techniques can be useful for improving the efficiency of imageprocessing algorithms. The improved efficiency can be realized either by reorganizing a computation to fit a specialized structure, such as an image-processing pipeline, or by reducing the number of operations used. In this paper two techniques are described for decomposing templates into sequences of 3×3 templates with respect to gray-scale morphological operations. Both techniques use linear programming and are guaranteed to find a decomposition of one exists.This work was supported in part by the U.S. Air Force Armament Laboratory of Eglin Air Force Base under contract F08635-89-C-0134.     

Multi-stack-counter languages

A stack-counter acceptor is a stack acceptor in which the storage alphabet is just one letter. The present paper discusses multi-stack-counter acceptors operating in quasirealtime, i.e., acceptors in which each storage tape is a stack counter and in which there are only a bounded number of consecutive-moves. For each positive integerk let be the family of languages accepted byk-stack-counter acceptors (k-counter acceptors). Each is a principal AFL closed under reversal but not under-free substitution or under intersection. Also, and a specific language in each, is exhibited. For each and there are noi andj such that. It is shown that a quasi-real-timek-stackcounter acceptor is equivalent to one operating in non-deterministic real time. Lastly, it is shown that acceptance by final state of ak-stack-counter acceptor is equivalent to acceptance by empty tape and final state.Also formerly with System Development Corporation, Santa Monica, California. Research sponsored in part by the Air Force Cambridge Research Laboratories, Office of Aerospace Research, USAF, under Contract F19628-70-C-0023; by the Air Force Office of Scientific Research, Office of Aerospace Research, USAF, under AFOSR No. F44620-70-C-0013; and by NSF Grant No. GJ454.     

Quasi-realtime languages

The quasi-realtime languages are seen to be the languages accepted by nondeterministic multitape Turing machines in real time. The family of quasi-realtime languages forms an abstract family of languages closed under intersection, linear erasing, and reversal. It is identical with the family of languages accepted by nondeterministic multitape Turing machines in linear time. Every quasi-realtime language can be accepted in real time by a nondeterministic one stack, one pushdown store machine, and can be expressed as the length-preserving homomorphic image of the intersection of three context-free languages.The research reported in this paper was announced at the ACM Symposium on the Theory of Computing, Marina del Rey, California, May, 1969. This research has been supported in part by Air Force Cambridge Research Laboratories, Office of Aerospace Research, USAF, under Contract F19628-68-C-0029.     

Constructing the Voronoi diagram of a set of line segments in parallel

In this paper we give a parallel algorithm for constructing the Voronoi diagram of a polygonal scene, i.e., a set of line segments in the plane such that no two segments intersect except possibly at their endpoints. Our algorithm runs inO(log² n) time usingO(n) processors in the CREW PRAM model.The research of M. T. Goodrich was supported by NSF under Grants CCR-8810568 and CCR-9003299 and by NSF/DARPA under Grant CCR-8908092. C. K. Yap's research was supported in part by NSF Grants DCR-8401898 and CCR-9002819.     

Constructing invariants for hybrid systems

We present a new method for generating algebraic invariants of hybrid systems. The method reduces the invariant generation problem to a constraint solving problem using techniques from the theory of ideals over polynomial rings. Starting with a template invariant—a polynomial equality over the system variables with unknown coefficients—constraints are generated on the coefficients guaranteeing that the solutions are inductive invariants. To control the complexity of the constraint solving, several stronger conditions that imply inductiveness are proposed, thus allowing a trade-off between the complexity of the invariant generation process and the strength of the resulting invariants. This research was supported in part by NSF grants CCR-01-21403, CCR-02-20134 and CCR-02-09237, by ARO grant DAAD19-01-1-0723, by ARPA/AF contracts F33615-00-C-1693 and F33615-99-C-3014, and by NAVY/ONR contract N00014-03-1-0939.     

A strongly competitive randomized paging algorithm

Thepaging problem is that of deciding which pages to keep in a memory ofk pages in order to minimize the number of page faults. We develop thepartitioning algorithm, a randomized on-line algorithm for the paging problem. We prove that its expected cost on any sequence of requests is within a factor ofH _k of optimum. (H _k is thekth harmonic number, which is about ln(k).) No on-line algorithm can perform better by this measure. Our result improves by a factor of two the best previous algorithm.Partial support for D. D. Sleator was provided by DARPA, ARPA Order 4976, Amendment 20, monitored by the Air Force Avionics Laboratory under Contract F33615-87-C-1499, and by the National Science Foundation under Grant CCR-8658139.     

A theory of nonmonotonic rule systems II

Conclusions We have proved a number of results on nonmonotonic rule systems. This theory allows us to capture many constructions appearing in the current literature on the logical foundations of artificial intelligence.Our results provide additional tools tying these constructs with traditional methods of logic and recursion theory.In a sequel we shall deal with rule systems containing variables in the rules and with predicate logics. We shall prove results related to the properties of recursive systems that are not necessarily highly recursive. We shall also explore connections with.Work partially supported by NSF grant RII-86-10671 and Kentucky EPSCoR program and ARO contract DAAL03-89-K-0124.Work partially supported by NSF grant DMS-89-02797 and ARO contract DAAG629-85-C-0018.Work partially supported by NSF grants DMS-87-02473 and DMS-90-06413.     

A mechanically verified language implementation

This paper briefly describes a programming language, its implementation on a microprocessor via a compiler and link-assembler, and the mechanically checked proof of the correctness of the implementation. The programming language, called Piton, is a high-level assembly language designed for verified applications and as the target language for high-level language compilers. It provides executeonly programs, recursive subroutine call and return, stack based parameter passing, local variables, global variables and arrays, a user-visible stack for intermediate results, and seven abstract data types including integers, data addresses, program addresses and subroutine names. Piton is formally specified by an interpreter written for it in the computational logic of Boyer and Moore. Piton has been implemented on the FM8502, a general purpose microprocessor whose gate-level design has been mechanically proved to implement its machine code interpreter. The FM8502 implementation of Piton is via a function in the Boyer-Moore logic which maps a Piton initial state into an FM8502 binary core image. The compiler and link-assembler are both defined as functions in the logic. The implementation requires approximately 36K bytes and 1400 lines of prettyprinted source code in the Pure Lisp-like syntax of the logic. The implementation has been mechanically proved correct. In particular, if a Piton state can be run to completion without error, then the final values of all the global data structures can be ascertained from an inspection of an FM8502 core image obtained by running the core image produced by the compiler and link-assembler. Thus, verified Piton programs running on FM8502 can be thought of as having been verified down to the gate level.This work was supported in part by the Defense Advanced Research Projects Agency under DARPA Orders 6082 and 9151, contract MDA904-87-C-H009.     

Extended parallelism in the Gröbner basis algorithm

This paper presents a new parallel implementation to compute Gröbner bases utilizing two different forms of parallelism. A coarse-grain technique developed by Jean-Phillipe Vidal expands and reducesS-polynomials in parallel. A finegrain technique, proposed by Melenk and Neun, constructs a pipeline of processors to overlap execution of the reduction operations. A hybrid algorithm that outperforms both of the original approaches is presented. The combined algorithm requires the user to select the appropriate allocation of processors to the two styles of parallelism, and uses this static assignment throughout the computation. The paper also discusses the design and implementation approaches used to construct an efficient version of this algorithm.The author was partially supported by an NSF graduate fellowship. This research was sponsored in part by the Avionics Laboratory, Wright Research and Development Center, Aeronautical Systems Division (AFSC), U.S. Air Force, Wright-Patterson AFB, Ohio 45433-6543 under Contract F33615-90-C-1465, ARPA Order No. 7597 and in part by the National Science Foundation under grant CCR-87-226-33. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of the National Science Foundation or the U.S. government.     

A comparison of simulation techniques and algebraic techniques for verifying concurrent systems

Simulation-based assertional techniques and process algebraic techniques are two of the major methods that have been proposed for the verification of concurrent and distributed systems. It is shown how each of these techniques can be applied to the task of verifying systems described as input/output automata; both safety and liveness properties are considered. A small but typical circuit is verified in both of these ways, first using forward simulations, an execution correspondence lemma, and a simple fairness argument, and second using deductions within the process algebra DIOA for I/O automata. An extended evaluation and comparison of the two methods is given.Supported by NSF grant CCR-89-15206, by DARPA contracts N00014-89-J-1988 and N00014-92J-4033, and by ONR contract N00014-91-J-1046.     

Design of a multimedia object-oriented DBMS

The emerging multimedia information (such as video, image, voice, graphics) services have imposed many new requirements and research considerations on the design of database management systems (DBMSs). Conventionally, a multimedia DBMS is designed by developing a multimedia presentation layer on top of a pre-existing object-oriented DBMS (which can be truly object-oriented or relational-based), such that the core of the DBMS was developed earlier independent of the design of the multimedia presentation layer. Due to the fact that multimedia capabilities are not actually embedded in the DBMSs, such systems tend to provide only a rather limited set of functionalities in multimedia and are not satisfactory in supporting multimedia applications. This paper describes some key features of a multimedia object-oriented DBMS that is currently being developed. In this system the DBMS is carefully redesigned to provide special multimedia capabilities, such that the mismatch between the DBMS and the multimedia application layer can be eliminated. In particular, this paper will focus on unique multimedia capabilities including multimedia object modeling, video data management, and distributed collaboration. This project was supported in part by Rome Laboratory, U.S. Air Force under the contract no. F30602-94-C-0090     

A formalization of priority inversion

A priority inversion occurs when a low-priority task causes the execution of a higher-priority task to be delayed. The possibility of priority inversions complicates the analysis of systems that use priority-based schedulers because priority inversions invalidate the assumption that a task can be delayed by only higher-priority tasks. This paper formalizes priority inversion and gives sufficient conditions as well as some new protocols for preventing priority inversions.Supported by the Commission of the European Communities under the ESPRIT Programme Basic Research Action Number 3092 (Predictably Dependable Computing Systems) and the Italian Ministry of Research and University, and in part by the Defense Advanced Research Projects Agency (DoD) under NASA Ames grant number NAG-2-593.Supported in part by the Defense Advanced Research Projects Agency (DoD) under NASA Ames grant number NAG 2-593, and by grants from IBM T.J. Watson Research Laboratory, the IBM Endicott Programming Laboratory, Siemens RTL, and Xerox Webster Research Center.Supported in part by the Office of Naval Research under contract N00014-91-J-1219, the National Science Foundation under Grant No. CCR-8701103, DARPA/NSF Grant No. CCR-9014363, and by the IBM Endicott Programming Laboratory.     

GSTE is partitioned model checking

Verifying whether an ω-regular property is satisfied by a finite-state system is a core problem in model checking. Standard techniques build an automaton with the complementary language, compute its product with the system, and then check for emptiness. Generalized symbolic trajectory evaluation (GSTE) has been recently proposed as an alternative approach, extending the computationally efficient symbolic trajectory evaluation (STE) to general ω-regular properties. In this paper, we show that the GSTE algorithms are essentially a partitioned version of standard symbolic model-checking (SMC) algorithms, where the partitioning is driven by the property under verification. We export this technique of property-driven partitioning to SMC and show that it typically does speed up SMC algorithms. A shorter version of this paper has been presented at CAV’04 (R. Sebastiani et al., Lecture Notes in Comput. Sci., vol. 3114, pp. 143–160, 2004). R. Sebastiani supported in part by the CALCULEMUS! IHP-RTN EC project, code HPRN-CT-2000-00102, by a MIUR COFIN02 project, code 2002097822_003, and by a grant from the Intel Corporation. M.Y. Vardi supported in part by NSF grants CCR-9988322, CCR-0124077, CCR-0311326, IIS-9908435, IIS-9978135, EIA-0086264, and ANI-0216467 by BSF grant 9800096, and by a grant from the Intel Corporation.