Guarded commands, nondeterminacy and formal derivation of programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Guarded commands, nondeterminacy and formal derivation of programs

Full text

Pdf (481 KB)

Source

Communications of the ACM archive
Volume 18 , Issue 8 (August 1975) table of contents

Pages: 453 - 457

Year of Publication: 1975

ISSN:0001-0782

Author

Edsger W. Dijkstra

Burroughs Corp., Nuenen, The Netherlands

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 48, Downloads (12 Months): 387, Citation Count: 220

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/360933.360975 What is a DOI?

ABSTRACT

So-called “guarded commands” are introduced as a building block for alternative and repetitive constructs that allow nondeterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily uniquely determined by the initial state. For the formal derivation of programs expressed in terms of these constructs, a calculus will be be shown.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
	2	Peter Naur , J. W. Backus , F. L. Bauer , J. Green , C. Katz , J. McCarthy , A. J. Perlis , H. Rutishauser , K. Samelson , B. Vauquois , J. H. Wegstein , A. van Wijngaarden , M. Woodger, Report on the algorithmic language ALGOL 60, Communications of the ACM, v.3 n.5, p.299-314, May 1960 [doi>10.1145/367236.367262]

CITED BY 220

	Felix C. Gärtner, Fundamentals of fault-tolerant distributed computing in asynchronous environments, ACM Computing Surveys (CSUR), v.31 n.1, p.1-26, March 1999
	Michael A. Arbib , Ernest G. Manes, The Pattern-of-Calls Expansion Is the Canonical Fixpoint for Recursive Definitions, Journal of the ACM (JACM), v.29 n.2, p.577-602, April 1982
	William E. McUmber , Betty H. C. Cheng, A general framework for formalizing UML with formal languages, Proceedings of the 23rd International Conference on Software Engineering, p.433-442, May 12-19, 2001, Toronto, Ontario, Canada
	P. M. Lenders , H. Schröder , P. Strazdins, Microprogramming instruction systolic arrays, ACM SIGMICRO Newsletter, v.20 n.3, p.56-69, Sep. 1989
	Yutaka Ishikawa , Hideyuki Tokuda, Object-oriented real-time language design: constructs for timing constraints, ACM SIGPLAN Notices, v.25 n.10, p.289-298, Oct. 1990
	Barry W. Boehm, Software engineering-as it is, Proceedings of the 4th international conference on Software engineering, p.11-21, September 17-19, 1979, Munich, Germany
	R. A. Mueller, Formalization and automated synthesis of microprograms, ACM SIGMICRO Newsletter, v.11 n.3-4, p.45-53, Dec. 1980
	Andrew D. Bailey, Jr. , James H. Gerlach , R. Preston McAfee , Andrew B. Whinston, An OIS model for internal accounting control evaluation, ACM Transactions on Information Systems (TOIS), v.1 n.1, p.25-44, Jan. 1983
	C. A. R. Hoare, Assertions: A Personal Perspective, IEEE Annals of the History of Computing, v.25 n.2, p.14-25, April 2003
	Henri E. Bal , Raoul Bhoedjang , Rutger Hofman , Ceriel Jacobs , Koen Langendoen , Tim Rühl , M. Frans Kaashoek, Performance evaluation of the Orca shared-object system, ACM Transactions on Computer Systems (TOCS), v.16 n.1, p.1-40, Feb. 1998
	J. Lebensold , T. Radhakrishnan , W. M. Jaworski, A modelling tool for office information systems, ACM SIGOA Newsletter, v.3 n.1-2, p.141-152, June 21-23, 1982
	G. N. Buckley , Abraham Silberschatz, An Effective Implementation for the Generalized Input-Output Construct of CSP, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.223-235, April 1983
	Douglas T. Ross, Origins of the APT language for automatically programmed tools, ACM SIGPLAN Notices, v.13 n.8, p.61-99, August 1978
	Michael Benedikt , Timothy Griffin , Leonid Libkin, Verifiable properties of database transactions, Proceedings of the fifteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.117-127, June 04-06, 1996, Montreal, Quebec, Canada
	P. K. Chrysanthis , D. Stemple , K. Ramamritham, A logically distributed approach for structuring office systems, ACM SIGOIS Bulletin, v.11 n.2-3, p.11-20, Apr. 1990
	Donald I. Good , Richard M. Cohen , James Keeton-Williams, Principles of proving concurrent programs in Gypsy, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.42-52, January 29-31, 1979, San Antonio, Texas
	J. A. Barnden, Nonsequentiality and Concrete Activity Phases in Discrete-Event Simulation Languages, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.3, p.293-317, July 1981
	Gregory R. Andrews , Fred B. Schneider, Concepts and Notations for Concurrent Programming, ACM Computing Surveys (CSUR), v.15 n.1, p.3-43, March 1983
	Kuo-chung Tai, Fault-tolerant string processing by pattern mapping, Proceedings of the 1977 annual conference, p.336-342, January 1977
	Gregory R. Andrews, Synchronizing Resources, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.405-430, Oct. 1981
	Nissim Francez , Dexter Kozen, Generalized fair termination, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.46-53, January 15-18, 1984, Salt Lake City, Utah, United States
	Michael J. O'Donnell, A critique of the foundations of Hoare style programming logics, Communications of the ACM, v.25 n.12, p.927-935, Dec 1982
	Toby Bloom, Evaluating synchronization mechanisms, Proceedings of the seventh ACM symposium on Operating systems principles, p.24-32, December 10-12, 1979, Pacific Grove, California, United States
	Martin Rem, Associons: A Program Notation with Tuples Instead of Variables, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.3, p.251-262, July 1981
	P. Y T Hsu , E. S. Davidson, Highly concurrent scalar processing, ACM SIGARCH Computer Architecture News, v.14 n.2, p.386-395, June 1986
	J. Zwiers , W. Roever, Predicates are predicate transformers: a unified compositional theory for concurrency, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.265-279, June 1989, Edmonton, Alberta, Canada
	Max Muhlhauser, Using distributed simulation for distributed application development, Proceedings of the 21st annual symposium on Simulation, p.189-206, January 1988, Tampa, Florida, United States
	Xuedong Luo, A practical sieve algorithm finding prime numbers, Communications of the ACM, v.32 n.3, p.344-346, March 1989
	Martin Rem, The Closure Statement: A Programming Language Construct Allowing Ultraconcurrent Execution, Journal of the ACM (JACM), v.28 n.2, p.393-410, April 1981
	Edsger W. Dijkstra , Leslie Lamport , A. J. Martin , C. S. Scholten , E. F. M. Steffens, On-the-fly garbage collection: an exercise in cooperation, Communications of the ACM, v.21 n.11, p.966-975, Nov. 1978
	Per Brinch Hansen, Distributed processes: a concurrent programming concept, Communications of the ACM, v.21 n.11, p.934-941, Nov. 1978
	Shang-Cheng Chyou, Structure charts and program correctness proofs, Proceedings of the 7th international conference on Software engineering, p.486-498, March 26-29, 1984, Orlando, Florida, United States
	Naoyuki Tamura, Knowledge-based optimization in Prolog compiler, Proceedings of 1986 ACM Fall joint computer conference, p.237-240, November 1986, Dallas, Texas, United States
	R. K. Gupta , C. N. Coelho, Jr. , G. De Micheli, Synthesis and simulation of digital systems containing interacting hardware and software components, Proceedings of the 29th ACM/IEEE conference on Design automation, p.225-230, June 08-12, 1992, Anaheim, California, United States
	David Gries , Jayadev Misra, A linear sieve algorithm for finding prime numbers, Communications of the ACM, v.21 n.12, p.999-1003, Dec. 1978
	Jarallah AlGhamdi , Joseph Urban, Comparing and assessing programming languages: basis for a qualitative methodology, Proceedings of the 1993 ACM/SIGAPP symposium on Applied computing: states of the art and practice, p.222-229, February 14-16, 1993, Indianapolis, Indiana, United States
	Timothy Griffin , Richard Hull, A framework for implementing hypothetical queries, ACM SIGMOD Record, v.26 n.2, p.231-242, June 1997
	R. L. Page , M. G. Conant , D. H. Grit, If-then-else as a concurrency inhibitor in eager beaver evaluation of recursive programs, Proceedings of the 1981 conference on Functional programming languages and computer architecture, p.179-186, October 18-22, 1981, Portsmouth, New Hampshire, United States
	V. R. Pratt, A practical decision method for propositional dynamic logic (Preliminary Report), Proceedings of the tenth annual ACM symposium on Theory of computing, p.326-337, May 01-03, 1978, San Diego, California, United States
	Michał Walicki , Sigurd Meldal, Algebraic approaches to nondeterminism—an overview, ACM Computing Surveys (CSUR), v.29 n.1, p.30-81, March 1997
	I. S. Chung , W. K. Lee , G. S. Yoon , Y. R. Kwon, Program slicing based on specification, Proceedings of the 2001 ACM symposium on Applied computing, p.605-609, March 2001, Las Vegas, Nevada, United States
	David Harel , Vaughan R. Pratt, Nondeterminism in logics of programs, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.203-213, January 23-25, 1978, Tucson, Arizona
	Bard Bloom , Allan Cheng , Ashvin Dsouza, Using a Protean Language to Enhance Expressiveness in Specification, IEEE Transactions on Software Engineering, v.23 n.4, p.224-234, April 1997
	Barton P. Miller , Jong-Deok Choi, A mechanism for efficient debugging of parallel programs, ACM SIGPLAN Notices, v.24 n.1, p.141-150, Jan. 1989
	Rajesh K. Gupta , Claudionor Nunes Coelho, Jr. , Giovanni De Micheli, Synthesis and simulation of digital systems containing interacting hardware and software components, Readings in hardware/software co-design, Kluwer Academic Publishers, Norwell, MA, 2001
	Verlynda Dobbs, A comparison of concurrent languages: a class project, ACM SIGCSE Bulletin, v.19 n.1, p.62-66, Feb. 1987
	I. Greif , A. Meyer, Specifying programming language semantics: a tutorial and critique of a paper by Hoare and Lauer, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.180-189, January 29-31, 1979, San Antonio, Texas
	Roberto Giacobazzi , Isabella Mastroeni, A characterization of symmetric semantics by domain complementation, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.115-126, September 20-23, 2000, Montreal, Quebec, Canada
	J. R. Jefferson Wadkins, Rigorous proofs of program correctness without formal logic, ACM SIGCSE Bulletin, v.27 n.1, p.307-311, March 1995
	Michael S. Miller , Howard Cunningham , Chan Lee , Steven R. Vegdahl, The application accelerator illustration system, ACM SIGPLAN Notices, v.21 n.11, p.294-302, Nov. 1986
	Van King Tan , Eugeniusz Eberbach, A CSA-based robot plan generator, Proceedings of the 1993 ACM conference on Computer science, p.115-123, February 16-18, 1993, Indianapolis, Indiana, United States
	R. L. Earle , R. B. Kieburtz , A. Silberschatz, Technical Correspondence, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.533-536, Oct. 1981
	Ehud Shapiro, The family of concurrent logic programming languages, ACM Computing Surveys (CSUR), v.21 n.3, p.413-510, Sep. 1989
	Henri E. Bal , Jennifer G. Steiner , Andrew S. Tanenbaum, Programming languages for distributed computing systems, ACM Computing Surveys (CSUR), v.21 n.3, p.261-322, Sep. 1989
	Albert R. Meyer , Joseph Y. Halpern, Axiomatic Definitions of Programming Languages: A Theoretical Assessment, Journal of the ACM (JACM), v.29 n.2, p.555-576, April 1982
	Thanasis Mitsolides , Malcolm Harrison, Generators and the replicator control structure in the parallel environment of ALLOY, ACM SIGPLAN Notices, v.25 n.6, p.189-196, Jun. 1990
	C.-D. Jung , E. Siberrt, Polling in concurrent programming, Proceedings of the 17th conference on ACM Annual Computer Science Conference, p.204-209, February 21-23, 1989, Louisville, Kentucky
	Fuyau Lin, A formalism for specifying communicating processes, Proceedings of the 1993 ACM conference on Computer science, p.123-130, February 16-18, 1993, Indianapolis, Indiana, United States
	Rajive Bagrodia, Synchronization of asynchronous processes in CSP, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.4, p.585-597, Oct. 1989
	ACM Forum: letters, Communications of the ACM, v.19 n.2, p.105-108, Feb. 1976
	Roberto Giacobazzi , Isabella Mastroeni, Compositionality in the puzzle of semantics, ACM SIGPLAN Notices, v.37 n.3, p.87-97, March 2002
	C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.26 n.1, p.100-106, Jan. 1983
	Michael J. Fischer , Richard E. Ladner, Propositional modal logic of programs, Proceedings of the ninth annual ACM symposium on Theory of computing, p.286-294, May 04-04, 1977, Boulder, Colorado, United States
	G. Castelli , F. De Cindio , G. De Michelis , C. Simone, An overview of the GCP programming language, Proceedings of the 1985 ACM SIGSMALL symposium on Small systems, p.245-253, May 1985, Danvers, Massachusetts, United States
	Isabel Gouveia Lima , Richard Hopkins , Lindsay Marshall , David Mundy , Philip Treleaven, Decentralised control flow - based on UNIX, Proceedings of the 1983 ACM SIGPLAN symposium on Programming language issues in software systems, p.192-201, June 27-29, 1983, San Francisco, California, United States
	Irene Greif , Albert R. Meyer, Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.484-507, Oct. 1981
	Miguel García Hoffmann, Hardware implementation of communication protocols: A formal approach, Proceedings of the 7th annual symposium on Computer Architecture, p.253-263, May 06-08, 1980, La Baule, United States
	Andrew D. Bailey, Jr. , James Gerlach , R. Preston McAfee , Andrew B. Whinston, An OIS model for internal control evaluation, ACM SIGOA Newsletter, v.3 n.1-2, p.27-28, June 21-23, 1982
	K. M. Mossaad , C. L. Wu, Parallel resource allocation algorithms on macro-pipelined architectures, Proceedings of the 19th annual conference on Computer Science, p.299-310, April 1991, San Antonio, Texas, United States
	Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000
	David S. Keyes , Laura K. Dillon , Moon Jung Chung, Analysis of a scheduler for a CAD framework, Proceedings of the 21st international conference on Software engineering, p.152-161, May 16-22, 1999, Los Angeles, California, United States
	Axel van Lamsweerde, Formal specification: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.147-159, June 04-11, 2000, Limerick, Ireland
	Toshimi Minoura , Shirish S. Pargaonkar , Kurt Rehfuss, Structural active object systems for simulation, ACM SIGPLAN Notices, v.28 n.10, p.338-355, Oct. 1, 1993
	M. Dr. Muhlhäuser, Software engineering for distributed applications: the design project, Proceedings of the 10th international conference on Software engineering, p.93-101, April 11-15, 1988, Singapore
	Arthur Bernstein, Output Guards and Nondeterminism in “Communicating Sequential Processes”, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.2, p.234-238, April 1980
	Robert A. Mueller , Gearold R. Johnson, Contrasting translation, verification and synthesis in software and firmware engineering, ACM SIGMICRO Newsletter, v.12 n.4, p.17-22, Dec. 1981
	Patrick Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, v.277 n.1-2, p.47-103, April 28, 2002
	Joost Engelfriet , Erik Meineche Schmidt , Jan van Leeuwen, Stack Machines and Classes of Nonnested Macro Languages, Journal of the ACM (JACM), v.27 n.1, p.96-117, Jan. 1980
	Ehud Gudes , Aharon Tubman, AutoWF: a secure web workflow system using autonomous objects, Data & Knowledge Engineering, v.43 n.1, p.1-27, October 2002
	Eduardo Casais, An object oriented system implementing KNOs, ACM SIGOIS Bulletin, v.9 n.2-3, p.284-290, April & July 1988
	María Consuelo Franky, JOYCE+: model and language for multi-site distributed systems, Proceedings of the second international symposium on Databases in parallel and distributed systems, p.160-170, July 02-04, 1990, Dublin, Ireland
	David Harel, Recursion in logics of programs, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.81-92, January 29-31, 1979, San Antonio, Texas
	D. E. Cooke, Towards a Formalism to Produce a Programmer Assistant CASE Tool, IEEE Transactions on Knowledge and Data Engineering, v.2 n.3, p.320-326, September 1990
	Ali Mili , Jules Desharnais , Jean Raynomd Gagné, Formal models of stepwise refinements of programs, ACM Computing Surveys (CSUR), v.18 n.3, p.231-276, Sept. 1986
	K. M. Chandy , J. Misra, The drinking philosophers problem, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.4, p.632-646, Oct. 1984
	James Donahue , Alan Demers, Data types are values, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.426-445, July 1985
	Robert A. Mueller , Joseph Varghese, Retargetable microcode synthesis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.2, p.257-276, April 1987
	Dieter Fensel , Enrico Motta , Frank van Harmelen , V. Richard Benjamins , Monica Crubezy , Stefan Decker , Mauro Gaspari , Rix Groenboom , William Grosso , Mark Musen , Enric Plaza , Guus Schreiber , Rudi Studer , Bob Wielinga, The unified problem-solving method development language UPML, Knowledge and Information Systems, v.5 n.1, p.83-131, March 2003
	Mitchell Wand, A new incompleteness result for Hoare's system, Proceedings of the eighth annual ACM symposium on Theory of computing, p.87-91, May 03-05, 1976, Hershey, Pennsylvania, United States
	Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia
	Jacques Chassin de Kergommeaux , Philippe Codognet, Parallel logic programming systems, ACM Computing Surveys (CSUR), v.26 n.3, p.295-336, Sept. 1994
	Jan van den Bos , R. Plasmeijer , Jan W. M. Stroet, Process Communication Based on Input Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.3, p.224-250, July 1981
	Frank D. Anger, On Lamport's interprocessor communication model, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.3, p.404-417, July 1989
	Zohar Manna , Richard Waldinger, The synthesis of structure-changing programs, Proceedings of the 3rd international conference on Software engineering, p.175-187, May 10-12, 1978, Atlanta, Georgia, United States
	Albert R. Meyer , Joseph Y. Halpern, Axiomatic definitions of programming languages: a theoretical assessment (preliminary report), Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.203-212, January 28-30, 1980, Las Vegas, Nevada
	Eric C. R. Hehner, Predicative programming Part I, Communications of the ACM, v.27 n.2, p.134-143, Feb. 1984
	Ian Foster , Stephen Taylor, A compiler approach to scalable concurrent-program design, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.577-604, May 1994
	G. A. Ringwood, Parlog86 and the dining logicians, Communications of the ACM, v.31 n.1, p.10-25, Jan. 1988
	Robert A. Mueller , Joseph Varghese, Formal semantics for the automated derivation of micro-code, Proceedings of the 19th conference on Design automation, p.815-824, January 1982
	H. G. Mendelbaum , D. Finkelman, Systems Design: CASDA: Synthesized Graphic Design of Real-Time Systems, IEEE Computer Graphics and Applications, v.9 n.1, p.40-46, January 1989
	V. R. Pratt, On the composition of processes, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-223, January 25-27, 1982, Albuquerque, Mexico
	Yifeng Chen, A fixpoint theory for non-monotonic parallelism, Theoretical Computer Science, v.308 n.1-3, p.367-392, 3 November 2003
	C. A. R. Hoare, Communicating sequential processes, The origin of concurrent programming: from semaphores to remote procedure calls, Springer-Verlag New York, Inc., New York, NY, 2002
	Per Brinch Hansen, The invention of concurrent programming, The origin of concurrent programming: from semaphores to remote procedure calls, Springer-Verlag New York, Inc., New York, NY, 2002
	C. Rolland , C. Richard, Transactions modeling, Proceedings of the 1982 ACM SIGMOD international conference on Management of data, June 02-04, 1982, Orlando, Florida
	D. Comte , G. Durrieu , O. Gelly , A. Plas , J. C. Syre, Parallelism, control and synchronization expression in a single assignment language, ACM SIGPLAN Notices, v.13 n.1, p.25-33, January 1978
	Per Brinch Hansen, Distributed processes: a concurrent programming concept, The origin of concurrent programming: from semaphores to remote procedure calls, Springer-Verlag New York, Inc., New York, NY, 2002
	Abraham Silberschatz, A note on the distributed program component cell, ACM SIGPLAN Notices, v.16 n.7, p.89-96, July 1981
	R. A. Nelson, XL: a language structure, ACM SIGPLAN Notices, v.13 n.12, p.73-87, December 1978
	Reza Ziaei , Gul Agha, SynchNet: a Petri net based coordination language for distributed objects, Proceedings of the second international conference on Generative programming and component engineering, p.324-343, September 22-25, 2003, Erfurt, Germany
	F. L. Bauer , M. Broy , R. Gnatz , W. Hesse , B. Krieg-Brückner , H. Partsch , P. Pepper , H. Wössner, Towards a wide spectrum language to support program specification and program development, ACM SIGPLAN Notices, v.13 n.12, p.15-24, December 1978
	R. Kurki-Suonio, Action systems in incremental and aspect-oriented modeling, Distributed Computing, v.16 n.2-3, p.201-217, September 2003
	Zhen-Hua Duan , Maciej Koutny, A framed temporal logic programming language, Journal of Computer Science and Technology, v.19 n.3, p.341-351, May 2004
	Yingzhou Zhang , Baowen Xu, A survey of semantic description frameworks for programming languages, ACM SIGPLAN Notices, v.39 n.3, March 2004
	Josyula R. Rao, Reasoning about probabilistic parallel programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.798-842, May 1994
	C. A. R. Hoare, Some Properties of Predicate Transformers, Journal of the ACM (JACM), v.25 n.3, p.461-480, July 1978
	F. L. Bauer, Programming as an evolutionary process, Proceedings of the 2nd international conference on Software engineering, p.223-234, October 13-15, 1976, San Francisco, California, United States
	S.-Y. Tan , S. B. Furber , W.-F. Yen, The design of an asynchronous VHDL synthesizer, Proceedings of the conference on Design, automation and test in Europe, p.44-51, February 23-26, 1998, Le Palais des Congrés de Paris, France
	Richard E. Nance , C. Michael Overstreet , Ernest H. Page, Redundancy in model specifications for discrete event simulation, ACM Transactions on Modeling and Computer Simulation (TOMACS), v.9 n.3, p.254-281, July 1999
	Raymond T. Yeh, An approach to program verification, Proceedings of the 13th conference on Design automation, p.295-300, June 28-30, 1976, San Francisco, California, United States
	Paul Pritchard, A sublinear additive sieve for finding prime number, Communications of the ACM, v.24 n.1, p.18-23, Jan. 1981
	B. P. Miller , Jong-Deok Choi, A mechanism for efficient debugging of parallel programs, ACM SIGPLAN Notices, v.23 n.7, p.135-144, July 1988
	Ian Foster, Compositional parallel programming languages, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.4, p.454-476, July 1996
	L. Chiu , M. T. Liu, High level specification of concurrency control in distributed database systems, Proceedings of the 10th international conference on Software engineering, p.309-317, April 11-15, 1988, Singapore
	Edward E. Balkovich , Colin Whitby-Strevens, On the performance of decentralized software, ACM SIGMETRICS Performance Evaluation Review, v.9 n.2, p.173-180, Summer 1980
	Lawrence Robinson , Karl N. Levitt, Proof techniques for hierarchically structured programs, Communications of the ACM, v.20 n.4, p.271-283, April 1977
	C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978
	M. B. Wells , B. L. Kurtz, Teaching multiple programming paradigms: a proposal for a paradigm general pseudocode, ACM SIGCSE Bulletin, v.21 n.1, p.246-251, Feb. 1989
	Mehmet Hakan Karaata, Self-Stabilizing Strong Fairness under Weak Fairness, IEEE Transactions on Parallel and Distributed Systems, v.12 n.4, p.337-345, April 2001
	Bent Bruun Kristensen , Ole Lehrmann Madsen , Birger Møller-Pedersen , Kristen Nygaard, Abstraction mechanisms in the BETA programming language, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.285-298, January 24-26, 1983, Austin, Texas
	David Gries, An exercise in proving parallel programs correct, Communications of the ACM, v.20 n.12, p.921-930, Dec. 1977
	O. M. Nierstrasz, Active objects in hybrid, ACM SIGPLAN Notices, v.22 n.12, p.243-253, Dec. 1987
	Eugeniusz Eberbach, CSA: two paradigms of the language for adaptive expert systems, Proceedings of the 19th annual conference on Computer Science, p.570-581, April 1991, San Antonio, Texas, United States
	E. M. J. C. Van Oost, DUIF: a data-driented flowchart environment, ACM SIGPLAN Notices, v.18 n.2, p.69-75, February 1983
	Roberto Giacobazzi , Isabella Mastroeni, Non-Standard Semantics for Program Slicing, Higher-Order and Symbolic Computation, v.16 n.4, p.297-339, December 2003
	Gregor Bochmann, Delay-Independent Design for Distributed Systems, IEEE Transactions on Software Engineering, v.14 n.8, p.1229-1237, August 1988
	Anne Dinning, A Survey of Synchronization Methods for Parallel Computers, Computer, v.22 n.7, p.66-77, July 1989
	Patrick M. Lenders, A Generalized Message-Passing Mechanism for Communicating Sequential Processes, IEEE Transactions on Computers, v.37 n.6, p.646-651, June 1988
	Mohsen AlSharif , Walter P. Bond , Turky Al-Otaiby, Assessing the complexity of software architecture, Proceedings of the 42nd annual Southeast regional conference, April 02-03, 2004, Huntsville, Alabama
	C. Roland , C. Richard , S. Leifert, A proposal for information systems design and management, ACM SIGDA Newsletter, v.10 n.2, p.83-109, Aut. 1980
	Shinichi Honiden , Kazuhiko Nishimura , Naoshi Uchihira , Kiyoshi Itoh, An Application of Artificial Intelligence to Object-Oriented Performance Design for Real-Time Systems, IEEE Transactions on Software Engineering, v.20 n.11, p.849-867, November 1994
	Lloyd Allison, On nondeterministic control structures, ACM SIGPLAN Notices, v.13 n.7, p.18-20, July 1978
	Ralph-Johan Back , Viorel Preoteasa, Reasoning about recursive procedures with parameters, Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.1-7, August 26, 2003, Uppsala, Sweden
	John K. Dixon , John McLean , David L. Parnas, Rapid prototyping by means of abstract module specifications written as trace axioms, ACM SIGSOFT Software Engineering Notes, v.7 n.5, p.45-49, December 1982
	Emin Gün Sirer , Ke Wang, An access control language for web services, Proceedings of the seventh ACM symposium on Access control models and technologies, June 03-04, 2002, Monterey, California, USA
	Saddek Bensalem , Yassine Lakhnech, Automatic Generation of Invariants, Formal Methods in System Design, v.15 n.1, p.75-92, July 1999
	Colette Rolland, Database dynamics, ACM SIGMIS Database, v.14 n.3, p.32-43, Spring 1983
	Daniel Powell, Automatic derivation of loop termination conditions to support verification, Proceedings of the 27th Australasian conference on Computer science, p.89-97, January 01, 2004, Dunedin, New Zealand
	Norihisa Suzuki , Kiyoshi Ishihata, Implementation of an array bound checker, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.132-143, January 17-19, 1977, Los Angeles, California
	Patrick Causot , Radhia Cousot, Static determination of dynamic properties of generalized type unions, ACM SIGPLAN Notices, v.12 n.3, p.77-94, March 1977
	Amiram Yehudai, Automatic indention versus program formatting, ACM SIGPLAN Notices, v.15 n.10, p.85-87, October 1980
	Daniel Le Métayer , Valérie-Anne Nicolas , Olivier Ridoux, Exploring the Software Development Trilogy, IEEE Software, v.15 n.6, p.75-81, November 1998
	Nicklaus Wirth, Hardware architectures for programming languages and programming languages for hardware architectures, ACM SIGARCH Computer Architecture News, v.15 n.5, p.2-8, Oct. 1987
	Robert M. Balzer , Neil M. Goldman , David S. Wile, Operational specification as the basis for rapid prototyping, ACM SIGSOFT Software Engineering Notes, v.7 n.5, p.3-16, December 1982
	Cliff B. Jones, The Early Search for Tractable Ways of Reasoning about Programs, IEEE Annals of the History of Computing, v.25 n.2, p.26-49, April 2003
	Shmuel Katz , Doron Peled, Verification of distributed programs using representative interleaving sequences, Distributed Computing, v.6 n.2, p.107-120, September 1992
	Christel Baier , Frank Ciesinski , Marcus Groesser, Quantitative analysis of distributed randomized protocols, Proceedings of the 10th international workshop on Formal methods for industrial critical systems, p.2-7, September 05-06, 2005, Lisbon, Portugal
	J. C. M. Baeten, A brief history of process algebra, Theoretical Computer Science, v.335 n.2-3, p.131-146, 23 May 2005
	Abraham Silberschatz, On the synchronization mechanism of the ADA language, ACM SIGPLAN Notices, v.16 n.2, p.96-103, February 1981
	Cormac Flanagan , Stephen N. Freund , Shaz Qadeer , Sanjit A. Seshia, Modular verification of multithreaded programs, Theoretical Computer Science, v.338 n.1-3, p.153-183, 10 June 2005
	Roberto Giacobazzi , Isabella Mastroeni, Transforming semantics by abstract interpretation, Theoretical Computer Science, v.337 n.1-3, p.1-50, 9 June 2005
	Robert A. Mueller , Joseph Varghese, Flow graph machine models in microcode synthesis, ACM SIGMICRO Newsletter, v.14 n.4, December 1983
	Mary Croarken , Nathan Ensmenger, Events & sightings, IEEE Annals of the History of Computing, v.25 n.1, p.65-69, January 2003
	Prasad Naldurg , Roy H. Campbell, Dynamic access control: preserving safety and trust for network defense operations, Proceedings of the eighth ACM symposium on Access control models and technologies, June 02-03, 2003, Como, Italy
	Tullio Vardanega , Juan Zamorano , Juan Antonio De La Puente, On the dynamic semantics and the timing behavior of Ravenscar kernels, Real-Time Systems, v.29 n.1, p.59-89, January 2005
	Pradeep Jain , Simon S. Lam, Specification of Real-Time Broadcast Networks, IEEE Transactions on Computers, v.40 n.4, p.404-422, April 1991
	V. C. Barbosa, Strategies for the Prevention of Communication Deadlocks in Distributed Parallel Programs, IEEE Transactions on Software Engineering, v.16 n.11, p.1311-1316, November 1990
	Fuyau Lin, Design and validation of a message-passing system, Proceedings of the 7th international workshop on Software specification and design, December 06-07, 1993, Redondo Beach, California
	J. J. P. Tsai , K.-Y. Fang , H.-Y. Chen , Y.-D. Bi, A Noninterference Monitoring and Replay Mechanism for Real-Time Software Testing and Debugging, IEEE Transactions on Software Engineering, v.16 n.8, p.897-916, August 1990
	Mehmet Hakan Karaata, An optimal self-stabilizing strarvation-free alternator, Journal of Computer and System Sciences, v.71 n.4, p.480-494, November 2005
	Hai Zhou, Deriving a new efficient algorithm for min-period retiming, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
	Lori A. Clarke , David S. Rosenblum, A historical perspective on runtime assertion checking in software development, ACM SIGSOFT Software Engineering Notes, v.31 n.3, May 2006
	Patrick M. Lenders, Distributed Computing with Single Read-Single Write Variables, IEEE Transactions on Software Engineering, v.15 n.5, p.569-574, May 1989
	Allen L. Ambler , Donald I. Good , James C. Browne , Wilhelm F. Burger , Richard M. Cohen , Charles G. Hoch , Robert E. Wells, Gypsy: A language for specification and implementation of verifiable programs, ACM SIGPLAN Notices, v.12 n.3, p.1-10, March 1977
	Robert B. Terwilliger, Toward tools to support the Gries/Dijkstra design process, ACM SIGSOFT Software Engineering Notes, v.18 n.2, p.50-59, April 1993
	Hidetaka Kondoh , Kokichi Futatsugi, To use or not to use the goto statement: programming styles viewed from Hoare logic, Science of Computer Programming, v.60 n.1, p.82-116, March 2006
	Deborah G. Johnson , Keith W. Miller, A dialogue on responsibility, moral agency, and IT systems, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
	Einar Broch Johnsen , Olaf Owe , Ingrid Chieh Yu, Creol: a type-safe object-oriented model for distributed concurrent systems, Theoretical Computer Science, v.365 n.1, p.23-66, 10 November 2006
	Douglas T. Ross, Origins of the APT language for automatically programmed tools, History of programming languages I, ACM Press, New York, NY, 1978
	Paolo Zuliani, Quantum Programming With Mixed States, Electronic Notes in Theoretical Computer Science (ENTCS), 170, p.185-199, March, 2007
	Bent Bruun Kristensen , Ole Lehrmann Madsen , Birger Møller-Pedersen, The when, why and why not of the BETA programming language, Proceedings of the third ACM SIGPLAN conference on History of programming languages, p.10-1-10-57, June 09-10, 2007, San Diego, California
	Leszek Kotulski , Lukasz Fryz , Tomasz Gorazd, On synchronization with direct delaying and resuming, Proceedings of the 25th conference on IASTED International Multi-Conference: Software Engineering, p.117-122, February 13-15, 2007, Innsbruck, Austria
	Farokh B. Bastani, Relational programs: An architecture for robust real-time safety-critical process-control systems, Annals of Software Engineering, v.7 n.1-4, p.5-24, 1999
	Dines Bjørner, Pinnacles of software engineering: 25 years of formal methods, Annals of Software Engineering, v.10 n.1-4, p.11-66, 2000
	Mansoor Ansari , Linda Ness , Marek Rusinkiewicz , Amit P. Sheth, Using Flexible Transactions to Support Multi-System Telecommunication Applications, Proceedings of the 18th International Conference on Very Large Data Bases, p.65-76, August 23-27, 1992
	Leo Geurts , Lambert Meertens, Remarks on Abstracto, ALGOL Bulletin
	M Collado , R Morales , J J Moreno, A Modula-2 implementation of CSP, ACM SIGPLAN Notices, v.22 n.6, p.25-38, June 1987
	A. Burns , G. Davies, Pascal-FC: a language for teaching concurrent programming, ACM SIGPLAN Notices, v.23 n.1, p.58-66, Jan., 1988
	J. Fullerton, An alternate design for Fortran 8X, ACM SIGPLAN Fortran Forum, v.6 n.3, p.31-40, Dec. 1987
	B. Lees, Introductory concurrent programming with Modula-2, ACM SIGCSE Bulletin, v.17 n.3, p.34-41, Sept. 1985
	Boyko B. Bantchev, Terminable statements and destructive computation, ACM SIGPLAN Notices, v.29 n.2, p.33-38, Feb. 1994
	R. A. Frost, Application programming as the construction of language interpreters, ACM SIGPLAN Notices, v.24 n.9, p.142-151, Sept. 1989
	Ward Douglas Maurer, Partially defined computer instructions and guards, Science of Computer Programming, v.72 n.3, p.220-239, August, 2008
	Manuel Costa , Miguel Castro , Lidong Zhou , Lintao Zhang , Marcus Peinado, Bouncer: securing software by blocking bad input, ACM SIGOPS Operating Systems Review, v.41 n.6, December 2007
	Aleksandar Nanevski , Paul Govereau , Greg Morrisett, Towards type-theoretic semantics for transactional concurrency, Proceedings of the 4th international workshop on Types in language design and implementation, January 24-24, 2009, Savannah, GA, USA
	Johan Dovland , Einar Broch Johnsen , Olaf Owe, Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects, Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.3, p.19-34, May, 2008
	Ilie Şavga , Michael Rudolf, Refactoring-based support for binary compatibility in evolving frameworks, Proceedings of the 6th international conference on Generative programming and component engineering, October 01-03, 2007, Salzburg, Austria
	Shuvendu K. Lahiri , Randal E. Bryant, Predicate abstraction with indexed predicates, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.4-es, December 2007
	Jonathan Edwards, No ifs, ands, or buts: uncovering the simplicity of conditionals, ACM SIGPLAN Notices, v.42 n.10, October 2007
	Hai Zhou, A new efficient retiming algorithm derived by formal manipulation, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.1, p.1-19, January 2008
	Anup Kumar Bandyopadhyay, Weakest precondition based verification tool that models spatial ordering, ACM SIGSOFT Software Engineering Notes, v.33 n.2, March 2008
	Arshad Jhumka , Felix Freiling , Christof Fetzer , Neeraj Suri, An approach to synthesise safe systems, International Journal of Security and Networks, v.1 n.1/2, p.62-74, September 2006
	Aleksandar Nanevski , Greg Morrisett , Avraham Shinnar , Paul Govereau , Lars Birkedal, Ynot: dependent types for imperative programs, ACM SIGPLAN Notices, v.43 n.9, September 2008
	Saddek Bensalem , Doron Peled , Hongyang Qu , Stavros Tripakis, Automatic generation of path conditions for concurrent timed systems, Theoretical Computer Science, v.404 n.3, p.275-292, September, 2008
	Manuel Costa , Jon Crowcroft , Miguel Castro , Antony Rowstron , Lidong Zhou , Lintao Zhang , Paul Barham, Vigilante: End-to-end containment of Internet worm epidemics, ACM Transactions on Computer Systems (TOCS), v.26 n.4, p.1-68, December 2008
	Ian J. Hayes, Towards reasoning about teleo-reactive programs for robust real-time systems, Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems, November 17-19, 2008, Newcastle upon Tyne, United Kingdom
	Aleksandar Nanevski , Greg Morrisett , Lars Birkedal, Hoare type theory, polymorphism and separation1, Journal of Functional Programming, v.18 n.5-6, p.865-911, September 2008
	Makoto Amamiya , Ryuzo Hasegawa , Osamu Nakamura , Hirohide Mikami, A list-processing-oriented data flow machine architecture, Proceedings of the June 7-10, 1982, national computer conference, June 07-10, 1982, Houston, Texas
	Jeremy Condit , Brian Hackett , Shuvendu K. Lahiri , Shaz Qadeer, Unifying type checking and property checking for low-level code, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Zhou Chaochen, Weakest environment of communicating processes, Proceedings of the June 7-10, 1982, national computer conference, June 07-10, 1982, Houston, Texas
	Jerrold L. Wagener, Guarded command, Encyclopedia of Computer Science, 4th edition, John Wiley and Sons Ltd., Chichester, 2003
	Christian Fritz , Richard Hull , Jianwen Su, Automatic construction of simple artifact-based business processes, Proceedings of the 12th International Conference on Database Theory, March 23-25, 2009, St. Petersburg, Russia
	David Lorge Parnas, Document based rational software development, Knowledge-Based Systems, v.22 n.3, p.132-141, April, 2009
	Musard Balliu , Isabella Mastroeni, A weakest precondition approach to active attacks analysis, Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, June 15-21, 2009, Dublin, Ireland
	Jussi Rintanen, Regression for Classical and Nondeterministic Planning, Proceeding of the 2008 conference on ECAI 2008: 18th European Conference on Artificial Intelligence, p.568-572, June 27, 2008
	R. M. Burstall , J. A. Goguen, Putting theories together to make specifications, Proceedings of the 5th international joint conference on Artificial intelligence, p.1045-1058, August 22-25, 1977, Cambridge, USA
	Stanley J. Rosenschein, Plan synthesis: a logical perspective, Proceedings of the 7th international joint conference on Artificial intelligence, p.331-337, August 24-28, 1981, Vancouver, BC, Canada
	D. Paul Benjamin, Learning strategies by reasoning about rules, Proceedings of the 10th international joint conference on Artificial intelligence, p.256-259, August 23-29, 1987, Milan, Italy
	Bruce W. Porter , Dennis F. Kibler, A comparison of analytic and experimental goal regression for machine learning, Proceedings of the 9th international joint conference on Artificial intelligence, p.555-559, August 18-23, 1985, Los Angeles, California
	Michal Armoni , Mordechai Ben-Ari, The concept of nondeterminism: its development and implications for teaching, ACM SIGCSE Bulletin, v.41 n.2, June 2009