Program transformation for development, verification, and synthesis of programs

Issue title: Evolutionary Computation – A Journey in Computational Logic in Italy – Dedicated to Prof. Alberto Martelli

Article type: Research Article

Authors: Fioravanti, Fabio | Pettorossi, Alberto | Proietti, Maurizio | Senni, Valerio

Affiliations: Department of Sciences, University of ‘G. D'Annunzio’, Viale Pindaro 42, Pescara, Italy | Department of Informatics, Systems, and Production, University of Rome ‘Tor Vergata’, Via del Politecnico 1, Rome, Italy | CNR-IASI, Viale Manzoni 30, Rome, Italy

Note: [] Corresponding author. CNR-IASI, Viale Manzoni 30, 00185 Rome, Italy. E-mails: maurizio.proietti@iasi.cnr.it (M. Proietti); pettorossi@disp.uniroma2.it (A. Pettorossi); senni@disp.uniroma2.it (V. Senni); fioravanti@sci.unich.it (F. Fioravanti).

Abstract: This paper briefly describes the use of the program transformation methodology for the development of correct and efficient programs. In particular, we will refer to the case of constraint logic programs and, through some examples, we will show how by program transformation, one can improve, synthesize, and verify programs.

Keywords: Constraint logic programming, model checking, program development, program synthesis, unfold/fold program transformation, software verification

DOI: 10.3233/IA-2011-0014

Journal: Intelligenza Artificiale, vol. 5, no. 1, pp. 119-125, 2011