swMATH ID: 14146
Software Authors: Lester, M.M., Neatherway, R.P., Ong, C.-H.L., Ramsay, S.J.
Description: THORS Hammer: Higher-order recursion schemes are a higher-order analogue of Boolean Programs; they form a natural class of abstractions for functional programs. We present a new, efficient algorithm for checking CTL properties of the trees generated by higher-order recursion schemes, which is an extension of Kobayashi’s intersection type-based model checking technique. We show that an implementation of this algorithm, THORS, performs well on a number of small examples and we demonstrate how it can be used to verify liveness properties of OCaml programs. Example properties include statements such as ”all opened sockets are eventually closed” and ”the lock is held until the file is closed”.
Homepage: http://mjolnir.cs.ox.ac.uk/thors/
Related Software: TRecS; EigenCFA
Cited in: 1 Publication

Cited in 0 Serials

Citations by Year