Rodin User’s Handbook v.2.8: The Proof Obligation Generator (2005)

Rodin Handbook

This work is sponsored by the Deploy Project

This work is sponsored by the ADVANCE Project

Creative Commons License

This work is licensed under a Creative Commons Attribution 3.0 Unported License

The Proof Obligation Generator (2005)

Rodin User’s Handbook v.2.8

1.2.6 The Proof Obligation Generator (2005)

In this technical report (ETH Zürich) Stefan Hallerstede describes which proof obligations (see Section 3.2.7) are generated for a model and gives a justification why these are correct.

Rodin User’s Handbook v.2.8 : Introduction : Further Reading : The Proof Obligation Generator (2005)