LA TRASFORMAZIONE DEI PROGRAMMI PER LO SVILUPPO, LA VERIFICA E LA SINTESI DEL SOFTWARE PROGRAM TRANSFORMATION FOR DEVELOPMENT, VERIFICATION, AND SYNTHESIS OF SOFTWARE

-

In questo articolo presentiamo brevemente la metodologia di trasformazione dei programmi per lo sviluppo di software corretto ed efficiente. Ci riferiremo, in particolare, al caso della trasformazione e dello sviluppo dei programmi logici con vincoli.

In this paper we briefly describe the use of the program transformation methodology for the development of correct and efficient programs. We will consider, in particular, the case of the transformation and the development of constraint logic programs. 1

Introduction

The program transformation methodology has been introduced in the case of functional programs by Burstall and Darlington [ 3 ] and then it has been adapted to logic programs by Hogger [ 11 ] and Tamaki and Sato [ 26 ]. The main idea of this methodology is to transform, maybe in several steps and by applying different transformation rules, the given initial program into a final program with the aim of improving its efficiency and preserving its correctness. If the initial program is a non-executable specification of an algorithm, while the final program is executable, then program transformation is equivalent to program synthesis. Thus, program transformation can be viewed as a technique both: (i) for program improvement and advanced compilation, and (ii) for program synthesis and program development.

In recent years program transformation has also been used as a technique for program verification. It has been shown, in fact, that via program transformation one can perform model checking and, in general, one can prove properties of infinite state systems that cannot be analyzed by using standard model checking techniques.

In what follows we will illustrate the three uses of program transformation we have mentioned above, namely (i) program improvement, (ii) program synthesis, and (iii) program verification. In particular, we will consider the case of algorithms and specifications written as constraint logic programs [ 12 ] and we will focus our attention on the following transformation rules [ 1, 6, 8, 9, 25, 26 ]: definition, unfolding, folding, goal replacement, and clause splitting which will be applied according to some specific strategies. This approach to program transformation is, thus, called the rules + strategies approach. 2

Program improvement

Programs are often written in a parametric form so that they can be reused in different contexts, and when a parametric program is reused, one may want to transform it for taking advantage of the new context of use. This transformation, called program specialization [ 10, 13, 16 ], usually allows a great efficiency improvement. Let us present an example of this transformation by deriving a deterministic, specialized pattern matcher from a given nondeterministic, parametric pattern matcher and a specific pattern. In this example the matching relation on strings of numbers is the relation le m(P, S) which holds between a pattern P = [p1, . . . , pn]¯and a string S iff in S there exists a substring Q = [q1, . . . , qn] such that for i = 1, . . . , n, pi ≤ qi. (This example can be generalized by considering any relation which can be expressed via a constraint logic program.)

The following constraint logic program can be taken as the specification of our general pattern matching problem: 1. le m(P, S) ← ap(B, C, S)∧ap(A, Q, B)∧le(P, Q) ¯ 2. ap([ ], Ys , Ys ) ← 3. ap([X|Xs ], Ys , [X|Zs ]) ← ap(Xs , Ys , Zs ) 4. le([ ], [ ]) ← 5. le([X|Xs ], [Y |Ys ]) ← X ≤ Y ∧le(Xs, Y s) where ap denotes list concatenation. Suppose that we want to use this general program in the case of the pattern P = [ 1,0,2 ]. We start off our transformation by introducing the following clause by applying the so-called definition rule: 6. le¯ms (S) ← le m([ 1,0,2 ], S)

¯ Clauses 1–6 constitute the initial program from which we begin our program transformation process by applying the transformation rules according to the so-called Determinization Strategy [ 8 ]. This strategy, which we will not present here, allows a fully automatic derivation of the deterministic, efficient pattern matcher. We unfold clause 6 w.r.t. the atom le m([ 1,0,2 ], S), that is, we replace the atom le m([ 1,0,2 ], S)¯ which is an instance of the head of clause 1,¯ by the corresponding instance of the body of clause 1. We get: 7. le¯ms (S) ← ap(B, C, S)∧ap(A, Q, B)∧le([ 1,0,2 ], Q) In order to fold clause 7, we introduce the following definition: 8. new 1(S) ← ap(B, C, S)∧ap(A, Q, B)∧le([ 1,0,2 ], Q) and then we fold clause 7, that is, we replace (the instance of) the body of a clause 8 which occurs in the body of clause 7 by (the corresponding instance of) the head of clause 8. We get: 9. le¯ms (S) ← new 1(S) Then we unfold clause 8 w.r.t. the atoms ap and le and we get: 10. new 1([X|Xs ]) ← 1 ≤ X ∧ap(Q, C, Xs )∧le([ 0,2 ], Q) 11. new 1([X|Xs ]) ← ap(B, C, Xs )∧ap(A, Q, B)∧ le([ 1,0,2 ], Q) Then we apply the clause splitting rule to clause 11, by separating the cases where 1 ≤ X and 1 > X . We get: 12. new 1([X|Xs ]) ←1 ≤ X ∧ap(B, C, Xs )∧ap(A, Q, B)∧ le([ 1,0,2 ], Q) 13. new 1([X|Xs ]) ←1 > X ∧ap(B, C, Xs )∧ap(A, Q, B)∧ le([ 1,0,2 ], Q) In order to fold clauses 10 and 12 we introduce the following two clauses defining the predicate new 2: 14. new 2(Xs ) ← ap(Q, C, Xs )∧le([ 0, 2 ], Q) 15. new 2(Xs ) ← ap(B,C,Xs )∧ap(A,Q,B)∧le([ 1,0,2 ],Q) Then we fold clauses 10 and 12 by using the two clauses 14 and 15 and we also fold clause 13 by using clause 8. We get the following clauses which define new 1: 16. new 1([X|Xs ]) ← 1 ≤ X∧new 2(Xs ) 17. new 1([X|Xs ]) ← 1 > X ∧new 1(Xs ) They are mutually exclusive because of the constraints 1 ≤ X and 1 > X . Now the program transformation continues in a similar way as above: we introduce the new predicates new 3 through new 6, we derive their defining clauses, and eventually, we get the following specialized, deterministic program: 9. le ms (S) ← new 1(S)

¯ 16. new 1([X|Xs ]) ← 1 ≤ X ∧new 2(Xs ) 17. new 1([X|Xs ]) ← 1 > X ∧new 1(Xs ) 18. new 2([X|Xs ]) ← 1 ≤ X ∧new 3(Xs ) 19. new 2([X|Xs ]) ← 0 ≤ X ∧1 > X ∧new 4(Xs ) 20. new 2([X|Xs ]) ← 0 > X ∧new 1(Xs ) 21. new 3([X|Xs ]) ← 2 ≤ X ∧new 5(Xs ) 22. new 3([X|Xs ]) ← 1 ≤ X ∧2 > X ∧new 3(Xs ) 23. new 3([X|Xs ]) ← 0 ≤ X ∧1 > X ∧new 4(Xs ) 24. new 3([X|Xs ]) ← 0 > X ∧new 1(Xs ) 25. new 4([X|Xs ]) ← 2 ≤ X ∧new 6(Xs ) 26. new 4([X|Xs ]) ← 1 ≤ X ∧2 > X ∧new 2(Xs ) 27. new 4([X|Xs ]) ← 1 > X ∧new 1(Xs ) 28. new 5([X|Xs ]) ← 29. new 6([X|Xs ]) ← This final program is deterministic in the sense that at most one clause can be applied during the evaluation of every ground goal. As in the case of the Knuth-Morris-Pratt matcher, the efficiency of this final program is very high because it behaves like a deterministic finite automaton. 3

Program Synthesis

Program synthesis is a technique for deriving programs from formal, possibly non-executable, specifications (see, for instance, [ 11, 24 ] for the derivation of logic programs from first-order logic specifications). In this section we present an example of use of the program transformation technique for performing program synthesis and deriving a constraint logic program from a first-order formula.

The example we will present is the N -queens example, which has been often considered in the literature for introducing programming techniques such as recursion and backtracking. The N -queens problem can be described as follows. We are required to place N (≥ 0) queens on an N×N chess board, so that no two queens attack each other, that is, they do not lie on the same row, column, or diagonal. By using the fact that no two queens should lie on the same row, we represent the position of the N queens on the N × N chess board as a permutation L = [i1, . . . , iN ] of the list [1, . . . , N ] such that ik is the column of the queen on row k.

A specification of the solution L for the N -queens problem is given by the following first-order formula ϕ(N, L): nat (N ) ∧ nat −list (L) ∧ length(L, N ) ∧ ∀X (member (X, L) → in(X, 1, N ))∧ ∀A,B,K,M ((1 ≤ K ∧ K ≤ M ∧occurs (A, K, L) ∧occurs (B,M,L)) → (A 6= B ∧ A−B 6= M −K ∧ B −A 6= M −K)) where the various predicates which occur in ϕ(N, L) are defined by the following constraint logic program P : nat (0) ← nat (N ) ← N = M +1 ∧ M ≥ 0 ∧ nat (M ) nat −list ([ ]) ← nat −list ([H |T ]) ← nat (H ) ∧ nat −list (T ) length([ ], 0) ← length([H |T ], N ) ← N = M +1 ∧ M ≥ 0 ∧ length(T , M ) member (X, [H |T ]) ← X = H member (X, [H |T ]) ← member (X, T ) in(X, M, N ) ← X = N ∧ M ≤ N in(X, M, N ) ← N = K +1 ∧ M ≤ K ∧ in(X, M, K) occurs (X, I, [H |T ]) ← I = 1 ∧ X = H occurs (X, I +1, [H |T ]) ← I ≥ 1 ∧ occurs (X, I, T ) Now, we would like to synthesize a constraint logic program R which computes a predicate queens (N, L) such that the following Property π holds: (π)

M (R) |= queens (N, L) iff M (P ) |= ϕ(N, L) where by M (R) and M (P ) we denote the perfect model of the program R and P , respectively. By applying the technique presented in [ 9 ], we start off from the formula queens (N, L) ← ϕ(N, L). From that formula by applying a variant of the Lloyd-Topor transformation [ 17 ], we derive this stratified program F : queens (N, L) ← nat (N ) ∧ nat −list (L) ∧ length(L, N )∧ ¬aux 1(L, N ) ∧ ¬aux 2(L) aux 1(L, N ) ← member (X, L) ∧ ¬in(X, 1, N ) aux 2(L) ← 1 ≤ K ∧ K ≤ M ∧ ¬(A 6= B ∧ A−B 6= M−K ∧ B−A 6= M−K)∧ occurs (A, K, L) ∧ occurs (B, M, L) It can be shown that this variant of the Lloyd-Topor transformation preserves the perfect model semantics and, thus, we have that:

M (P ∪ F ) |= queens (N, L) iff M (P ) |= ϕ(N, L). The derived program P ∪ F is not very satisfactory from a computational point of view, when using SLDNF resolution with the left-to-right selection rule. Indeed, for a query of the form queens (n, L), where n is a nonnegative integer and L is a variable, program P ∪ F works by first generating a value l for L and then testing whether or not length(l, n) ∧ ¬aux 1(l, n) ∧ ¬aux 2(l) holds. This generate-and-test behavior is very inefficient and it may also lead to nontermination. Thus, the process of program synthesis proceeds by applying the definition, unfolding, folding, and goal replacement transformation rules (see [ 9 ] for details), with the objective of deriving a more efficient, terminating program. We derive the following definite logic program R: queens (N, L) ← new 2(N, L, 0) new 2(N, [ ], K) ← N = K new 2(N, [H |T ], K) ← N ≥ K +1 ∧ new 2(N, T , K +1)∧ new 3(H, T , N, 0) new 3(A, [ ], N, M ) ← in(A, 1, N ) ∧ nat (A) new 3(A, [B|T ], N, M ) ← A 6= B ∧ A−B 6= M +1 ∧ B −A 6= M +1 ∧ nat (B) ∧ new 3(A, T , N, M +1) together with the clauses defining the predicates in and nat .

Since the transformation rules preserve the perfect model semantics, we have that M (R) |= queens (N, L) iff M (P ∪ F ) |= queens (N, L) and, thus, Property (π) holds. Moreover, it can be shown that R terminates for all queries of the form queens (n, L) and it computes a solution for the N -queens problem in a clever way: each time a queen is placed on the board, program R tests whether or not it attacks every other queen already placed on the board. 4

Program Verification

The proof of program properties is often needed during program development for checking the correctness of software components w.r.t. their specifications. In this section we see the use of program transformation for proving program properties specified either by first-order formulas or by temporal logic formulas.

Proofs performed by using program transformation have strong relationships with proofs by mathematical induction (see [ 2 ] for a survey on inductive proofs). In particular, the unfolding rule can be used for decomposing a formula of the form ϕ(f (X)), where f (X) is a complex term, into a combination of n formulas of the forms ϕ1(X), . . . , ϕn(X), and the folding rule can be used for applying inductive hypotheses.

It has been shown that the unfold/fold transformations introduced in [ 3, 26 ] can be used for proving several kinds of program properties, such as equivalences of functions defined by recursive equation programs [ 14 ], equivalences of predicates defined by logic programs [ 20 ], first-order properties of predicates defined by constraint logic programs [ 21 ], and temporal properties of concurrent systems [ 7, 23 ]. 4.1

The unfold/fold proof method

By using a simple example taken from [ 21 ], we illustrate a method based on program transformation, called unfold/fold proof method, for proving first-order properties of constraint logic programs. Consider the following constraint logic program Member which defines the membership relation for lists: member (X, [Y |L]) ← X = Y member (X, [Y |L]) ← member (X, L) Suppose we want to show that every finite list of numbers has an upper bound, i.e., the following formula holds: ϕ : ∀L ∃U ∀X (member (X, L) → X ≤ U ) The unfold/fold proof method works in two steps. In the first step, ϕ is transformed into a set of clauses by applying a variant of the Lloyd-Topor transformation [ 17 ], thereby deriving the following program Prop1: prop ← ¬p p ← list (L) ∧ ¬q(L) q(L) ← list (L) ∧ ¬r(L, U ) r(L, U ) ← X > U ∧ list (L) ∧ member (X, L) The predicate prop is equivalent to ϕ in the sense that M (Member ) |= ϕ iff M (Member ∪ Prop1) |= prop. In the second step, we eliminate the existential variables occurring in Prop1 (that is, the variables occurring in the body of a clause and not in its head) by applying the transformation strategy presented in [ 21 ]. We derive the following program Prop2 which defines the predicate prop: prop ← ¬p p ← p1 p1 ← p1 Now, Prop2 is a propositional program and has a finite perfect model, which is {prop}. Since all transformations we have made can be shown to preserve the perfect model, we have that M (Member ) |= ϕ iff M (Prop2) |= prop and, therefore, we have completed the proof of ϕ because prop belongs to M (Prop2).

Note that the unfold/fold proof method can be viewed as an extension to constraint logic programs of the quantifier elimination method, which has well-known applications in the field of automated theorem proving (see [ 22 ] for a brief survey). 4.2

Infinite-state model checking

Now we present a method for verifying temporal properties of infinite state systems based on the transformation of constraint logic programs [ 7 ].

As indicated in [ 4 ], the behavior of a concurrent system that evolves over time according to a given protocol can be modeled by means of a state transition system, that is, (i) a set S of states, (ii) an initial state s0 ∈ S, and (iii) a transition relation t ⊆ S × S. We assume that t is a total relation, that is, for every state s ∈ S there exists a state s0 ∈ S, called successor state of s, such that t(s, s0) holds. A computation path starting from a (possibly not initial) state s1 is an infinite sequence of states s1 s2 . . . such that, for every i ≥ 1, there is a transition from si to si+1.

The properties of the evolution over time of a concurrent system are specified by using a temporal logic called Computation Tree Logic (or CTL, for short [ 4 ]) which specifies the properties of the computation paths. The formulas of CTL are built from a given set of elementary properties of the states by using: (i) the connectives: ¬ (‘not’) and ∧ (‘and’), (ii) the following quantifiers along a computation path: g (‘for all states on the path’ or ‘globally’), f (‘there exists a state on the path’ or ‘in the future’), x (‘next time’), and u (‘until’), and (iii) the quantifiers over computation paths: a (‘for all paths’) and e (‘there exists a path’).

Very efficient algorithms and tools exist for verifying temporal properties of finite state systems, that is, systems where the set S of states is finite [ 4 ]. However, many concurrent systems cannot be modeled by finite state systems. Unfortunately, the problem of verifying CTL properties of infinite state systems is undecidable, in general, and thus, it cannot be approached by traditional model checking techniques. For this reason various methods based on automated theorem proving have been proposed for enhancing model checking and allowing us to deal with infinite state ht, A2, B1, B2i

A2 := B2+1 A2 < B2 ∨ B2 = 0 hw, A2, B1, B2i

A2 := 0 hu, A2, B1, B2i systems (see [ 5 ] for a method based on constraint logic programming). Due to the above mentioned undecidability limitation, all these methods are incomplete.

As an example of use of program transformation for verifying CTL properties of infinite state systems, now we consider the Bakery protocol [ 15 ] and we verify that it satisfies the mutual exclusion and starvation freedom properties.

Let us consider two agents A and B which want to access a shared resource in a mutual exclusive way by using the Bakery protocol. The state of agent A is represented by a pair hA1, A2i, where A1 is an element of the set {t, w, u} of control states (where t, w, and u stand for think, wait, and use, respectively) and A2 is a counter that takes values from the set of natural numbers. Analogously, the state of agent B is represented by a pair hB1, B2i. The state of the system consisting of the two agents A and B, whose states are hA1, A2i and hB1, B2i, respectively, is represented by the 4-tuple hA1, A2, B1, B2i. The transition relation t of the two agent system from an old state OldS to a new state NewS , is defined as follows: t(OldS , NewS ) ← tA(OldS , NewS ) t(OldS , NewS ) ← tB (OldS , NewS ) where the transition relation tA for the agent A is given by the following clauses whose bodies are conjunctions of constraints (see also Figure 1): tA(ht , A2, B1, B2i, hw , A21, B1, B2i) ← A21 = B2+1 tA(hw , A2, B1, B2i, hu, A2, B1, B2i) ← A2 < B2 tA(hw , A2, B1, B2i, hu, A2, B1, B2i) ← B2 = 0 tA(hu, A2, B1, B2i, ht , A21, B1, B2i) ← A21 = 0 The following analogous clauses define the transition relation tB for the agent B: tB (hA1, A2, t , B2i, hA1, A2, w , B21i) ← B21 = A2+1 tB (hA1, A2, w , B2i, hA1, A2, u, B2i) ← B2 < A2 tB (hA1, A2, w , B2i, hA1, A2, u, B2i) ← A2 = 0 tB (hA1, A2, u, B2i, hA1, A2, t , B21i) ← B21 = 0 Note that the system has an infinite number of states, because counters may increase in an unbounded way.

The temporal properties of a transition system are specified by defining a predicate sat (S, P ) which holds if and only if the temporal formula P is true at state S. For instance, the clauses defining sat (S, P ) for the cases where P is: (i) an elementary formula F , (ii) a formula of the form ¬F , (iii) a formula of the form F1 ∧ F2, (iv) a formula of the form ef (F ), are the following ones: sat (S, F ) ← elem(S, F ) sat (S, ¬F ) ← ¬sat (S, F ) sat (X, F1 ∧ F2) ← sat (X, F1) ∧ sat (X, F2) sat (S, ef (F )) ← sat (S, F ) sat (S, ef (F )) ← t (S, T ) ∧ sat (T , ef (F )) where elem(S, F ) holds iff F is an elementary property which is true at state S. In particular, for the Bakery protocol we have the following clause: elem(hu, A2, u, B2i, unsafe) ← that is, unsafe holds at a state where both agents A and B are in the control state u (both agents are accessing the shared resource at the same time).

Note that by ef we denote the composition of e (there exists a computation path) and f (there exists a state on the path) and, indeed, sat (S, ef (F )) holds iff there exists a computation path π starting from S and a state s on π such that F is true at s.

The mutual exclusion property holds for the Bakery protocol if there is no computation path starting from the initial state such that at a state on this path the unsafe property holds. Thus, the mutual exclusion property holds if sat (ht , 0, t , 0i, ¬ef (unsafe)) belongs to the perfect model M (Pmex ), where: (i) ht , 0, t , 0i is the initial state of the system and (ii) Pmex is the program consisting of the clauses for the predicates t, tA, tB , sat, and elem defined above.

In order to show that sat (ht , 0, t , 0i, ¬ef (unsafe)) ∈ M (Pmex ), we introduce a new predicate mex defined by the following clause:

(μ) mex ← sat (ht , 0, t , 0i, ¬ef unsafe) and we transform the program Pmex ∪ {μ} into a new program Q which contains a clause of the form mex ←. This transformation is performed by applying the definition, unfolding, and folding rules according to the specialization strategy, that is, a strategy that derives clauses specialized to the computation of predicate mex . From the correctness of the transformation rules we have that mex ∈ M (Q) iff mex ∈ M (Pmex ∪ {μ}) and, hence, sat (ht , 0, t , 0i, ¬ef (unsafe)) ∈ M (Pmex ), that is, the mutual exclusion property holds.

For the Bakery protocol we may also want to prove the starvation freedom property which ensures that an agent, say A, which requests the shared resource, will eventually get it. This property is expressed by the CTL formula: ag (wA → af (uA)), which is equivalent to: ¬ef ((wA ∧ ¬af (uA)). The clauses defining the elementary properties wA and uA are: elem(hw , A2, B1, B2i, wA) ← elem(hu, A2, B1, B2i, uA) ←

The clauses defining the predicate sat (S, P ) for the case where P is a CTL formula of the form af (F ) are: sat (X, af (F )) ← sat (X, F ) sat (X, af (F )) ← ts (X, Ys ) ∧ sat all (Ys , af (F )) sat all ([ ], F ) ← sat all ([X|Xs ], F ) ← sat (X, F ) ∧ sat all (Xs , F ) where ts (X, Ys ) holds iff Ys is a list of all successor states of X. For instance, one of the clauses defining predicate ts in our Bakery example is: ts (ht , A2, t , B2i, [hw , A21, t , B2i, ht , A2, w , B21i]) ←

A21 = B2+1 ∧ B21 = A2+1 which states that the state ht , A2, t , B2i has two possible successor states: hw , A21, t , B2i (with A21 = B2+1) and ht , A2, w , B21i (with B21 = A2+1).

Let Psf denote the program obtained by adding to Pmex the clauses defining: (i) the elementary properties wA and uA, (ii) the atom sat (X, af (F )), (iii) the predicate sat all , and (iv) the predicate ts . In order to verify the starvation freedom property we introduce the clause:

(σ) sf ← sat (ht , 0, t , 0i, ¬ef (wA ∧ ¬af (uA))) and, by applying the definition, unfolding, and folding rules according to the specialization strategy, we transform the program Psf ∪ {σ} into a new program R which contains a clause of the form sf ←.

The derivations needed for verifying the mutual exclusion and the starvation freedom properties were performed in a fully automatic way by using our experimental constraint logic program transformation system MAP [ 18 ]. 5

Conclusions and Future Directions

We have presented the program transformation methodology and we have demonstrated that it is very effective for: (i) the derivation of correct software modules from their formal specifications, and (ii) the proof of properties of programs. Since program transformation preserves correctness and improves efficiency, it is very useful for constructing software products which are provably correct and whose time and space performance is very high.

In order to make program transformation effective in practice we need to increase the level of automation of the transformation strategies for program improvement, program synthesis, and program verification. Furthermore, these strategies should be incorporated into powerful tools for program development.

An important direction for future research is also the exploration of new areas of application of the transformation methodology. In this paper we have described the use of program transformation for verifying temporal properties of infinite state concurrent systems. Similar techniques could also be devised for verifying other kinds of properties and other classes of systems, such as security properties of distributed systems, safety properties of hybrid systems, and protocol conformance of multiagent systems. A more challenging issue is the fully automatic synthesis of software systems which are guaranteed to satisfy the properties specified by the designer. 6

Acknowledgements

We would like to thank the editors of the Intelligenza Artificiale Magazine for their invitation to write this paper in honor of Prof. Alberto Martelli. We also thank Prof. Martelli for teaching us the ‘structural way’ of presenting algorithms which we learned from his unification paper [ 19 ].

Contacts

8

Biography

Alberto Pettorossi is professor of Theoretical Computer Science at the Engineering Faculty of the University of Roma “Tor Vergata”. His research activity has been in the area of rewriting systems and concurrent computation, and it is now concerned with the automatic derivation, transformation, and verification of programs.

Maurizio Proietti received his Laurea degree in Mathematics from the University of Roma “Sapienza”. He is a senior researcher at the Istituto di Analisi dei Sistemi e Informatica “A. Ruberti” of the National Research Council (IASI-CNR) in Roma. His research interests include various aspects of constraint and logic programming, and automatic methods for the transformation, synthesis, and verification of programs.

Valerio Senni is a Ph. D. student in Information Engineering at the the University of Roma “Tor Vergata”. He holds a research contract for the development of automatic methods for proving program correctness.

Photograph. A black and white glossy photograph, passport- sized of each author is also required. It will be printed in the corresponding biography box.

References

[1] A. Bossi , N. Cocco , and S. Etalle . Transforming normal programs by replacement . In Proc. Meta '92, LNCS 649 , 265 - 279 . Springer-Verlag, 1992 .

[2] A. Bundy . The automation of proof by mathematical induction. In A. Robinson and A . Voronkov, editors, Handbook of Automated Reasoning , volume I, 845 - 911 . North Holland, 2001 .

[3] R. M. Burstall and J. Darlington . A transformation system for developing recursive programs . J. ACM , 24 ( 1 ): 44 - 67 , January 1977 .

[4] E. M. Clarke , O. Grumberg , and D. Peled . Model Checking. MIT Press, 2000 .

[5] G. Delzanno and A. Podelski . Constraint-based deductive model checking . Int. J. Software Tools for Technology Transfer , 3 ( 3 ): 250 - 270 , 2001 .

[6] S. Etalle and M. Gabbrielli . Transformations of CLP modules . Theo. Comp. Sci. , 166 : 101 - 146 , 1996 .

[7] F. Fioravanti , A. Pettorossi , and M. Proietti . Verifying CTL properties of infinite state systems by specializing constraint logic programs . In Proc. VCL'01 , Florence (Italy), 85 - 96 . Univ. Southampton, UK, 2001 .

[8] F. Fioravanti , A. Pettorossi , and M. Proietti . Specialization with clause splitting for deriving deterministic constraint logic programs . In Proc. IEEE Int. Conf. on Systems, Man and Cybernetics , Hammamet (Tunisia) , Vol. 1 , 188 - 193 . IEEE Computer Society Press, 2002 .

[9] F. Fioravanti , A. Pettorossi , and M. Proietti . Transformation rules for locally stratified constraint logic programs . In Program Development in Computational Logic, LNCS 3049 , 292 - 340 . Springer-Verlag, 2004 .

[10] J. P. Gallagher . Tutorial on specialisation of logic programs . In Proc. PEPM '93 , Copenhagen, Denmark, 88 - 98 . ACM Press, 1993 .

[11] C. J. Hogger . Derivation of logic programs . Journal of the ACM , 28 ( 2 ): 372 - 392 , 1981 .

[12] J. Jaffar and M. Maher . Constraint logic programming: A survey . Journal of Logic Programming , 19 /20: 503 - 581 , 1994 .

[13] N. D. Jones , C. K. Gomard , and P. Sestoft . Partial Evaluation and Automatic Program Generation . Prentice Hall, 1993 .

[14] L. Kott . The McCarthy's induction principle: 'oldy' but 'goody' . Calcolo , 19 ( 1 ): 59 - 69 , 1982 .

[15] L. Lamport . A new solution of Dijkstra's concurrent programming problem . Communications ACM , 17 ( 8 ): 453 - 455 , 1974 .

[16] M. Leuschel and M. Bruynooghe . Logic program specialisation through partial deduction: Control issues . Theory and Practice of Logic Programming , 2 ( 4 &5): 461 - 515 , 2002 .

[17] J. W. Lloyd . Foundations of Logic Programming . Springer-Verlag, Berlin, 1987 . Second Edition .

[18] MAP . The MAP transformation system . http:// www.iasi.cnr.it/˜proietti/system.html,

[19] A. Martelli and U. Montanari . An efficient unification algorithm . ACM TOPLAS , 4 ( 12 ): 258 - 282 , 1982 .

[20] A. Pettorossi and M. Proietti . Synthesis and transformation of logic programs using unfold/fold proofs . Journal of Logic Programming , 41 ( 2 &3): 197 - 230 , 1999 .

[21] A. Pettorossi , M. Proietti , and V. Senni . Proving properties of constraint logic programs by eliminating existential variables . In Proc. ICLP '06, LNCS 4079 , 179 - 195 . Springer-Verlag, 2006 .

[22] M. O. Rabin . Decidable theories . In Jon Barwise, editor, Handbook of Mathematical Logic , 595 - 629 . North-Holland, 1977 .

[23] A. Roychoudhury , K. Narayan Kumar , C. R. Ramakrishnan , I. V. Ramakrishnan , and S. A. Smolka . Verification of parameterized systems using logic program transformations . In Proc. TACAS 2000 , Berlin, Germany, LNCS 1785 , 172 - 187 . Springer, 2000 .

[24] T. Sato and H. Tamaki . Transformational logic program synthesis . In Proc. Int. Conf. on Fifth Generation Computer Systems , 195 - 201 . ICOT, 1984 .

[25] H. Seki . Unfold/fold transformation of stratified programs . Theo. Comp. Sci. , 86 : 107 - 139 , 1991 .

[26] H. Tamaki and T. Sato . Unfold/fold transformation of logic programs . In Proc. ICLP ' 84 , 127 - 138 , Uppsala, Sweden. Uppsala University, 1984 .