Case Study on Verification of Logic Programs

Case Study on Verification of Logic Programs


The following case studies have been developed as projects in the PhD course Verification of Logic Programs held by K. R. Apt and D. Pedreschi at Dept. of Computer Science, University of Pisa in 1996. The case studies have been taken from the Prolog programming competition held at ILPS'94, Ithaca, New York. The proof method adopted for studing properties of the case study programs is substantially the one proposed by D. Pedreschi and S. Ruggieri, Verification of Logic Programs, Journal of Logic Programming, 39 (1-3):125-176, April 1999.

ILPS'94 Competition Documentation

Spiral
by C. Renso and S. Ruggieri

Domino Solitaire
by S. Contiero and A. Giani

Crosswords
by R. Bruni and M. Pistore

Path (in italian)
by M. Comini and E. Zaffanella

Loops (not available)
by R. Bagnara and D. Pasetto



Salvatore Ruggieri