This work provides both a specification and a proof of correctness
for the system PDP (Prolog Distributed Processor) which make use
of Abstract State Machines (ASMs). PDP is a recomputation-based
model for parallel execution of Prolog on distributed memory.
The system exploits OR_paralleism, Independent AND_parallelism
as well as the combination of both. The verification process starts
from the SLD trees, which define the execution of a Prolog program,
and going through the parallel model, it arrives to the abstract
machine designed for PDP, an extension of the WAM (Warren Abstract
Machine), the most common sequential implementation of Prolog. The
first step of this process consists in defining  parallel SLD
subtrees, which are a kind of partition of the SLD tree for programs
whose clauses are annotated with parallelism. In a subsequent step the
parallel execution approach of PDP is modeled by means of an  OR_TASK
ASM. In this ASM each task is associated with the execution of a parallel
SLD subtree. The execution of the parallel SLD subtree corresponding to
each task is modeled by a NODE submachine which is an extension of
the one proposed by Börger and Rosenzweig to verify the sequential
execution of Prolog. Accordingly, the verification leans on the results
of this work in order to avoid the verification of the common points with
the sequential execution. The new elements of the execution due to
parallelism exploitation are modeled at successive steps of the
verification process, finally leading to the extended WAM which implements
PDP. The PDP verification proves correctness for this particular
system but it can readily be adapted to prove it in other related
parallel systems exploiting AND, OR or both kinds of parallelism.