Memorias de investigación
Conferencias:
Analysis and Verification ?of and with? CLP. Keynote speech at COST action ?rich model toolkit? meeting, Malta, 2013
Año:2013

Áreas de investigación
  • Ciencias de la computación y tecnología informática

Datos
Descripción
The talk started with an overview of techniques for abstract interpretation-based program analysis and verification of constraint logic programs (CLP), with emphasis on the on top-down fixpoint algorithms used in the Ciao system (note that bottom-up techniques will be covered in John Gallagher's talk). We will demonstrate the Ciao system analysis and verification-based program development environment, built around these techniques and capable of verifying shapes, modes, determinacy, non-failure, numerical properties, etc. as well as resources such as bandwidth, time, memory, or, more recently, energy. We will then address how, by using CLP as an intermediate representation, the approach (and the Ciao system itself) also supports the verification of similar properties in programs in other programming paradigms, including Java source or bytecode, and assembly code produced from C sources. Finally, we present how the same fixpoint techniques are applied in the execution of Tabled LP programs (such as in the XSB system) and Tabled CLP programs (such as in the TCLP package of the Ciao system), which can be an interesting component for program analyzers for other programming paradigms.
Internacional
Si
ISSN o ISBN
Entidad relacionada
Rich Model Tool Kit COST Action
Nacionalidad Entidad
Sin nacionalidad
Lugar del congreso
Malta

Esta actividad pertenece a memorias de investigación

Participantes

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