Búsqueda avanzada

A Tool for Black-Box Testing in a Multilanguage Verification Platform (Trabajo en progreso)

In the context of the multilanguage verification platform CAVI-ART, we have defined an Intermediate Representation (IR) to which all the source languages are translated. This IR contains both the code and the assertions given by the programmer. Its primary purpose was automatically generating and proving, in a source language independent way, the verification conditions ensuring the program correctness. The logical formulas are sent by the platform to an SMT solver which checks their validity.

In this paper we present a new use of the IR: we transform it into an executable language (that it turns out to be Haskell) and also transform the assertions into executable (Haskell) code. Thanks to that, tests can be run on the transformed program, and bugs can be detected either in the specification assertions or in the code. Moreover, we use the assertions to generate black-box test-cases from them, and also as test oracles. In this way, given the IR of a program, all the process —namely, test-case generation, test running, and test correctness checking— is completely automatic. So, thousands of tests can be run with little or none effort. The only burden for the programmer is providing the precondition and the postcondition of the code under test, which anyway should have been provided in advance, since the primary goal was to verify the program.

We discuss the problems we have encountered while implementing this idea, and how we have solved them. In particular, we report on the use of Haskell resources such as GADTs, efficient data structures, and specialized libraries.

Termination Analysis in a Multi-language Verification Platform (Trabajo en progreso)

One aim of the verification platform CAVI-ART is to provide as much assistance as possible to programmers in order to alleviate their verification effort. One of these aids is automatically proving termination of programs, whenever this is possible. Since CAVI-ART is a multi-language platform, the analysis is performed at the level of the platform Intermediate Representation language (IR), to which all source languages are first translated.

We have selected one of the the most successful termination tools, called RANK, and transform our IR-programs to an appropriate input for RANK. There is a fundamental mismatch between the functional, stateless, recursive flavour of our IR, and the automaton-based input of RANK, which is a tool developed for imperative, mutable-state programs. In this paper we show how we have circumvented this problem, and present an algorithm transforming the IR to an automaton. We give some examples of recursive programs that we have successfully proved terminating.