We first define a new fixpoint semantics which correctly models finite failure and is and-compositional. We then consider the problem of verification w.r.t. finite failure and we show how Ferrand's approach, using both a least fixpoint and greatest fixpoint semantics, can be adapted to finite failure. The verification method is not effective. There fore, we consider an approximation from above and an approximation from below of our semantics, which give two different finite approximations. These approximations are used for effective program verification.
On the verification of finite failure
GORI, ROBERTA;
1999-01-01
Abstract
We first define a new fixpoint semantics which correctly models finite failure and is and-compositional. We then consider the problem of verification w.r.t. finite failure and we show how Ferrand's approach, using both a least fixpoint and greatest fixpoint semantics, can be adapted to finite failure. The verification method is not effective. There fore, we consider an approximation from above and an approximation from below of our semantics, which give two different finite approximations. These approximations are used for effective program verification.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
