Modalities in analysis and verification
Mads Dam · ACM Computing Surveys · 1996
Concurrent systems with program code-passing capabilities pose severe challenges to current technologies for program verification and analysis.We suggest higherorder modal and temporal logic as a tool for behavioral encapsulation of such systems.The difficulty is to provide usable and generally applicable tools for showing that a system satisfies the properties required of it.Compositional techniques have this potentiality and recent work appears to demonstrate that they may be more applicable than previously thought.