Report
Model checking liveness properties of higher-order functional programs
- Abstract:
-
Recent advances in the model checking of recursion schemes have opened the prospect of a model checking approach to the verification of higher-order functional programs. We formulate the Resource Usage Verification Problem in a general (liveness) setting, where good behaviours are specified by alternating parity (word) automata; and we give a sound and complete decision procedure by reduction to the problem of model checking higher-order recursion schemes (HORS) against alternating parit...
Expand abstract
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Authors
Bibliographic Details
- Publication date:
- 2011-06-07
Item Description
- Pubs id:
-
pubs:911547
- UUID:
-
uuid:bf35bab8-b395-4f85-93bd-57ca0328a1d3
- Local pid:
- cs:6255
- Deposit date:
- 2015-03-31
Terms of use
- Copyright date:
- 2011
- Notes:
- This is an author version of the report.
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record