Selected Publications

Orc related publications.
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 Unpublished manuscript, 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, 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) Verified software: theories, tools, experiments. Vision of a Grand Challenge project (A position paper). LNCS 4171, pp 1--18, Springer Verlag.

(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.