Orc home page.
(This page includes all the relevant
material for Orc, including the facility to run Orc programs in your browser.)

Bilateral Proofs of Safety and Progress Properties of
Concurrent Programs Submitted for Publication,
Oct. 2016.

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.

Mapping among the nodes of infinite trees: A variation of
Koenig's infinity lemma. Information Processing Letters (to
appear), Jan. 2015.

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.

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,

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.

Derivation
of a Parallel String Matching Algorithm,

Information Processing Letters, 85(5): 255-260, January 2003.

(with Ham Richards) In Memoriam, Edsger Wybe Dijkstra (1930-2002).

A Reduction Theorem for Concurrent Object-Oriented Programs,

Programming Methodology, ed. Annabelle McIver and Carroll
Morgan, Springer-Verlag, pp 69-92, 2002.

(with Young-ri Choi, Amit Garg, Siddhartha Rai, Harrick Vin) Orchestrating Computations on the World-wide Web,

Proceedings of the Euro-Par 2002, Paderborn, Germany, August 2002.

A Simple,
Object-based View of Multiprogramming,

Formal Methods in System Design,
Vol. 20, No. 1, January 2002.

(with Edsger W. Dijkstra) Designing a Calculational Proof of Cantor's Theorem,

American Mathematical
Monthly, May 2001.

A Walk over the Shortest Path: Dijkstra's Algorithm Viewed as
Fixed-Point Computation,

Information Processing Letters, 77(2--4), pp 197--200, February 2001.

Strategies to Combat Software Piracy January 2000 (Unpublished).

(with Rajeev Joshi)
Maximally Concurrent Programs

Formal Aspects of
Computing, 2000, 12: 100--119.

(with Rajeev Joshi) On the Impossibility of Robust Solutions for Fair Resource allocation (Unpublished).

Generating-Functions
of Interconnection Networks

Millennial Perspectives in Computer Science:

the proceedings of the 1999 Oxford--Microsoft Symposium in honour of
Sir Tony Hoare.

Modular
Multiprogramming,

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.

An Object Model
for Multiprogramming, Proc. 10th. IPPS/SPDP 98 Workshops, Jose Rolim (ed.),

Lecture Notes
in Computer Sciences, Springer-Verlag, Vol. 1388, pp. 881-889, 1998.

(with Al Carruth) Proof
of a Real-Time Mutual-Exclusion Algorithm,

Parallel Processing Letters,
Vol 6, No. 2, pp 251-257, 1996.

A logic
for Concurrent Programming (in two parts): Safety and Progress,

Journal
of Computer
and Software Engineering, Vol.3, No.2, pp 239-300, 1995.

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

Information Processing Letters, Vol. 41, pp. 131-133, 1992.

Phase
Synchronization

Information Processing Letters, Vol. 38,
pp. 81-85, 1991
Corrigenda

41, p. 59, 1992.

Equational
Reasoning About Nondeterministic Processes,

Formal Aspects of
Computing, 2:2, 167-195, 1990.

Specifying
Concurrent Objects as Communicating Processes,

Science of Computer Programming
14, 159-184, 1990.

(with K. Mani Chandy) Proofs
of Distributed Algorithms: An Exercise

Developments in
Concurrency and Communication, U.T. Year of Programming Series, Addison-Wesley, 1990.

Specification
Structuring,

Proc. Belgian FNRS, International Chair of Computer Science,
Louvain-la-Neuve, March 18-23, 1990.

A Foundation
of Parallel Programming,

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.

A Simple Proof
of a Simple Consensus Algorithm

Information Processing Letters, 33:1, pp. 21-24, 1989.

(with K. M. Chandy and R. L. Bagrodia) A
Message Based Approach to Discrete Event Simulation

IEEE TSE,
Vol. SE-13, No.6, June 1987.

(with K. Mani Chandy) Systolic Algorithms as Programs

Distributed Computing,
1:177-183, 1986.

(with K. Mani Chandy) An
Example of Stepwise Refinement of Distributed Programs: Quiescence
Detection

ACM Transactions on Programming Languages and
Systems, Vol. 8, No. 3, pp 326-343, July 1986.

Axioms for Memory Access in Asynchronous Hardware

ACM Transactions
on Programming Languages and Systems, Vol. 8, 1:142-153, 1986.

Distributed Discrete Event Simulation

Computing Surveys, vol.18, No.1,
pp 39-65, March 1986.

(with K. M. Chandy) How Processes Learn

Journal of Distributed Computing,
1:40-52, 1986.

(with K. M. Chandy) The
Drinking Philosophers Problem

ACM Transactions on Programming
Languages and Systems, Vol. 6, No. 4, pp 632-646, October 1984.

Detecting Termination of Distributed Computations Using Markers

Proc. of PODC, Montreal, Canada, August 17-19, 1983.

(with K. M. Chandy and Laura M. Haas) Distributed
Deadlock Detection

ACM Transactions on Computer Systems, Vol. 1, No. 2, pp. 144-156,
May 1983.

(with K. M. Chandy) Distributed
Computation on Graphs: Shortest Path Algorithms

ACM Transactions on Programming
Languages and Systems, Vol. 25, No. 11, pp. 833-837,
November 1982.

(with K. M. Chandy) A
Distributed Graph Algorithm: Knot Detection

Communications of the ACM, Vol. 4, No. 4, pp. 678-686,
October 1982.

(with K. M. Chandy and Todd Smith) Proving safety and liveness of communicating processes with examples

Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of
distributed computing,
August 1982.

(with K. M. Chandy) A distributed algorithm for detecting resource deadlocks in distributed systems

Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of
distributed computing,
August 1982.

(with David Gries) Finding
Repeated Elements

Science of Computer Programming, 2:143-152, 1982.

(with K. M. Chandy) Termination
Detection of Diffusing Computations in Communicating Sequential
Processes

CACM, Vol. 4, No. 1, pp. 37-43, January 1982.

(with K. M. Chandy) Proofs
of Networks of Processes

IEEE, Vol. SE-7, No. 4, pp. 417-426,
July 1981.

(with K. M. Chandy) Asynchronous
Distributed Simulation via a Sequence of Parallel Computations

CACM, Vol. 24, No. 11, pp. 417-426, April 1981.

An Exercise in Program Explanation

CACM, Vol. 3, No. 1, pp. 104-109, January 1981.

(with K. M. Chandy) A
simple model of distributed programs based on implementation-hiding
and process autonomy

ACM SIGPLAN Notices, Vol. 15 Issue 7 and 8,
July 1980.

(with K. M. Chandy) Deadlock
Absence Proofs for Networks of Communicating Processes

Information Processing Letters, Vol. 9, No. 4, pp. 185-189,
November 1979.

(with K. M. Chandy) Distributed
Simulation: A case study in design and verification of distributed programs

IEEE, Vol. SE-5, No. 5, pp. 440-452,
September 1979.

(with L. Flon) A Unified Approach to the Specification and Verification of Abstract Data Types

Proceedings of the IEEE Conference on Specifications of Reliable Software,
Cambridge, Massachusetts, April 1979.

Space-Time Trade off in Implementing Certain Set Operations

Information Processing Letters, Vol. 8, No. 2, pp. 81-85, February 1979.

(with K. M. Chandy and Victor Holmes) Distributed
Simulation of Networks

Computer Networks, Vol. 3, pp. 105-113, January 1979.

(with D. Gries) A Linear Sieve Algorithm for Finding Prime Numbers

CACM, Vol.21, No. 12, pp. 999-1003, December 1978.

Some Aspects of the Verification of Loop Computations

IEEE, Vol. SE-4, No. 6, pp. 478-486, November 1978.

An Approach to Formal Definitions and Proofs of Programming Principles

IEEE, Vol. SE-4, No. 5, pp. 410-413, September 1978.

Assertion
Graphs for Verifying and Synthesizing Programs

Rechnical Report, TR 83, University of Texas at Austin, August 1978.

A Technique of Algorithm Construction on Sequences

IEEE, Vol. SE-4, No. 1, pp. 65-69, January 1978.

Prospects and Limitations of Automatic Assertion Generation for Loop Programs

SIAM Journal on Computing, Vol. 6, No. 4, December 1977.

(with S. Kundu) A Linear Tree Partitioning Algorithm

SIAM Journal on Computing, Vol. 6, No. 1, pp. 151-154, March 1977.

A
Principle of Algorithm Design on Limited Problem Domain

The proceedings of the thirteenth design automation conference,
San Francisco, California, pp. 479-483, 1976.

(with S. K. Basu) Some Classes of Naturally Provable Programs

Proceedings of the 2nd International Conference on Software
Engineering, San Francisco, California, October 1976.

(with R. Endre Tarjan) Optimal
Chain Partitions of Trees

Information Processing Letters, Vol. 4, No. 1, pp. 24-26, September 1975.

Remark on Algorithm 246[Z]

ACM Transactions on Mathematical Software, Vol. 1, No. 3, September 1975.

(with S. K. Basu) Proving Loop Programs

IEEE, Vol. SE-1, No. 1, pp. 76-86, March 1975.