skip to main content
Idioma:

Model Checking Higher-Order Programs

KOBAYASHI, Naoki

Journal of the ACM, 2013-06, Vol.60 (3), p.1-62 [Periódico revisado por pares]

New York, NY: Association for Computing Machinery

Texto completo disponível

Citações Citado por
  • Título:
    Model Checking Higher-Order Programs
  • Autor: KOBAYASHI, Naoki
  • Assuntos: Algorithmics. Computability. Computer arithmetics ; Algorithms ; Applied sciences ; Computer programming ; Computer science; control theory; systems ; Computer systems performance. Reliability ; Exact sciences and technology ; Mathematical functions ; Mathematical models ; Programming languages ; Prototypes ; Software ; Studies ; Theoretical computing
  • É parte de: Journal of the ACM, 2013-06, Vol.60 (3), p.1-62
  • Notas: ObjectType-Article-2
    SourceType-Scholarly Journals-1
    ObjectType-Feature-1
    content type line 23
  • Descrição: We propose a novel verification method for higher-order functional programs based on higher-order model checking, or more precisely, model checking of higher-order recursion schemes (recursion schemes, for short). The most distinguishing feature of our verification method for higher-order programs is that it is sound, complete, and automatic for the simply typed λ-calculus with recursion and finite base types, and for various program verification problems such as reachability, flow analysis, and resource usage verification. We first show that a variety of program verification problems can be reduced to model checking problems for recursion schemes, by transforming a program into a recursion scheme that generates a tree representing all the interesting possible event sequences of the program. We then develop a new type-based model-checking algorithm for recursion schemes and implement a prototype recursion scheme model checker. To our knowledge, this is the first implementation of a recursion scheme model checker. Experiments show that our model checker is reasonably fast, despite the worst-case time complexity of recursion scheme model checking being hyperexponential in general. Altogether, the results provide a new, promising approach to verification of higher-order functional programs.
  • Editor: New York, NY: Association for Computing Machinery
  • Idioma: Inglês
Links
Voltar para lista de resultados

  • Realização: ABCD-USP USP   Logos de Redes Sociais: Freepik

Buscando em bases de dados remotas. Favor aguardar.