Using partial evaluation to enable verification of concurrent software
Matthew B. Dwyer, John Hatcliff, Muhammad Nanda · ACM Computing Surveys · 1998
Partial evaluation and finite-state verification techniques have been developed, for the most part, in separate communities. Despite this there is significant overlap at both conceptual and technical levels involving specific program analysis and transformation methods. In this paper, we describe some of the connections between these two areas of research and how, by exploiting these connections, we can increase the impact of these techniques on software practice. 1 Introduction Modern computing applications increasingly require software systems that are extremely reliable and concurrent or distributed. Unfortunately, current software validation techniques are unable to provide high levels of assurance of correctness for these systems due to system size and complexity as well as the fundamental difficulties of reasoning about concurrency. Finite-state verification (FSV) techniques (originally developed for hardware verification) are emerging as a promising technology for assuring hig...