1 Introduction A Perspective on Formal Methods in Education (2009)
It is tempting for me to give a speech about my latest research. Fortunately, for
Structured Interacting Computations (A position paper) ⋆ (2009)
Abstract. Today, concurrency is ubiquitous, in desktop applications, client-server systems, workflow systems, transaction processing and web services. Design of concurrent systems, particularly in...
Add�ÙandÐ�Ø ���� � �ÜÔÖ as two possible (2009)
¯Define an asynchronous semantics, using labeled transitions. An expression transits to another expression, causing an event. Labels are events. ¯Refine asynchronous semantics to a synchronous...
A walk over the shortest path: Dijkstra’s Algorithm viewed as fixed-point computation (2009)
We present a derivation Dijkstra’s shortest path algorithm[1]. We view the problem as computation of a “greatest solution ” of a set of equations. A UNITY-style computation[0] is then...
An object model for multiprogramming (2009)
Abstract. We have developed a programming model that integrates concurrency with object-based programming. The model includes features for object definition and instantiation, and it supports...
Orchestration in Orc: A Deterministic Distributed Programming Model (2009)
William R. Cook, Jayadev Misra
Abstract. Orc is a new model of distributed programming which provides a strong theoretical foundation for internet computing based on compositions of web-services. Orc combines some of the power and...
Abstract A Timed Semantics of Orc (2009)
Ian Wehrman, David Kitchin, William R. Cook, Jayadev Misra
Orc is a kernel language for structured concurrent programming. Orc provides three powerful combinators that define the structure of a concurrent computation. These combinators support sequential and...
ORIGINAL ARTICLE Concurrent maintenance of rings (2008)
Xiaozhou Li, Jayadev Misra, C. Greg Plaxton, X. Li, J. Misra
Abstract A central problem for structured peer-topeer networks is topology maintenance, that is, how to properly update neighbor variables when nodes join or leave the network, possibly concurrently....
Abstract DETECTING TERMINATION OF DISTRIBUTED COMPUTATIONS USING MARKERS (2008)
A problem of considerable importance in designing computations by process networks, is detection of termination. We propose a very simple algorithm for termination detection in an arbitrary network...
A combination of program-proving ideas and stepwise refinement is used to develop and explain an algorithm which uses a variation of the sieve method for computing primes.
To My Parents Sashibhusan and Shanty Preface (2008)
For every complex problem, there is a solution that is simple, neat and
Transaction Orchestration (2008)
The internet promises a truly global computer where all services and data are available to all users at all time. True internet computing, which we call wide-area computing, will combine multiple...
Active and Concurrent Maintenance of a Structured Peer-to-Peer Network Topology (2008)
Xiaozhou Li, Jayadev Misra, C. Greg Plaxton
A central problem for structured peer-to-peer networks is topology maintenance, that is, how to properly update neighbor variables when nodes join and leave the network, possibly concurrently. In...
A Theorem Relating leads-to and unless Notes on UNITY: 04-88 (2008)
The following theorem has recently been discovered by Ambuj Singh [3]; a very similar result had been observed by Ernie Cohen and J. R. Rao [1] about a year back, in proving a corollary of this...
How to reason with Strong-fairness and No-fairness Notes on UNITY: 31–92 1 The Problem (2008)
Some feel that the UNITY-logic is deficient because it embeds a fixed notion of fairness, namely that each statement be executed infinitely often in any execution. Other notions of fairness, such as...
Software & Systems Modeling manuscript No. (will be inserted by the editor) (2008)
Jayadev Misra, William R. Cook, Computation Orchestration
Abstract The widespread deployment of networked applications and adoption of the internet has fostered an environment in which many distributed services are available. There is great demand to...
1 Problem Statement Phase Synchronization Notes on UNITY: 12-90 (2008)
Consider a set of asynchronous processes where each process executes a sequence of phases; a process begins its next phase only upon completion of its previous phase. What constitutes a phase is...
Progress–Safety–Safety Notes on UNITY: 05-89 (2008)
The PSP rule (PSP is an abbreviation for Progress–Safety–Progress) is a fundamental rule for deriving a progress property from a progress and a safety property. We had no analogous rule for...
1.2 Site name vs. site call: let(M) vs. M............... 5 1.3 Memoization............................. 5
A timed semantics of orc (2008)
Ian Wehrman, David Kitchin, William R. Cook, Jayadev Misra
Orc is a kernel language for structured concurrent programming. Orc provides three powerful combinators that define the structure of a concurrent computation. These combinators support sequential and...
Generalization, Lemma Generation, and Induction in (2008)
John D. Erickson, Matt Kaufmann, Vladimir Lifschitz, Jayadev Misra, John D. Erickson, To Nikki
I would like to thank J Moore for his encouragement and support. His depth of knowledge about theorem proving never ceased to amaze me. He was always able to offer me some kind of wisdom, no matter...
A timed semantics of orc (2008)
Ian Wehrman, David Kitchin, William R. Cook, Jayadev Misra
Abstract. Orc is a kernel language for structured concurrent programming. Orc provides three powerful combinators that define the structure of a concurrent computation. These combinators support...
A Specialization of detects Notes on UNITY: 18-90 (2007)
For a given program, p detects q, for predicates p; q is: p) q and q 7! p It is shown in [1] how certain kinds of detection problems---detection of termination, deadlock,
General Conjunction and Disjunction Rules for (2007)
fconjunctiong; h9 i :: p:ii unless h8 i :: :p:i q:ii h9 i :: q:ii fdisjunctiong 2 Proofs of the Rules In a program we have the restriction that every statement is deterministic and execution of any...
Chapter 5 Asynchronous Compositions of Programs (2007)
data types and the development of data structures. C.ACM, 20(6):396--404, June 1977. [5] C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, London, 1984. [6] E. Knapp....
A Composition Theorem About Fixed Points (2007)
Notes On Unity, Jayadev Misra, T F:fp
llary to the union theorem on the above and (1) 5 Theorem 2: T ) F:FP; T is stable in G; p ensures q in G T p ensures T q in F [] G This work was partially supported by ONR Contracts N00014-87-K-0510...
Proving Progress for Program Sequencing (2007)
Introduction We interpret the program F ; G in operational terms as follows. Program F 's execution is started. If a fixedpoint state of F is reached, the execution of G is started from that...
Soundness of the Substitution Axiom (2007)
Introduction To paraphrase Mark Twain, the unsoundness of the substitution axiom has been greatly exaggerated. Last June, Jan van de Snepscheut showed me an example where p unless q, in a given...
.7> ff 1 : hP(sem)i ; fi 1 : hx := x + 1i ; fl 1 : hV(sem)i endloop [] loop ff 2 : hP(sem)i fi 2 : hy := y + 1i fl 2 : hV(sem)i coend endloop This material is based in part upon work supported by...
A Theorem Relating leads-to and unless (2007)
F21.6> r , trivially r 7! q , since p 7! q from p ensures q r unless q , from p ensures q we have p unless q 2) p 7! s ; s 7! q : Inductively, we may assume from p 7! s that there is a predicate...
In Memoriam Woodrow Wilson Bledsoe (2007)
Robert S. Boyer, James C. Browne, Jayadev Misra, Woodrow Wilson Bledsoe
by mathematics and recalls spending "hours just roaming around, sometimes working mathematics problems mentally" (Bledsoe 1976). When Woody was 12, his father died. It was a devastating...
CHARACTERISTIC FORqCTIONS AS A BASIS OF DATA SPECIFICATION AND PROOF + (2007)
A method for specification of data abstraction, using charac-teristic functions, is proposed in this paper It is shown that the notion of characteristic functions is a generalization of V-function of...
QUiCYADDER: A NEW SOLUTION TO AI OLD PROBLEM (2007)
introduction We propose a new design for fixed point adders The speed of the proposed circuit compares favorably with the'ones in practice [1] More importantly the major part of the circuit is...
THE UNIVERSITY OF TEXAS AT AUSTIN Assertion Graphs for Verifying and Synthsizing Programs (2007)
Tilak Agerwala, Tilak Agerwala, Jayadev Misra, Jayadev Misra
by
Woodrow W. Bledsoe, Philip Chang, Daniel Chester, Jayadev Misra, Laurant Siklossy, Robert Simmons, ...
by
A Note on Subgoal Induction (2007)
Jayadev Misra, Subgoal Induction, Introduced Morris
We define "power " of an induction rule and show that a slight modification to subgoal induction rule increases its power We give an infinite sequence of induction rules of strictly...
Strategies to Combat Software Piracy (2007)
It is impossible to combat software piracy as long as the machines on which the programs execute are indistinguishable; then, any program that can execute on one machine may be copied for execution...
A walk over the shortest path: Dijkstra's Algorithm viewed as xed-point computation (2007)
We present a derivation Dijkstra's shortest path algorithm[1]. We view the problem as computation of a \greatest solution " of a set of equations. A UNITY-style computation[0] is then...
For every complex problem, there is a solution that is simple, neat and (2007)
wrong, so noted H. L. Mencken. 1 It is with great trepidation, therefore, that I propose a simple, and mostly neat, solution for designing distributed applications. The solution consists of an...
Specification Structuring (2007)
Programs that accept inputs, compute and produce outputs are specified by describing all possible inputs and the corresponding outputs. When the possible inputs are finite in number---as is the case...
Proofs of Distributed Algorithms: An Exercise (2007)
It is generally assumed that formal proofs of programs are considerably longer and more tedious than their informal counterparts. Informal proofs employ a form of common sense reasoning whereby...
Generating-Functions of Interconnection Networks (2007)
Generating functions have long been used to analyze properties of sequences of numbers. In this note, we use generating functions to analyze a class of combinatorial objects, called interconnection...
An object model for multiprogramming (2007)
Abstract. We have developed a programming model that integrates concurrency with object-based programming. The model includes features for object definition and instantiation, and it supports...
A language for task orchestration and its semantic properties (2006)
David Kitchin, William R. Cook, Jayadev Misra
Abstract. Orc is a new language for task orchestration, a form of concurrent programming with applications in workflow, business process management, and web service orchestration. Orc provides...
Semantic properties of asynchronous Orc (2006)
David Kitchin, William R. Cook, Jayadev Misra
Orc is a new language for task orchestration, a form of concurrent programming with applications in workflow, business process management, and web service orchestration. Orc provides constructs to...
Jayadev Misra, Copyright Jayadev Misra
“He who loves practice without theory is like the sailor who boards ship without a rudder and compass and never knows where he may be cast.” Leonardo da Vinci (1452–1519) Computer programming...
Concurrent Maintenance of Rings (2006)
Xiaozhou Li Jayadev, Xiaozhou Li, Jayadev Misra, C. Greg Plaxton
A central problem for structured peer-to-peer networks is topology maintenance, that is, how to properly update neighbor variables when membership changes (i.e., nodes join or leave the network,...
Concurrent maintenance of rings (2006)
Xiaozhou Li, Jayadev Misra, C. Greg Plaxton
A central problem for structured peer-to-peer networks is topology maintenance, that is, how to properly update neighbor variables when membership changes (i.e., nodes join or leave the network,...
Workflow patterns in orc (2006)
William R. Cook, Sourabh Patwardhan, Jayadev Misra
Abstract. Van der Aalst recently proposed a set of workflow patterns to characterize the kinds of control flow that appear frequently in workflow processes. These patterns are useful for evaluating...
Jayadev Misra, Copyright Jayadev Misra
“He who loves practice without theory is like the sailor who boards ship without a rudder and compass and never knows where he may be cast.” Leonardo da Vinci (1452–1519) Computer programming...
Xiaozhou Li The, Xiaozhou Li, Greg Plaxton Supervisor, Lorenzo Alvisi, Gustavo De Veciana, Jayadev Misra, ...
vi List of Figures xi Chapter 1
Active and Concurrent Topology Maintenance (2004)
Xiaozhou Li Jayadev, Xiaozhou Li, Jayadev Misra, C. Greg Plaxton
A central problem for structured peer-to-peer networks is topology maintenance, that is, how to properly update neighbor variables when nodes join and leave the network, possibly concurrently. In...
Active and Concurrent Topology Maintenance (2004)
Xiaozhou Li, Jayadev Misra, C. Greg Plaxton
Depending on whether the neighbor variables are immediately updated once a membership change occurs, there are two general approaches to topology maintenance: the passive approach and the active...
Demonic Nondeterminacy: A Tribute to Edsger Wybe Dijkstra (2003)
Please permit me to talk about the paper ”Guarded Commands, Nondeterminacy,
Synthesizing Programs over Recursive Data Structures (2003)
This paper describes a methodology and its theoretical basis for synthesizing a class of programs which operate on recursive data structures. The methodology has appeared in an earlier paper by the...
Derivation of a Parallel String Matching Algorithm (2003)
We derive an ecient parallel algorithm to nd all occurrences of a pattern string in a subject string in O(log n) time, where n is the length of the subject string. The number of processors employed...
Synthesizing Programs over Recursive Data Structures 0 Abstract (2003)
Dedicated to the memory of
A theory of hints in model checking (2003)
Markus Kaltenbach, Jayadev Misra
Abstract. Model checking, in particular symbolic model checking, has proved to be extremely successful in establishing properties of finite state programs. In most cases, the proven properties are...
Derivation of a Parallel String Matching Algorithm (2003)
We derive an efficient parallel algorithm to find all occurrences of a pattern string in a subject string in O(log n) time, where n is the length of the subject string. The number of processors...
A reduction theorem for concurrent object-oriented programs (2003)
ABSTRACT A typical execution of a concurrent program is an interleaving of the threads of its components. It is well known that the net effect of a concurrent execution may be quite different from...
A Computability Theory for Distributed Systems. (2002)
The work proposed under this grant was to develop theories which will contribute to the design and analysis of distributed systems. The major emphasis of the proposed research was to study how and...
Orchestrating computations on the world-wide web (2002)
Young-ri Choi, Amit Garg, Siddhartha Rai, Jayadev Misra, Harrick Vin
Word processing software, email, and spreadsheet have revolutionized office activities. There are many other office tasks that are amenable to automation, such as: scheduling a visit by an external...
Computing the Spans in a sequence (2001)
The following problem has been treated as an example in a book by Goodrich and Tamassia [1, section 3.5]. Given is a sequence of integers, p0,..., pN−1. Henceforth, assume that p0 exceeds all other...
Generating-Functions of Interconnection Networks (2000)
Generating functions have long been used to analyze properties of sequences of numbers. In this note, we use generating functions to analyze a class of combinatorial objects, called interconnection...
On the impossibility of robust solutions for fair resource allocation (1999)
We show that the presence of even a single faulty process makes it impossible to design a strategy for fair allocation of a shared resource.
On the impossibility of robust solutions for fair resource allocation (1999)
We show that the presence of even a single faulty process makes it impossible to design a strategy for fair allocation of a shared resource.
Contents 4 Progress 5 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 4.2 Fairness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 4.2.1 Minimal Progress . . . ....
A Discipline of Multiprogramming (1999)
ion of the Scheduling Problem . . . . . . . . 70 4.3.2 Specification . . . . . . . . . . . . . . . . . . . . . . . . . 71 4.3.3 A Scheduling Strategy . . . . . . . . . . . . . . . . . . . . 71 4.3.4...
1 Problem Statement Phase Synchronization (1999)
Consider a set of asynchronous processes where each process executes a sequence of phases; a process begins its next phase only upon completion of its previous phase. What constitutes a phase is...
Browne, James C., Misra, Jayadev
The 1987 University of Texas Year of Programming was established early in 1986, in response to a proposal by Profs. Browne and Misra, with the following goals: 1) to advance the art and science of...
An Object Model for Multiprogramming (1998)
. We have developed a programming model that integrates concurrency with object-based programming. The model includes features for object definition and instantiation, and it supports concurrent...
Modular Multiprogramming ∗ (1998)
Object-based sequential programming has had a major impact on software engineering. However, object-based concurrent programming remains elusive as an effective programming tool. The class of...
Seuss: What the Doctor Ordered (1997)
Lorenzo Alvisi, Rajeev Joshi, Calvin Lin, Jayadev Misra
Reconciling the conflicting goals of simplicity and efficiency has traditionally been a major challenge in the development of concurrent programs. Seuss [16] is a methodology for concurrent...
Seuss: What the doctor ordered (1997)
Lorenzo Alvisi, Rajeev Joshi, Calvin Lin, Jayadev Misra
Reconciling the conflicting goals of simplicity and efficiency has traditionally been a major challenge in the development of concurrent programs. Seuss [16] is a methodology for concurrent...
A Discipline of Multiprogramming (1996)
this document is based on two observations: (1) the applications that will be implemented on networks of processors in the future will be significantly more ambitious than the current applications...
Approaches to Design of Circuits for Low-Power Computation (1995)
Priyadarsan Patra, Priyadarsan Patra, B. Sc, Donald S. Fussell, Jayadev Misra, Jacob A. Abraham
Copyright by
A Simple, Object-based View of Multiprogramming (1995)
Jayadev Misra, Dominique Mery, Beverly S
Abstract. Object-based sequential programming has had a major impact on software engineering. However, object-based concurrent programming remains elusive as an effective programming tool. The class...
A logic for concurrent programming: Safety (1995)
The UNITY-logic is a fragment of linear temporal logic. It was designed to specify safety and and progress properties of reactive systems. Experience gained in applying this logic in practice has led...
A logic for concurrent programming (1994)
Typically, program design involves constructing a program P that implements a given specification S; that is, the set P of executions of P is a subset of the set S of executions satisfying S. In many...
Powerlist: a structure for parallel recursion (1994)
Many data parallel algorithms-- Fast Fourier Transform, Batcher's sorting networks and prefix-sum-- exhibit recursive structure. We propose a data structure, powerlist, that permits succinct...
A logic for concurrent programming (1994)
Typically, program design involves constructing a program, P, that implements a given specification, S; that is, the set P of executions of P is a subset of the set S of executions satisfying S. In...
Contents 3 Safety Properties 3 3.1 Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 3.2 The meaning of co : : : : : : : : : : : : : : : : : : : : : : : 4 3.3 Special cases of co :...
A Logic for Concurrent Programming (1994)
The UNITY-logic, a fragment of linear temporal logic, was introduced in [5]. In this paper, we describe several recent modifications to this logic. In particular, the operator co replaces unless, for...
A Family of 2-process Mutual Exclusion Algorithms - Notes on UNITY: 13-90 (1994)
Introduction In Peterson [1981], Peterson suggested a mutual exclusion algorithm. The algorithm, though simple in structure, seems quite involved when a formal proof is attempted. We suggest how...
Powerlist: A Structure for Parallel Recursion (1994)
Many data parallel algorithms -- Fast Fourier Transform, Batcher's sorting networks and prefix-sum -- exhibit recursive structure. We propose a data structure, powerlist, that permits succinct...
A Discipline of Multiprogramming (1994)
. Research in multiprogramming has, traditionally, attempted to reconcile two apparently contradictory goals: (1) it should be possible to understand a module (e.g., a process or a data object) in...
Contents 4 Progress 3 4.1 Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 4.2 Fairness : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 4 4.2.1 Minimal Progress : : : :...
A logic for concurrent programming (1994)
In this paper, we suggest a method for proving the maximality of a program with respect to a given specification. Even though we prove facts about possible executions of programs there is no need to...
Powerlist: a structure for parallel recursion (1994)
Many data parallel algorithms – Fast Fourier Transform, Batcher’s sorting schemes and prefixsum – exhibit recursive structure. We propose a data structure, powerlist, that permits succinct...
The Academic Life of Louis E. Rosier (1993)
Nancy E. Lawler, Jayadev Misra, Vijaya Ramachandran
This document is a celebration of his life and his accomplishments.
Proof of a Real-Time Mutual-Exclusion Algorithm (1992)
Notes On, John Allen Carruth, Jayadev Misra
Michael Fischer[2] has proposed a mutual exclusion algorithm that ingeniously exploits real time. We prove this algorithm using the time-honored technique of establishing an appropriate invariant. 1...
Proof of a real-time mutual-exclusion algorithm. Notes on UNITY (1992)
John Allen Carruth, Jayadev Misra
Michael Fischer[2] has proposed a mutual exclusion algorithm that ingeniously exploits real time. We prove this algorithm using the time-honored technique of establishing an appropriate invariant. 1
Consider a set of asynchronous processes where each process executes a sequence of phases; a process begins its next phase only upon completion of its previous phase. What constitutes a phase is...
Specifying concurrent objects as communicating processes (1990)
An object and its associated operations may be specified in many ways. One way is to give an abstract representation of the object data structure (viz., representing a queue by a sequence) and the...
Equational reasoning about nondeterministic processes (1990)
A deterministic message-communicating process can be characterized by a "continuous" function f which describes the relationship between the inputs and the outputs of the process....
Preserving Progress Under Program Composition - Notes on UNITY: 17-90 (1990)
Introduction The question considered in this note is this: Under what condition is a progress property of program F preserved when F is composed with another program? For safety properties and...
this paper we show a very simple scheme for solving this problem.
Introduction Auxiliary variables are usually employed to record the history of a computation, and, thereby, allow reasoning over the entire computation history. They are typically defined by...
Progress--Safety--Safety (1990)
Now This work was partially supported by ONR Contracts N00014-87-K-0510 and N00014-86-0763, by a grant from the John Simon Guggenheim Foundation. s :r :q 7! false , PSP on (3) and (4) s ) q r ,...
More on Strengthening the Guard (1990)
Introduction It is well known that strengthening a guard of any statement in a program preserves all its safety properties though certain progress properties may be destroyed. (If all guards are...
Equational reasoning about nondeterministic processes (1990)
A deterministic message-communicating process can be characterized by a “continuous” function f which describes the relationship between the inputs and the outputs of the process. The operational...
A simple proof of a simple consensus algorithm (1989)
We present a proof of a simple consensus algorithm. The algorithm is known [1]; the proof style is new. It is difficult to reason about communicating processes when some of them may fail. We show...
A theorem about dynamic acyclic graphs. Notes on UNITY: 02--88, The Univ. of Texas at (1988)
Given is a finite directed acyclic graph. A top vertex has no incoming edge; a bottom vertex has no outgoing edge. The graph is changed according to the following operation: Pick an arbitrary vertex;...
General Conjunction and Disjunction Rules for unless," Notes on Unity 01-88 (1988)
The conjunction and disjunction rules for unless, as given in [1], are as follows. p unless q, p ′ unless q ′ p ∧ p ′ unless (p ∧ q ′ ) ∨ (p ′ ∧ q) ∨ (q ∧ q ′ ) {conjunction}...
1 The Problem A Theorem About Dynamic Acyclic Graphs Notes on UNITY: 02-88 (1988)
Given is a finite directed acyclic graph. A top vertex has no incoming edge; a bottom vertex has no outgoing edge. The graph is changed according to the following operation: Pick an arbitrary vertex;...
Distributed discrete-event simulation (1986)
Traditional discrete-event simulations employ an inherently sequential algorithm. In practice, simulations of large systems are limited by this sequentiality, because only a modest number of events...
An example of stepwise refinement of distributed programs: Quiescence detection (1986)
We propose a methodology for the development of concurrent programs and apply it to an important class of problems: quiescence detection. The methodology is based on a novel view of programs. A key...
Finding Repeated Elements (1982)
Two algorithms are presented for finding the values that occur more than $n \div k$ times in array b[O:n-1]. The second algorithm requires time $O(n \log(k))$ and extra space $O(k)$. We prove that...
Finding Repeated Elements (1982)
Two algorithms are presented for finding the values that occur more than $n \div k$ times in array b[O:n-1]. The second algorithm requires time $O(n \log(k))$ and extra space $O(k)$. We prove that...
Termination detection of diffusing computations in communicating sequential processes (1982)
In this paper it is shown how the Dijkstra-Scholten scheme for termination detection in a diffusing computation can be adapted to detect termination or deadlock in a network of communicating...
A Linear Sieve Algorithm for Finding Prime Numbers (1977)
NO ABSTRACT SUPPLIED
A Linear Sieve Algorithm for Finding Prime Numbers (1977)
NO ABSTRACT SUPPLIED