Correctness and Bounded Correctness [Keynote Address]

Summary form only given, as follows. The complete presentation was not made available for publication as part of the conference proceedings. Correctness is an important issue in computer science and software engineering. For concurrent systems, the definition of correctness is usually based on properties of infinite execution paths. Bounded correctness is a kind of correctness defined on finite paths, and provides a different view on the issue of correctness. This talk focuses on the concept of bounded correctness and the relation between correctness and bounded correctness. For the purpose of verification, the definition of correctness based on infinite paths is not directly applicable as a means for verification, and the approaches for such a purpose include those based on the analysis of strongly connected components and on the computation of fixed points. On the other hand, correctness may be verified in terms of bounded correctness by an approach derived from the definition of bounded correctness. The complementariness of these verification approaches is explained.