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 |