ABSTRACT
--------

The design of concurrent programs that run reliably and efficiently on 
networks of interconnected computers will remain an important 
challenge for the foreseeable future, as the size and complexity of 
such systems will continue to grow.  Verification techniques based on 
appropriate design formalism and complemented by mechanical support 
will play an important role for asserting the correctness and quality 
of these concurrent systems.

In this dissertation we focus on providing suitable automated 
assistance to the design and verification of concurrent systems by 
developing a model checker for finite state programs and propositional 
UNITY logic.  Combining the verification technique of model checking 
with the temporal logic of UNITY was motivated by two goals, namely to 
exploit the simplicity and structure of UNITY logic as to provide 
efficient checking algorithms for a mostly automated verification, and 
to allow the user to interactively supply design knowledge in order to 
improve the system performance.

These goals have been met in three ways: (i) we have derived a model 
checking procedure for safety and basic progress properties that is 
based on the proof rules of UNITY logic, increases the efficiency of 
verification by making it possible to replace fixpoint computations by 
simple verification checks, and, moreover, takes advantage of 
state-based design knowledge in the form of invariants; (ii) we have 
developed and formally investigated a new theory of generalized 
progress, in which action-based hints can be provided to indicate how 
progress is achieved and which can be used to improve the efficiency 
of checking and reasoning about arbitrary progress properties; (iii) 
finally, we have implemented the resulting model checking procedures 
as part of the UNITY Verifier System and have used our implementation 
to demonstrate the improved verification performance with several 
examples.


KEYWORDS
--------

concurrent systems, verification, model checking, UNITY, design
knowledge, progress properties, regular expressions, predicate
transformers, games