Bilateral Proofs of Safety and Progress Properties of
Concurrent Programs Unpublished manuscript,
Oct. 2016.
Mapping among the nodes of infinite trees: A variation of
Koenig's infinity lemma. Information Processing Letters, Jan. 2015.
A denotational semantic theory of concurrent systems.
This paper proposes a general denotational semantic theory suitable
for most concurrent systems. It is based on well-known concepts of
events, traces and specifications of systems as sets of traces. Unpublished
manuscript. Aug. 2014.
A Secure Voting Scheme based on Rational Self-Interest. Formal
Aspects of Computing, Volume 24, Issue 4 (2012), Page
793-805, also available at
the publisher.
Processing Boolean Equalities and Inequalities. Unpublished
manuscript.
Virtual Time and Timeout in Client-Server Networks. Unpublished manuscript.
(with Xiaozhou Li, C. Greg Plaxton)
Maintaining the Ranch Topology. Journal of Parallel and Distributed Computing Vol. 70(11), Nov. 2010, pp 1142--1158.
(with Tony Hoare) (with Ankur Gupta) Synthesizing Programs over Recursive Data Structures (Unpublished). (with Markus Kaltenbach) A Theory of Hints in
Model checking, Derivation
of a Parallel String Matching Algorithm, (with Ham Richards)
In
Memoriam, Edsger Wybe Dijkstra (1930-2002).
A Reduction Theorem for Concurrent Object-Oriented Programs, (with Young-ri Choi, Amit Garg, Siddhartha Rai, Harrick Vin) Orchestrating Computations on the World-wide Web, A Simple,
Object-based View of Multiprogramming, (with Edsger W. Dijkstra) Designing a Calculational Proof of Cantor's Theorem, A Walk over the Shortest Path: Dijkstra's Algorithm Viewed as
Fixed-Point Computation,
Strategies to Combat Software Piracy
January 2000 (Unpublished).
(with Rajeev Joshi)
Maximally Concurrent Programs (with Rajeev Joshi)
On the Impossibility of Robust Solutions for Fair Resource
allocation (Unpublished).
Generating-Functions
of Interconnection Networks Modular
Multiprogramming, An Object Model
for Multiprogramming, Proc. 10th. IPPS/SPDP 98 Workshops, Jose Rolim (ed.),
(with Al Carruth) Proof
of a Real-Time Mutual-Exclusion Algorithm, A logic
for Concurrent Programming (in two parts): Safety and Progress, Powerlist:
A Structure for Parallel Recursion, TOPLAS, Vol. 16, No. 6,
pp. 1737-1767, November 1994.
Loosely
Coupled Processes, Future Generations Computer Systems 8, 269-286, North-Holland,
1992.
(with David Gries) A
Constructive Proof of Vizing's Theorem Phase
Synchronization Equational
Reasoning About Nondeterministic Processes, Specifying
Concurrent Objects as Communicating Processes, (with K. Mani Chandy) Proofs
of Distributed Algorithms: An Exercise Specification
Structuring, A Foundation
of Parallel Programming, A Simple Proof
of a Simple Consensus Algorithm (with K. M. Chandy) Another view on
fairness A rebuttal to Dijkstra's position on fairness.
(with K. M. Chandy and R. L. Bagrodia) A
Message Based Approach to Discrete Event Simulation (with K. Mani Chandy) Systolic Algorithms as Programs (with K. Mani Chandy) An
Example of Stepwise Refinement of Distributed Programs: Quiescence
Detection Axioms for Memory Access in Asynchronous Hardware Distributed Discrete Event Simulation (with K. M. Chandy) How Processes Learn (with K. M. Chandy) The
Drinking Philosophers Problem Detecting Termination of Distributed Computations Using Markers (with K. M. Chandy and Laura M. Haas) Distributed
Deadlock Detection (with K. M. Chandy) Distributed
Computation on Graphs: Shortest Path Algorithms
(with K. M. Chandy) A
Distributed Graph Algorithm: Knot Detection
(with K. M. Chandy and Todd Smith) Proving safety and liveness of communicating processes with examples (with K. M. Chandy) A distributed algorithm for detecting resource deadlocks in distributed systems (with David Gries) Finding
Repeated Elements (with K. M. Chandy) Termination
Detection of Diffusing Computations in Communicating Sequential
Processes (with K. M. Chandy) Proofs
of Networks of Processes (with K. M. Chandy) Asynchronous
Distributed Simulation via a Sequence of Parallel Computations
An Exercise in Program Explanation
(with K. M. Chandy) A
simple model of distributed programs based on implementation-hiding
and process autonomy (with K. M. Chandy) Deadlock
Absence Proofs for Networks of Communicating Processes
(with K. M. Chandy) Distributed
Simulation: A case study in design and verification of distributed programs
(with L. Flon) A Unified Approach to the Specification and Verification of Abstract Data Types
Space-Time Trade off in Implementing Certain Set Operations
(with K. M. Chandy and Victor Holmes) Distributed
Simulation of Networks
(with D. Gries) A Linear Sieve Algorithm for Finding Prime Numbers
Some Aspects of the Verification of Loop Computations
An Approach to Formal Definitions and Proofs of Programming Principles
Assertion
Graphs for Verifying and Synthesizing Programs
A Technique of Algorithm Construction on Sequences
Prospects and Limitations of Automatic Assertion Generation for Loop Programs
(with S. Kundu) A Linear Tree Partitioning Algorithm
A
Principle of Algorithm Design on Limited Problem Domain
(with S. K. Basu) Some Classes of Naturally Provable Programs
(with R. Endre Tarjan) Optimal
Chain Partitions of Trees
Remark on Algorithm 246[Z]
(with S. K. Basu) Proving Loop Programs
Orc home page.
(This page includes all the relevant
material for Orc, including the facility to run Orc programs in your browser.)
This paper suggests a theory of composable specification of
concurrent programs that permits: (1) verification of program
code for a given specification, and (2) composition of the
specifications of the components to yield the specification of a
program. The specification consists of both terminal properties
that hold at the end of a program execution (if the execution
terminates) and perpetual properties that hold throughout an
execution. We devise (1) proof techniques for verification,
and (2) composition rules to derive the specification of a
program from those of its components. We employ terminal
properties of components to derive perpetual properties of a
program and conversely. Hence, this proof strategy is called
bilateral. The compositional aspect of the theory is important in
assembling a program out of components some of whose source code
may not be available, as is increasingly the case with
cross-vendor program integration.
Koenig's infinity lemma states that an infinite rooted tree in which
every node has finite degree has an infinite path. A variation of this
lemma about mappings from one tree to another is presented in this
note. Its proof utilizes Koenig's lemma, and Koenig's lemma follows
from this variation.
Formal Methods at the
Crossroads: From Panacea to Foundational Support, ed. Bernhard
K. Aichernig and Tom Maibaum, LNCS 2757, pp 423-438, Springer-Verlag, 2003.
Information Processing Letters, 85(5): 255-260, January 2003.
Programming Methodology, ed. Annabelle McIver and Carroll
Morgan, Springer-Verlag, pp 69-92, 2002.
Proceedings of the Euro-Par 2002, Paderborn, Germany, August 2002.
Formal Methods in System Design,
Vol. 20, No. 1, January 2002.
American Mathematical
Monthly, May 2001.
Information Processing Letters, 77(2--4), pp 197--200, February 2001.
Formal Aspects of
Computing, 2000, 12: 100--119.
Millennial Perspectives in Computer Science:
the proceedings of the 1999 Oxford--Microsoft Symposium in honour of
Sir Tony Hoare.
Proc. NATO Advanced Study Institute on
Calculational System Design,
Marktoberdorf, Germany, July
28-August 9, 1998,
in NATO Science Series, Vol. 173, ed. Manfred
Broy and Ralf Steinbruggen, IOS Press, pp. 131--165, 1999.
Lecture Notes
in Computer Sciences, Springer-Verlag, Vol. 1388, pp. 881-889, 1998.
Parallel Processing Letters,
Vol 6, No. 2, pp 251-257, 1996.
Journal
of Computer
and Software Engineering, Vol.3, No.2, pp 239-300, 1995.
Information Processing Letters, Vol. 41, pp. 131-133, 1992.
Information Processing Letters, Vol. 38,
pp. 81-85, 1991
Corrigenda
41, p. 59, 1992.
Formal Aspects of
Computing, 2:2, 167-195, 1990.
Science of Computer Programming
14, 159-184, 1990.
Developments in
Concurrency and Communication, U.T. Year of Programming Series, Addison-Wesley, 1990.
Proc. Belgian FNRS, International Chair of Computer Science,
Louvain-la-Neuve, March 18-23, 1990.
Proc. 9th International Summer School on Constructive
Methods in Computer Science,
Marktoberdorf, Germany, July 24-August 5,
1988,
in NATO ASI Series, Vol. F 55, ed. Manfred Broy, Springer-Verlag,
pp. 397--433, 1989.
Information Processing Letters, 33:1, pp. 21-24, 1989.
Software Engineering Notes, 13, 3 (July 1988), 21.
IEEE TSE,
Vol. SE-13, No.6, June 1987.
Distributed Computing,
1:177-183, 1986.
ACM Transactions on Programming Languages and
Systems, Vol. 8, No. 3, pp 326-343, July 1986.
ACM Transactions
on Programming Languages and Systems, Vol. 8, 1:142-153, 1986.
Computing Surveys, vol.18, No.1,
pp 39-65, March 1986.
Journal of Distributed Computing,
1:40-52, 1986.
ACM Transactions on Programming
Languages and Systems, Vol. 6, No. 4, pp 632-646, October 1984.
Proc. of PODC, Montreal, Canada, August 17-19, 1983.
ACM Transactions on Computer Systems, Vol. 1, No. 2, pp. 144-156,
May 1983.
ACM Transactions on Programming
Languages and Systems, Vol. 25, No. 11, pp. 833-837,
November 1982.
Communications of the ACM, Vol. 4, No. 4, pp. 678-686,
October 1982.
Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of
distributed computing,
August 1982.
Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of
distributed computing,
August 1982.
Science of Computer Programming, 2:143-152, 1982.
CACM, Vol. 4, No. 1, pp. 37-43, January 1982.
IEEE, Vol. SE-7, No. 4, pp. 417-426,
July 1981.
CACM, Vol. 24, No. 11, pp. 417-426, April 1981.
CACM, Vol. 3, No. 1, pp. 104-109, January 1981.
ACM SIGPLAN Notices, Vol. 15 Issue 7 and 8,
July 1980.
Information Processing Letters, Vol. 9, No. 4, pp. 185-189,
November 1979.
IEEE, Vol. SE-5, No. 5, pp. 440-452,
September 1979.
Proceedings of the IEEE Conference on Specifications of Reliable Software,
Cambridge, Massachusetts, April 1979.
Information Processing Letters, Vol. 8, No. 2, pp. 81-85, February 1979.
Computer Networks, Vol. 3, pp. 105-113, January 1979.
CACM, Vol.21, No. 12, pp. 999-1003, December 1978.
IEEE, Vol. SE-4, No. 6, pp. 478-486, November 1978.
IEEE, Vol. SE-4, No. 5, pp. 410-413, September 1978.
Rechnical Report, TR 83, University of Texas at Austin, August 1978.
IEEE, Vol. SE-4, No. 1, pp. 65-69, January 1978.
SIAM Journal on Computing, Vol. 6, No. 4, December 1977.
SIAM Journal on Computing, Vol. 6, No. 1, pp. 151-154, March 1977.
The proceedings of the thirteenth design automation conference,
San Francisco, California, pp. 479-483, 1976.
Proceedings of the 2nd International Conference on Software
Engineering, San Francisco, California, October 1976.
Information Processing Letters, Vol. 4, No. 1, pp. 24-26, September 1975.
ACM Transactions on Mathematical Software, Vol. 1, No. 3, September 1975.
IEEE, Vol. SE-1, No. 1, pp. 76-86, March 1975.