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.
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