Hierarchical correctness proofs for distributed algorithms

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Hierarchical correctness proofs for distributed algorithms

Full text

Pdf (1.71 MB)

Source

Annual ACM Symposium on Principles of Distributed Computing archive
Proceedings of the sixth annual ACM Symposium on Principles of distributed computing table of contents

Vancouver, British Columbia, Canada

Pages: 137 - 151

Year of Publication: 1987

ISBN:0-89791-239-4

Authors

Nancy A. Lynch	Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, Massachusetts
Mark R. Tuttle	Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, Massachusetts

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGOPS: ACM Special Interest Group on Operating Systems

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 73, Citation Count: 125

Additional Information:

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/41840.41852 What is a DOI?

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.

	AS87	Bowen Alpern and Fred B. Schneider. Proving boolean combinations of deterministic properties. In Proceedings o/ Seeo~td Annual Symposium on Logic in Computer Science, June 1987.
	BKP84	Howard Barringer , Ruurd Kuiper , Amir Pnueli, Now you may compose temporal logic specifications, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.51-63, December 1984 [doi>10.1145/800057.808665]
	Blo87	Bard Bloom, Constructing two-writer atomic registers, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.249-259, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41861]
	FLMW87	A. Fekete , N. Lynch , M. Merrit , W. Weihl, Nested transactions and read-write locking, Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.97-111, March 23-25, 1987, San Diego, California, United States [doi>10.1145/28659.28669]
	FLS87	Alan Fekete, N~ncy Lynch, and Liuba Shrira. A modular proof of correctness for a network synchronizer. 1987. In progress.
	Fra86	Nissim Francez, Fairness, Springer-Verlag New York, Inc., New York, NY, 1986
	GHS83	R. G. Gallager , P. A. Humblet , P. M. Spira, A Distributed Algorithm for Minimum-Weight Spanning Trees, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.1, p.66-77, Jan. 1983 [doi>10.1145/357195.357200]
	GL87	Kenneth J. Goldman , Nancy A. Lynch, Quorum consensus in nested transaction systems, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.27-41, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41843]
	Har87	David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
	HLMW87	Maurice Herlihy, Nancy Lynch, Michael Merritt, and William Weihl. On the correctness of orphan elimination algorithms. In Proceeding~ of the 17th Annual IEEE Symposium on Fault-Tolerant Computing, July 1987.
	Hoa85	C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
	Lam83	Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
	LM86	N. A. Lynch , M. Merritt, INTRODUCTION TO THE THEORY OF NESTED TRANSACTIONS, Massachusetts Institute of Technology, Cambridge, MA, 1986
	LS84a	Simon S. Lala and A. Udaya Shankar. Protocol verification via projections. IEEE Transactions ou Software Engineering, SE-10(4)'325-342, july 1984.
	LS84b	Leslie Lamport , Fred B. Schneider, The ``Hoare Logic'' of CSP, and All That, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.2, p.281-296, April 1984 [doi>10.1145/2993.357247]
	LT87	N. A. Lynch , M. Tuttle, HIERARCHICAL CORRECTNESS PROOFS FOR DISTRIBUTED ALGORITHMS, Massachusetts Institute of Technology, Cambridge, MA, 1987
	Lyn83	N. A. Lynch, CONCURRENCY CONTROL FOR RESILIENT NESTED TRANSACTIONS, Massachusetts Institute of Technology, Cambridge, MA, 1983
	Lyn86	Nancy Lynch. Unpublished notes, 1986.
	Mil80	R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	MP81a	Zohar Manna , Amir Pnueli, Verification of Concurrent Programs: Temporal Proof Principles, Logic of Programs, Workshop, p.200-252, May 01, 1981
	MP81b	Zohar Manna and Amir Pnueli. Verification of concurrent programs" the temporal framework. In Robert S. Boyer and J. Strother Moore, editors, The Correctness Proble~ in Computer Science, pages 215-273, Academic Press, London, 1981.
	OG76	Susan Owicki and David Cries. An axiomatic proof technique for parallel programs I. Acts lnformatica, 6(4)'319-340, August 1976.
	Sch80	Arnold Schonhage. Personal Communication, 1980.
	Sta84	E. W. Stark, FOUNDATIONS OF A THEORY OF SPECIFICATION FOR DISTRIBUTED SYSTEMS, Massachusetts Institute of Technology, Cambridge, MA, 1984
	Wel87	Jennifer L. Welch. Synthesis of efficient mutual exclusion algorithms. 1987. In progress.

CITED BY 125

	Phillip B. Gibbons , Michael Merritt , Kourosh Gharachorloo, Proving sequential consistency of high-performance shared memories (extended abstract), Proceedings of the third annual ACM symposium on Parallel algorithms and architectures, p.292-303, July 21-24, 1991, Hilton Head, South Carolina, United States
	Nir Shavit , Dan Touitou, Elimination trees and the construction of pools and stacks: preliminary version, Proceedings of the seventh annual ACM symposium on Parallel algorithms and architectures, p.54-63, June 24-26, 1995, Santa Barbara, California, United States
	C. S. Jutla , E. Knapp , J. R. Rao, A predicate transformer approach to semantics of parallel programs, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.249-263, June 1989, Edmonton, Alberta, Canada
	Nir Shavit , Dan Touitou, Software transactional memory, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, p.204-213, August 20-23, 1995, Ottowa, Ontario, Canada
	B. Jonsson, A fully abstract trace model for dataflow networks, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.155-165, January 11-13, 1989, Austin, Texas, United States
	O. Goldreich , A. Herzberg , Y. Mansour, Source to destination communication in the presence of faults, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.85-101, June 1989, Edmonton, Alberta, Canada
	Haim Gaifman , Michael J. Maher , Ehud Shapiro, Replay, recovery, replication, and snapshots of nondeterministic concurrent programs, Proceedings of the tenth annual ACM symposium on Principles of distributed computing, p.241-255, August 19-21, 1991, Montreal, Quebec, Canada
	Ching Tsun Chou , Eli Gafni, Understanding and verifying distributed algorithms using stratified decomposition, Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, p.44-65, August 15-17, 1988, Toronto, Ontario, Canada
	Martin Abadi , Gordon Plotkin, A logical view of composition and refinement, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.323-332, January 21-23, 1991, Orlando, Florida, United States
	Roberto Segala , Nancy Lynch, Probabilistic simulations for probabilistic processes, Nordic Journal of Computing, v.2 n.2, p.250-273, Summer 1995
	Yehuda Afek , David S. Greenberg , Michael Merritt , Gadi Taubenfeld, Computing with faulty shared memory, Proceedings of the eleventh annual ACM symposium on Principles of distributed computing, p.47-58, August 10-12, 1992, Vancouver, British Columbia, Canada
	Nils Klarlund , Mogens Nielsen , Kim Sunesen, Automated logical verification based on trace abstractions, Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing, p.101-110, May 23-26, 1996, Philadelphia, Pennsylvania, United States
	Martín Abadi , Leslie Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.73-132, Jan. 1993
	Manfred Broy, Functional specification of time-sensitive communicating systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.1, p.1-46, Jan. 1993
	Phillip B. Gibbons , Michael Merritt, Specifying non-blocking shared memories (extended abstract), Proceedings of the fourth annual ACM symposium on Parallel algorithms and architectures, p.306-315, June 29-July 01, 1992, San Diego, California, United States
	Thomas A. Henzinger , Orna Kupferman , Sriram K. Rajamani, Fair simulation, Information and Computation, v.173 n.1, p.64-81, February 25, 2002
	Judi Romijn, A Timed Verification of the IEEE 1394 Leader Election Protocol, Formal Methods in System Design, v.19 n.2, p.165-194, September 2001
	Nir Shavit , Asaph Zemach, Diffracting trees, ACM Transactions on Computer Systems (TOCS), v.14 n.4, p.385-428, Nov. 1996
	A. P. Sistla , J. L. Welch, Efficient distributed recovery using message logging, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.223-238, June 1989, Edmonton, Alberta, Canada
	Yehuda Afek , Danny Dolev , Hagit Attiya , Eli Gafni , Michael Merritt , Nir Shavit, Atomic snapshots of shared memory, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.1-13, August 22-24, 1990, Quebec City, Quebec, Canada
	John Kyu Lee, Precision locking for nested transaction systems, Proceedings of the second international conference on Information and knowledge management, p.674-683, November 01-05, 1993, Washington, D.C., United States
	Yehuda Afek , Michael Merritt , Gadi Taubenfeld, The power of multi-objects (extended abstract), Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing, p.213-222, May 23-26, 1996, Philadelphia, Pennsylvania, United States
	Alan Fekete, Liveness conditions in model-based service specifications: a case study, ACM SIGSOFT Software Engineering Notes, v.20 n.4, p.62-71, Oct. 1995
	Nir Shavit , Asaph Zemach, Combining funnels: a new twist on an old tale…, Proceedings of the seventeenth annual ACM symposium on Principles of distributed computing, p.61-70, June 28-July 02, 1998, Puerto Vallarta, Mexico
	Rajeev Alur , Radu Grosu, Modular refinement of hierarchic reactive machines, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.390-402, January 19-21, 2000, Boston, MA, USA
	Yehuda Afek , Hagit Attiya , Alan Fekete , Michael Fischer , Nancy Lynch , Yishay Mansour , Dai-Wei Wang , Lenore Zuck, Reliable communication over unreliable channels, Journal of the ACM (JACM), v.41 n.6, p.1267-1297, Nov. 1994
	Bengt Jonsson, Compositional specification and verification of distributed systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.2, p.259-303, March 1994
	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
	Yishay Mansour , Baruch Schieber, The intractability of bounded protocols for on-line sequence transmission over non-FIFO channels, Journal of the ACM (JACM), v.39 n.4, p.783-799, Oct. 1992
	Yehuda Afek , David S. Greenberg , Michael Merritt , Gadi Taubenfeld, Computing with faulty shared objects, Journal of the ACM (JACM), v.42 n.6, p.1231-1274, Nov. 1995
	Gurdip Singh, A methodology for designing communication protocols, ACM SIGCOMM Computer Communication Review, v.24 n.4, p.245-255, Oct. 1994
	N. Lynch, A hundred impossibility proofs for distributed computing, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.1-28, June 1989, Edmonton, Alberta, Canada
	Y. Mansour , B. Schieber, The intractability of bounded protocols for non-FIFO channels, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.59-72, June 1989, Edmonton, Alberta, Canada
	Nancy Lynch , Hagit Attiya, Using mappings to prove timing properties, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.265-280, August 22-24, 1990, Quebec City, Quebec, Canada
	Luca de Alfaro , Thomas A. Henzinger, Interface automata, ACM SIGSOFT Software Engineering Notes, v.26 n.5, Sept. 2001
	Faith Fich , Maurice Herlihy , Nir Shavit, On the space complexity of randomized synchronization, Journal of the ACM (JACM), v.45 n.5, p.843-862, Sept. 1998
	A. Udaya Shankar, An introduction to assertional reasoning for concurrent systems, ACM Computing Surveys (CSUR), v.25 n.3, p.225-262, Sept. 1993
	Mingsheng Ying, Additive models of probabilistic processes, Theoretical Computer Science, v.275 n.1-2, p.481-519, March 28 2002
	Yehuda Afek , Geoffrey Brown , Michael Merritt, Lazy caching, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.182-205, Jan. 1993
	Tevfik Bultan , Xiang Fu , Richard Hull , Jianwen Su, Conversation specification: a new approach to design and analysis of e-service composition, Proceedings of the 12th international conference on World Wide Web, May 20-24, 2003, Budapest, Hungary
	Maurice Herlihy , Nancy Lynch , Michael Merritt , William Weihl, On the correctness of orphan management algorithms, Journal of the ACM (JACM), v.39 n.4, p.881-930, Oct. 1992
	James Aspnes , Maurice Herlihy , Nir Shavit, Counting networks, Journal of the ACM (JACM), v.41 n.5, p.1020-1048, Sept. 1994
	Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994
	Ricardo Galli , Yuhua Luo, Mu3D: a causal consistency protocol for a collaborative VRML editor, Proceedings of the fifth symposium on Virtual reality modeling language (Web3D-VRML), p.53-62, February 20-24, 2000, Monterey, California, United States
	Gurdip Singh, Constraint-based structuring of distributed protocols, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, p.266, August 20-23, 1995, Ottowa, Ontario, Canada
	Bard Bloom, Structured operational semantics as a specification language, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.107-117, January 23-25, 1995, San Francisco, California, United States
	Nancy Lynch , Nir Shavit , Alex Shvartsman , Dan Touitou, Counting networks are practically linearizable, Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing, p.280-289, May 23-26, 1996, Philadelphia, Pennsylvania, United States
	Ehud Shapiro, Separating concurrent languages with categories of language embeddings, Proceedings of the twenty-third annual ACM symposium on Theory of computing, p.198-208, May 05-08, 1991, New Orleans, Louisiana, United States
	Nancy A. Lynch , Yishay Mansour , Alan Fekete, Data link layer: two impossibility results, Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, p.149-170, August 15-17, 1988, Toronto, Ontario, Canada
	Da-Wei Wang , Lenore Zuck, Real-time sequence transmission problem, Proceedings of the tenth annual ACM symposium on Principles of distributed computing, p.111-123, August 19-21, 1991, Montreal, Quebec, Canada
	Alan Fekete , Nancy Lynch , Yishay Mansour , John Spinelli, The impossibility of implementing reliable communication in the face of crashes, Journal of the ACM (JACM), v.40 n.5, p.1087-1107, Nov. 1993
	Kenneth J. Goldman , Nancy Lynch, Quorum consensus in nested-transaction systems, ACM Transactions on Database Systems (TODS), v.19 n.4, p.537-585, Dec. 1994
	M. Bravetti , A. Aldini, Discrete time generative-reactive probabilistic processes with different advancing speeds, Theoretical Computer Science, v.290 n.1, p.355-406, 1 January 2003
	Paul C. Attie , E. Allen Emerson, Synthesis of concurrent programs for an atomic read/write model of computation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.2, p.187-242, March 2001
	Hakan Erdogmus, Architecture-driven verification of concurrent systems, Nordic Journal of Computing, v.4 n.4, p.380-413, Winter 1997
	Roberto Segala, Verification of randomized distributed algorithms, Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science, Springer-Verlag New York, Inc., New York, NY, 2002
	Roberto Passerone , Luca de Alfaro , Thomas A. Henzinger , Alberto L. Sangiovanni-Vincentelli, Convertibility verification and converter synthesis: two faces of the same coin, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.132-139, November 10-14, 2002, San Jose, California
	Maurice H. ter Beek , Jetty Kleijn, Modularity for teams of I/O automata, Information Processing Letters, v.95 n.5, p.487-495, 15 September 2005
	Nancy Lynch , Roberto Segala , Frits Vaandrager, Hybrid I/O automata, Information and Computation, v.185 n.1, p.105-157, August 25, 2003
	M. Merritt , A. Orda , S. R. Sachs, Formal Verification of a Distributed Computer System, Formal Methods in System Design, v.10 n.1, p.93-125, February 1997
	Paul C. Attie , Anish Arora , E. Allen Emerson, Synthesis of fault-tolerant concurrent programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.1, p.125-185, January 2004
	Rajeev Alur , Radu Grosu, Modular refinement of hierarchic reactive machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.2, p.339-369, March 2004
	Xingwu Liu, Evaluation of the capability of interaction, ACM SIGGROUP Bulletin, v.24 n.3, December 2003
	A. Udaya Shankar , Simon S. Lam, A stepwise refinement heuristic for protocol construction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.3, p.417-461, July 1992
	Kenneth J. Goldman , Nancy A. Lynch, Quorum consensus in nested transaction systems, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.27-41, August 10-12, 1987, Vancouver, British Columbia, Canada
	Matteo Frigo , Victor Luchangco, Computation-centric memory models, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.240-249, June 28-July 02, 1998, Puerto Vallarta, Mexico
	Simon S. Lam , A. Udaya Shankar, A Relational Notation for State Transition Systems, IEEE Transactions on Software Engineering, v.16 n.7, p.755-775, July 1990
	M. G. Staskauskas, Formal Derivation of Concurrent Programs: An Example from Industry, IEEE Transactions on Software Engineering, v.19 n.5, p.503-528, May 1993
	Jennifer L. Welch , Leslie Lamport , Nancy Lynch, A lattice-structured proof of a minimum spanning, Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, p.28-43, August 15-17, 1988, Toronto, Ontario, Canada
	Faith Fich , Maurice Herlihy , Nir Shavit, On the space complexity of randomized synchronization, Proceedings of the twelfth annual ACM symposium on Principles of distributed computing, p.241-249, August 15-18, 1993, Ithaca, New York, United States
	Leslie Lamport, Fairness and hyperfairness, Distributed Computing, v.13 n.4, p.239-245, November 2000
	Yehuda Afek , Hagit Attiya , Danny Dolev , Eli Gafni , Michael Merritt , Nir Shavit, Atomic snapshots of shared memory, Journal of the ACM (JACM), v.40 n.4, p.873-890, Sept. 1993
	Jeffrey J. P. Tsai , Alan Liu , Eric Juan , Avinash Sahay, Knowledge-Based Software Architectures: Acquisition, Specification, and Verification, IEEE Transactions on Knowledge and Data Engineering, v.11 n.1, p.187-201, January 1999
	Dean Kuo, Model and verification of a data manager based on ARIES, ACM Transactions on Database Systems (TODS), v.21 n.4, p.427-479, Dec. 1996
	Alan Feteke, Formal Models of Communication Services: A Case Study, Computer, v.26 n.8, p.37-47, August 1993
	Edgar Knapp, An exercise in the formal derivation of parallel programs: maximum flows in graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.2, p.203-223, April 1990
	Ying Liu , Ambuj K. Singh , Rajive L. Bagrodia, A Decompositional Approach to the Design of Parallel Programs, IEEE Transactions on Software Engineering, v.20 n.12, p.914-932, December 1994
	Nancy Lynch, Some perspectives on PODC, Distributed Computing, v.16 n.2-3, p.71-74, September 2003
	Simon Doherty , David L. Detlefs , Lindsay Grove , Christine H. Flood , Victor Luchangco , Paul A. Martin , Mark Moir , Nir Shavit , Guy L. Steele, Jr., DCAS is not a silver bullet for nonblocking algorithm design, Proceedings of the sixteenth annual ACM symposium on Parallelism in algorithms and architectures, June 27-30, 2004, Barcelona, Spain
	Gurdip Singh, Constraint-based structuring of network protocols, Distributed Computing, v.12 n.1, p.1-12, March 1999
	David Griffioen , Frits Vaandrager, A theory of normed simulations, ACM Transactions on Computational Logic (TOCL), v.5 n.4, p.577-610, October 2004
	Jonathan Burton , Maciej Koutny , Giuseppe Pappalardo, Relating communicating processes with different interfaces, Fundamenta Informaticae, v.59 n.1, p.1-37, January 2004
	Anna Pogosyants , Roberto Segala , Nancy Lynch, Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study, Distributed Computing, v.13 n.3, p.155-186, July 2000
	Reino Kurki-Suonio, Operational specification with joint actions: serializable databases, Distributed Computing, v.6 n.1, p.19-37, July 1992
	Fong Pong , Michel Dubois, Formal Automatic Verification of Cache Coherence in Multiprocessors with Relaxed Memory Models, IEEE Transactions on Parallel and Distributed Systems, v.11 n.9, p.989-1006, September 2000
	Tamer Elsharnouby , A. Udaya Shankar, Using SeSFJava in teaching introductory network courses, ACM SIGCSE Bulletin, v.37 n.1, 2005
	Jeffrey J. P. Tsai , Eric Y. T. Juan , Avinash Sahay, Model and Algorithm for Efficient Verification of High-Assurance Properties of Real-Time Systems, IEEE Transactions on Knowledge and Data Engineering, v.15 n.2, p.405-422, February 2003
	Manfred Broy, Algebraic and functional specification of an interactive serializable database interface, Distributed Computing, v.6 n.1, p.5-18, July 1992
	Nancy A. Lynch , Hagit Attiya, Using mappings to prove timing properties, Distributed Computing, v.6 n.2, p.121-139, September 1992
	Panagiota Fatourou , Maurice Herlihy, Read-modify-write networks, Distributed Computing, v.17 n.1, p.33-46, February 2004
	Jennifer L. Welch , Nancy A. Lynch, A modular drinking philosophers algorithm, Distributed Computing, v.6 n.4, p.233-244, July 1993
	Bengt Jonsson , Amir Pnueli , Camilla Rump, Proving refinement using transduction, Distributed Computing, v.12 n.2/3, p.129-149, June 1999
	Natarajan Shankar, Automated verification using deduction, exploration, and abstraction, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
	Bengt Jonsson, A fully abstract trace model for dataflow and asynchronous networks, Distributed Computing, v.7 n.4, p.197-212, May 1994
	Viktor Vafeiadis , Maurice Herlihy , Tony Hoare , Marc Shapiro, Proving correctness of highly-concurrent linearisable objects, Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming, March 29-31, 2006, New York, New York, USA
	Simon S. Lam , A. Udaya Shankar, Specifying modules to satisfy interfaces: a state transition system approach, Distributed Computing, v.6 n.1, p.39-63, July 1992
	Amos Israeli , Amnon Shaham, Time and space optimal implementations of atomic multi-writer register, Information and Computation, v.200 n.1, p.62-106, 1 July 2005
	Alan Jeffrey , Julian Rathke, A fully abstract may testing semantics for concurrent objects, Theoretical Computer Science, v.338 n.1-3, p.17-63, 10 June 2005
	Xiang Fu , Tevfik Bultan , Jianwen Su, Conversation protocols: a formalism for specification and verification of reactive electronic services, Theoretical Computer Science, v.328 n.1-2, p.19-37, 29 November 2004
	S. S. Lam , A. U. Shankar, A Theory of Interfaces and Modules - I: Composition Theorem, IEEE Transactions on Software Engineering, v.20 n.1, p.55-71, January 1994
	Eugene W. Stark, On behaviour equivalence for probabilistic I/O automata and its relationship to probabilistic bisimulation, Journal of Automata, Languages and Combinatorics, v.8 n.2, p.361-395, April 2003
	Maurice Herlihy , Nir Shavit , Orli Waarts, Linearizable counting networks, Distributed Computing, v.9 n.4, p.193-203, February 1996
	Michael Merritt, Introduction, Distributed Computing, v.12 n.2/3, p.55-56, June 1999
	Luboš Brim , Ivana Černá , Pavlína Vařeková , Barbora Zimmerova, Component-interaction automata as a verification-oriented component-based system specification, ACM SIGSOFT Software Engineering Notes, v.31 n.2, March 2006
	I. B. Bourdonov , A. S. Kossatchev , V. V. Kuliamin, Formalization of test experiments, Programming and Computing Software, v.33 n.5, p.239-260, September 2007
	Michel Raynal, A simple taxonomy for distributed mutual exclusion algorithms, ACM SIGOPS Operating Systems Review, v.25 n.2, p.47-50, April 1991
	Maciej Koutny , Giuseppe Pappalardo, Behaviour Abstraction for Communicating Sequential Processes, Fundamenta Informaticae, v.48 n.1, p.21-54, January 2001
	Alan Fekete , Nancy Lynch , William E. Weihl, A serialization graph construction for nested transactions, Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.94-108, April 02-04, 1990, Nashville, Tennessee, United States
	Wan Fokkink , Jun Pang , Jaco De Pol, Cones and foci: A mechanical framework for protocol verification, Formal Methods in System Design, v.29 n.1, p.1-31, July 2006
	Zhe Dang , Oscar H. Ibarra , Jianwen Su, On composition and lookahead delegation of e-services modeled by automata, Theoretical Computer Science, v.341 n.1, p.344-363, 5 September 2005
	Danny Dolev, Century papers at the first quarter-century milestone, Proceedings of the twenty-fifth annual ACM symposium on Principles of distributed computing, p.3-4, July 23-26, 2006, Denver, Colorado, USA
	Monika Solanki , Antonio Cau , Hussein Zedan, ASDL: a wide spectrum language for designing web services, Proceedings of the 15th international conference on World Wide Web, May 23-26, 2006, Edinburgh, Scotland
	R. P. Kurshan , M. Merritt , A. Orda , S. R. Sachs, Modelling Asynchrony with a Synchronous Model, Formal Methods in System Design, v.15 n.3, p.175-199, Nov. 1999
	R. Negulescu , J. A. Brzozowski, Relative Liveness: From Intuition to Automated Verification, Formal Methods in System Design, v.12 n.1, p.73-115, Jan., 1998
	James Aspnes , Alan Fekete , Nancy A. Lynch , Michael Merritt , William E. Weihl, A Theory of Timestamp-Based Concurrency Control for Nested Transactions, Proceedings of the 14th International Conference on Very Large Data Bases, p.431-444, August 29-September 01, 1988
	Edward G. Amoroso, Creating formal specifications from requirements documents, ACM SIGSOFT Software Engineering Notes, v.20 n.1, p.67-70, Jan. 1995
	Vijay D'silva , S. Ramesh , Arcot Sowmya, Synchronous Protocol Automata: A Framework for Modelling and Verification of SoC Communication Architectures, Proceedings of the conference on Design, automation and test in Europe, p.10390, February 16-20, 2004
	Y. Afek , G. Brown , M. Merritt, A lazy cache algorithm, Proceedings of the first annual ACM symposium on Parallel algorithms and architectures, p.209-222, June 18-21, 1989, Santa Fe, New Mexico, United States
	Xiaojun Liu , Edward A. Lee, CPO semantics of timed interactive actor networks, Theoretical Computer Science, v.409 n.1, p.110-125, December, 2008
	Amir Herzberg , Igal Yoffe, The layered games framework for specifications and analysis of security protocols, International Journal of Applied Cryptography, v.1 n.2, p.144-159, November 2008
	Toufik Taibi, Formal specification and validation of multi-agent behaviour using TLA+ and TLC model checker, International Journal of Artificial Intelligence and Soft Computing, v.1 n.1, p.99-113, November 2008
	Shahram Esmaeilsabzali , Nancy A. Day , Farhad Mavaddat, Interface Automata with Complex Actions: Limiting Interleaving in Interface Automata, Fundamenta Informaticae, v.82 n.4, p.465-512, February 2008
	Roberto Segala, The power of simulation relations, Proceedings of the twenty-seventh ACM symposium on Principles of distributed computing, August 18-21, 2008, Toronto, Canada
	Shiva Nejati , Mehrdad Sabetzadeh , Marsha Chechik , Sebastian Uchitel , Pamela Zave, Towards compositional synthesis of evolving systems, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
	Jay Ligatti , Lujo Bauer , David Walker, Run-Time Enforcement of Nonsafety Policies, ACM Transactions on Information and System Security (TISSEC), v.12 n.3, p.1-41, January 2009