Observatorio de I+D+i UPM

Memorias de investigación
Dynamic Checking of Assertions for Higher-order Predicates
Áreas de investigación
  • Ciencias de la computación y tecnología informática
In order to improve the quality of software products, various techniques can be used within the software development life cycle. A topic that has received significant interest in recent years has been the technique of program validation via static and/or dynamic checking of user.provider assertions. Such assertions can be considered a (partial) program specification in the form of annotations in the source code. Together with analysis tools, they allow detecting incorrect program behaviors, studying resource consumption, and reasoning about various other properties of the program. This approach has proven quite useful in the domain of Logic Programming, where on of the richest designs and implementations of a combination of assertion language and analysis tools can be found in the Ciao System. On of the features of this system is the support of higher-order. Higher-order logic programming extends the expressiveness of conventional first-order logic programming, both syntactical and semantically. While quite useful in practice, higher-order also poses challenges in analysis and verification. This thesis contributes to solving the problem of analysis, checking, and specification of higer-order logic programs. It proposes a higher-order extension of the traditional Ciao assertion language and of the CiaoPPP run-time verification mechanisms. We explore different alternatives for checking, highlighting the benefits and drawbacks of each of them. We also present a prototype implementation, based on the current language extension mechanism of Ciao, and some early experimental results. We expect this first approach to the problem to serve as a basis for the design and development of more sophisticated checking and analysis tools of high-order programs.
Tipo de Tesis
Sobresaliente cum laude
Esta actividad pertenece a memorias de investigación
  • Director: Manuel de Hermenegildo Salinas (UPM)
  • Director: Jose Francisco Morales Caballero (UPM)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: Computación lógica, Lenguajes, Implementación y Paralelismo (CLIP)
  • Departamento: Inteligencia Artificial
S2i 2023 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)