From model checking to a temporal proof for partial models: preliminary example

A. Bernasconi, C. Menghi, P. Spoletini +2

This paper describes in detail the example introduced in the preliminary evaluation of THRIVE. Specifically, it evaluates THRIVE over an abstraction of the ground model proposed fo…