Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue
 
home
browse
current
etoc
authors
subinfo
subscribers
samples

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 2, April 2002: pp. 255-269

[mu]-Calculus with Explicit Points and Approximations

Mads Dam1 and Dilian Gurov2

1Department of Microelectronics and Information Technology (IMIT), Royal Institute of Technology (KTH), Electrum 229, SE-164 40 Kista, Sweden. E-mail: mfd@it.kth.se
2Swedish Institute of Computer Science (SICS), Box 1263, SE-164 29 Kista, Sweden. E-mail: dilian@sics.se

We present a Gentzen-style sequent calculus for program verification which accommodates both model checking-like verification based on global state space exploration, and compositional reasoning. To handle the complexities arising from the presence of fixed-point formulas, programs with dynamically evolving architecture, and cut rules we use transition assertions, and introduce fixed-point approximants explicitly into the assertion language. We address, in a game-based manner, the semantical basis of this approach, as it applies to the entailment subproblem. Soundness and completeness results are obtained, and examples are shown illustrating some of the concepts.

Keywords: [mu]-calculus; sequent calculus; program verification; compositionality

Table of Contents   Full-Text PDF (174 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement