Model checking liveness properties of higher-order functional programs

摘要: Recent advances in the model checking of recursion schemes have opened prospect a approach to verification higher-order functional programs. We formulate Resource Usage Verification Problem general (liveness) setting, where good behaviours are specified by alternating parity (word) automata; and we give sound complete decision procedure reduction problem (HORS) against tree automata. Extending Kobayashi's type-inference approach, present an efficient algorithm for deciding restriction which properties expressed weak automata (and hence all CTL formulas). constructed checker, THORS, that implements our number optimisations. Despite hugely challenging worst-case time complexity, THORS performs remarkably well on small examples, even up order 5. To knowledge, this is first checker HORS allows specification with non-trivial acceptance condition, including properties.