GLIMPSE SEARCH FOR "UNITY" @Article{Sanders91, title = "Eliminating the Substitution Axiom from {UNITY} Logic", author = "Beverly Sanders", journal = "Formal Aspects of Computing", volume = "3", number = "2", pages = "189--205", year = "1991", } @Article{Staskaukas88, author = "Mark G. Staskaukas", title = "The Formal Specification and Design of a Distributed Electronic Funds-Transfer System", journal = "IEEE Trans. on Computers", volume = "37", number = "12", pages = "1515--1528", month = dec, year = "1988", abstract = "{\bf Abstract:} We present the design of an electronic funds-transfer (EFT) systems using the UNITY parallel programming methodology of Chandy and Misra[3]. We begin with a high-level specification that captures the essence of transaction processing in the system. In a series of refinement steps, this specification is transformed into one that leads directly to a program suitable for execution on the distributed architecture of the EFT system. Each refinement step involves replacing a data structure by a distributed version that can be implemented efficiently on the target architecture. By defining a correspondence between the replaced data structure and its distributed counterpart, we are able to demonstrate formally that each refinement step preserves the intent of the original specification.", } * @TechReport{IB-B921125, author = "U. Fuhrbach", title = "Formal Specification Methods for Reactive Systems", address = "Koblenz", year = "1991", descriptor = "Prozess-Spezifikation, Reaktives System, Formale Spezifikation, Nebenlaeufigkeit", annote = "Uebersicht ueber Spezifikationsformalismen fuer reaktive Systeme: - Uebergangsnetzwerke - Statecharts - Sdl - Petri-Netze - Parallele Prolog-Dialekte - Prozessspezifikation: Csp, Cls, Unity, Lotos, Esterel", } @PhdThesis{And92, author = "{F. Andersen}", title = "A Theorem Prover for {UNITY} in Higher Order Logic", year = "1992", address = "Horsholm, Denmark", month = mar, key = "And92", keyword = "HOL UNITY", owner = "Ralf Reetz", } @InProceedings{AnPP93, author = "{F. Andersen} and {K.D. Petersen} and {J.S. Pettersson}", title = "Program Verification using {HOL-UNITY}", booktitle = "{HUG93}, {HOL} User's Group Workshop", year = "1993", publisher = "Springer Verlag", address = "Vancouver, Canada", month = aug, key = "AnPP93", } @Book{ChMi89, author = "{K.M. Chandy} and {J. Misra}", title = "Parallel Program Design", publisher = "Addison-Wesley", year = "1989", address = "Austin, Texas", month = may, key = "ChMi89", keyword = "UNITY", owner = "Info-Bib: E Cha", } * @TechReport{Hudak88d, author = "P. R. Hudak and R. S. Sundaresh", title = "On the Expressiveness of Purely Functional {I}/{O} Systems", institution = "Yale University, Department of Computer Science", type = "Research Report", number = "YALEU/DCS/RR-665", address = "New Haven, CT", year = "1988", keywords = "input output io haskell systems model non determinism non-determinism", abstract = "Functional programming languages have traditionally lacked complete, flexible, and yet referentially transparent I/O mechanisms. Previous proposals for I/O have used either the notion of lazy streams or continuations to model interaction with the external world. We discuss and generalize these models and introduce a third, which we call the systems model, to perform I/O. The expressiveness of the styles are compared by means of an example. We then give a series of surprisingly simple translations between the three models, demonstrating that they are not as different as their programming styles suggest, and implying that the styles could be mixed within a single program. The need to express non-deterministic behavior in a functional language is well recognized. So is the problem of doing so without destroying referential transparency. We survey past approaches to this problem, and suggest a solution in the context of the I/O models described. The I/O system of the purely functional language Haskell is presented. The system includes a rich set of operations, and distinguishes between file and channel I/O. The approach to non-determinism is also presented. A useful aspect of the design is that it includes a rigorous specification of the behavior of the operating system, thus precisely fixing the semantics of the various I/O operations. The Haskell I/O system is capable of supporting may other paradigms of concurrent computation in a natural way. We demonstrate this through the emulation of Actors, UNITY, CSP, CCS and Linda.", } * BIBLIOGRAPHY ON PROTEIN (DNA) PATTERN MATCHING (REFS: 379) @Article{Singh1, author = "A. K. Singh and R. Overbeek", title = "Derivation of efficient parallel programs: An example from Genetic Sequence Analysis", journal = "International Journal of Parallel Programming", volume = "18", pages = "447--484", year = "1989", comment = "A parallel version of the standard dynamic programming algorithm is used as an example to developing parallel programs using unity.", } @TechReport{MIT/LCS/TM-400, author = "M. F. Nour", title = "An Automata-Theoretic Model For Unity", institution = "MIT Laboratory for Computer Science", number = "MIT/LCS/TM-400", pages = "64", month = jun, year = "1989", keywords = "randomized algorithms, automata, parallel program design", abstract = "UNITY - Unbounded Nondeterministic Iterative Transformations - is a computational model and a proof system to aid in the design of parallel programs developed by K. Mani Chandy and Jayadev Misra at the University of Texas. The Input/Output Automaton model is a computational model developed by Nancy Lynch and Mark Tuttle at MIT that may be used to model concurrent and distributed systems. This thesis connects these two theories. Specifically it: 1. defines UNITY Automata, a subset of I/O Automata based on the UNITY computational model, the UNITY program, 2. defines a mapping from UNITY programs to UNITY Automata, 3. adapts the UNITY proof concepts to the I/O Automaton computational model in order to obtain UNITY style proof rules for I/O Automata, 4. adapts UNITY composition operators to the I/O Automaton model and obtains composition proof rules for them, and 5. considers various examples illustrating the above work. In addition, this paper introduces an augmentation to the I/O Automaton model which facilitates reasoning about randomized algorithms, adapts UNITY concepts to it, and presents an example of a UNITY style high probability proof using such a model.", note = "Prize: \$7.00", } @Article{ReiFia93, author = "Reichwein and Fiadeiro", title = "Models for the Substitution Axiom of {UNITY} Logic", journal = "Information Processing Letters", volume = "48", year = "1993", } @Article{UdiKok93, author = "Udink and Kok", title = "Unity Properties and Sequences of States, Some Observations", journal = "Information Processing Letters", volume = "47", year = "1993", } @Article{Pachl92, author = "Pachl", title = "A Simple Proof of a Completeness Result for leads-to in the {UNITY} Logic (Corrigendum)", journal = "Information Processing Letters", volume = "44", year = "1992", } @Article{Pachl92, author = "Pachl", title = "A Simple Proof of a Completeness Result for leads-to in the {UNITY} Logic", journal = "Information Processing Letters", volume = "41", year = "1992", } @Article{GMSDAAU, author = "R. Gates and F. Manganotti and N. Sabadini and R. F. C. Walters", title = "Distributive automata and {\sc unity}", year = "1993", month = mar, note = "Submitted. Available by anonymous {\tt ftp} at {\tt ghost.sm.dsi.unimi.it} in the directory {\tt pub2/papers/sabadini} and at {\tt maths.su.oz.au} in the directory {\tt sydcat/papers/walters}", } @Book{chanmis:unity, author = "K. M. Chandy and Misra J.", title = "Parallel Program Design", publisher = "Addison-Wesley", year = "1988", } @Article{unity:001, author = "K. M. Chandy and J. Misra", title = "An Example of Stepwise Refinement of Distributed Programs: Quiescence Detection", journal = "ACM Transactions on Programming Languages and Systems", volume = "8", number = "3", pages = "326--343", month = jul, year = "1986", } @InCollection{unity:002, author = "K. M. Chandy and J. Misra", title = "Proofs of Distributed Algorithms: An Exercise", booktitle = "Developments in Concurrency and Communication", editor = "C. A. R. Hoare", chapter = "11", pages = "305--332", year = "1990", publisher = "Addison-Wesley", address = "Reading, Massachusetts", } @InProceedings{unity:003, author = "K. M. Chandy", title = "Concurrent Programming for the Masses (1984 Invited Address)", booktitle = "Proceedings of the 4th ACM Symposium on the Principles of Distributed Computing", pages = "1--12", month = aug, year = "1985", } @InCollection{unity:004, author = "K. M. Chandy", title = "Mathematics of Program Construction Applied to Analog Neural Networks", booktitle = "Proceedings of the Conference on the Mathematics of Program Construction, Groningen", editor = "J. L. A. van de Snepscheut", pages = "21--35", month = jun, year = "1989", publisher = "Springer-Verlag", address = "New York", } @InProceedings{misra-88a, author = "J. Misra", title = "A Foundation of Parallel Programming", booktitle = "Proceedings of the International Summer School on Constructive Methods in Computing Science", month = aug, year = "1988", } @InProceedings{unity:005, author = "J. Misra", title = "Specifications of concurrently accessed data", booktitle = "Mathematics of program construction", pages = "90--114", year = "1989", comment = "weitere Inferenzregeln fuer unless", } @InCollection{unity:006, author = "J. Misra", title = "Specifications of Concurrently Accessed Data", booktitle = "Proceedings of the Conference on the Mathematics of Program Construction, Groningen", editor = "J. L. A. van de Snepscheut", pages = "91--114", month = jun, year = "1989", publisher = "Springer-Verlag", address = "New York", } @InCollection{unity:007, author = "J. Misra", title = "A Simple Proof of a Simple Consensus Algorithm", booktitle = "Beauty is Our Business", chapter = "35", pages = "312--318", year = "1990", publisher = "Springer-Verlag", address = "New York", source = "hcc book", } @InProceedings{unity:08, author = "J. R. Rao", title = "Reasoning about Probabilistic Algorithms", booktitle = "Proceedings of the Ninth Annual ACM Symposium on the Principles of Distributed Computing", year = "1990", organization = ACM, } @Article{unity:009, author = "M. G. Staskauskas", title = "The Formal Specification and Design of a Distributed Electronic Funds Transfer System", journal = IEEETC, volume = "37", number = "12", pages = "1515--1528", month = dec, year = "1988", } @Article{unity:010, author = "E. Knapp", title = "An Exercise in the Formal Derivation of Parallel Programs: Maximum Flows in Graphs", journal = "ACM Transactions on Programming Languages and Systems", volume = "12", number = "2", pages = "203--223", month = apr, year = "1990", comment = "Gute knappe Einfuehrung in UNITY; Argumentation ueber weakest precondition", } @TechReport{unity:011, author = "E. Knapp", title = "Derivation of Parallel Programs: Two Examples", institution = "UT", month = oct, year = "1988", number = "TR-90-33", } @TechReport{unity:012, author = "E. Knapp", title = "A Comparison of {\em led-from} and {\em leads-to}", institution = "UT", month = oct, year = "1988", number = "TR-88-35", } @Article{unity:013, author = "E. Knapp", title = "A Predicate Transformer for Progress", journal = ipl, volume = "33", pages = "323--330", year = "1989", } @InProceedings{unity:014, author = "C. S. Jutla and E. Knapp and J. R. Rao", title = "A Predicate Transformer Approach to Semantics of Parallel Programs", booktitle = "8th Annual PODC", pages = "249--263", year = "1989", } @InProceedings{unity:015, author = "R. Gerth and A. Pnueli", title = "{Rooting {\sf UNITY}}", booktitle = "Proceedings Fifth International Workshop on Software Specification and Design", month = may, year = "1989", address = "Pittsburgh, Penn.", } %Other work includes: @TechReport{unity:016, author = "Beverly Sanders", title = "Eliminating the Substitution Axiom from {UNITY} Logic", institution = "ETH Z{\"{}u}rich, Departement Informatik", number = "128", month = may, year = "1990", } @Article{unity:017, author = "D. M. Goldschlag", title = "Mechanically verifying concurrent programs with the Boyer-Moore prover", journal = "IEEE Transaction on Software Engineering", volume = "16", number = "9", pages = "1005--1023", month = sep, year = "1990", } @MastersThesis{unity:018, author = "A. Mester", title = "entwurf verteilter Programme mit {UNITY}", school = "Universit{\"a}t Dortmund, Fachbereich Informatik", month = jan, year = "1991", } @TechReport{unity:019, author = "S. D. Swierstra P. J. A. Lentfert and A. H. Uittenbogaard", title = "Distributed Incremental Maximum Finding in Hierarchicaly Divided Graphs", institution = "Utrecht University", month = sep, year = "1990", number = "RUU-CS-90-30", } @InProceedings{unity:020, author = "A. K. Singh", title = "Program Refinement in Fair Transition Systems", booktitle = "Conference on Parallel Architectures and Languages Europe", month = jun, year = "1991", } @InProceedings{unity:021, author = "A. K. Singh", title = "Parallel Programming: Achieving Portability Through Abstraction", booktitle = "11th International Conference on Distributed Computing Systems", month = may, year = "1991", } @Article{unity:022, author = "A. K. Singh", title = "Specification of Concurrent Objects Using Auxiliary Variables", journal = "Science of Computer Programming", year = "1991", note = "to appear", } @Article{unity:023, author = "A. K. Singh and R. Overbeek", title = "Derivation of Efficient Parallel Programs: An Example From Genetic Sequence Analysis", journal = "International Journal of Parallel Programming", volume = "18", number = "6", pages = "447--484", month = dec, year = "1989", } %Here are three which have been built on a Unity-like foundation. @Article{unity:024, author = "G. C. Roman and H. C. Cunningham", title = "Mixed Programming Metaphors in a Shared Dataspace Model of Concurrency", journal = "IEEE Transactions on Software Engineering", volume = "16", number = "12", pages = "1361--1373", month = dec, year = "1990", } @Article{unity:025, author = "H. C. Cunningham and G.-C. Roman", title = "A {UNITY}-style Programming Logic for Shared Dataspace Programs", journal = "IEEE Transactions on Parallel and Distributed Systems", volume = "1", number = "3", pages = "365--376", month = jul, year = "1990", } @InProceedings{unity:026, author = "G. C. Roman and H. C. Cunningham", title = "The Synchronic Group: {A} Concurrent Programming Concept and Its Proof Logic", booktitle = "Proceedings of the 10th International Conference on Distributed Computing Systems", publisher = IEEE, month = may, year = "1990", }