This paper presents two formal models for parallel computation: an abstract conceptual model and a parallel-program model. The conceptual model does not distinguish between control and data states, while the parallel-program model allows for an infinite set of control states through the use of arbitrarily many instruction pointers. An induction principle is introduced that treats control and data states on equal footing, enabling the expression of correctness conditions without explicitly enumerating all possible control states. Examples demonstrate the use of this principle to prove mutual exclusion. It is shown that assertions-oriented proof methods are special cases of this induction principle. A special case, parallel place assertions, is found to be incomplete. A formalization of deadlock is presented, and a concept of "norm" is introduced to extend Floyd's technique for proving termination. The paper also discusses an extension of the program model that allows each process to have its own local variables and permits shared global variables. Correctness of certain implementations is discussed. The paper relates this work to previous work on the satisfiability of logical formulas. Key concepts include parallel programs, correctness, verification, assertions, deadlock, mutual exclusion, and Petri nets. The paper discusses the use of induction principles for proving invariants in parallel programs, including the use of place variables and the concept of a home state for proving deadlock avoidance. The paper also discusses extensions to the model, including the use of local variables and the ability to handle an arbitrary number of dynamically created processes.This paper presents two formal models for parallel computation: an abstract conceptual model and a parallel-program model. The conceptual model does not distinguish between control and data states, while the parallel-program model allows for an infinite set of control states through the use of arbitrarily many instruction pointers. An induction principle is introduced that treats control and data states on equal footing, enabling the expression of correctness conditions without explicitly enumerating all possible control states. Examples demonstrate the use of this principle to prove mutual exclusion. It is shown that assertions-oriented proof methods are special cases of this induction principle. A special case, parallel place assertions, is found to be incomplete. A formalization of deadlock is presented, and a concept of "norm" is introduced to extend Floyd's technique for proving termination. The paper also discusses an extension of the program model that allows each process to have its own local variables and permits shared global variables. Correctness of certain implementations is discussed. The paper relates this work to previous work on the satisfiability of logical formulas. Key concepts include parallel programs, correctness, verification, assertions, deadlock, mutual exclusion, and Petri nets. The paper discusses the use of induction principles for proving invariants in parallel programs, including the use of place variables and the concept of a home state for proving deadlock avoidance. The paper also discusses extensions to the model, including the use of local variables and the ability to handle an arbitrary number of dynamically created processes.