Volume 6: January - December 1996

Issue 3: June 1996


Verification of temporal properties

  • Verification of temporal properties
  • L. Fix1 and O. Grumberg2 1Upson Hall, Computer Science Dept., Cornell University, Ithaca, NY 14850, USA. Email: fix@cs.cornell.edu and 2Computer Science Dept., Technion, Haifa 32000, Israel. Email: orna@cs.technion.ac.il


    The paper presents a relatively complete deductive system for proving branching time temporal properties of reactive programs. No deductive system for verifying branching time temporal porperties has been presented before. Our deductive system enjoys the following advantages. First, given a well-formed specification there is no need to translate it into a normal-form specification since the system can handle any well-formed specification. Second, given a specification to be verified, the proof rule to be applied is easily determined according to the top level operator of the specification. Third, the system reduces temporal verification to assertional reasoning rather than to temporal reasoning.

    Keywords: program verification, temporal logic, branching-time, CTL, deductive system.

    Pages: 343 - 361

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    Click here to register with OUP.

    This page is maintained by OUP admin

    Last updated 23 Jul 96

    Part of the OUP Journals World Wide Web service.

    Copyright Oxford University Press, 1996