Title :
Higher-Order Model Checking: From Theory to Practice
Author :
Kobayashi, Naoki
Author_Institution :
Tohoku Univ., Sendai, Japan
Abstract :
The model checking of higher-order recursion schemes (higher-order model checking for short) has been actively studied in the last decade, and has seen significant progress in both theory and practice. From a practical perspective, higher-order model checking provides a foundation for software model checkers for functional programming languages such as ML and Haskell. This short article aims to provide an overview of the recent progress in higher-order model checking and discuss future directions.
Keywords :
ML language; formal verification; functional programming; Haskell; ML; functional programming languages; higher-order model checking; higher-order recursion schemes; software model checkers; Analytical models; Automata; Complexity theory; Computational modeling; Computer science; Safety; Software;
Conference_Titel :
Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on
Conference_Location :
Toronto, ON
Print_ISBN :
978-1-4577-0451-2
Electronic_ISBN :
1043-6871
DOI :
10.1109/LICS.2011.15
