Static analysis of Prolog with cut

Abstract. This paper presents a general approach to the Abstract In-terpretation of Prolog programs with cut. In most of previous approaches the cut primitive is merely ignored. Our method consists in trasforming an interpreter for Prolog into an in-terpreter that computes on abstract values and that performs loop-checks by storing all encountered call patterns into a table. In order to guaran-tee correctness, this tabled interpreter needs information about the sure success of the corresponding concrete computations. Such information, called control information, is used to control the execution of the cuts by the tabled interpreter: a cut is executed only if the control information guarantees that it is also executed at the concrete level, otherwise, the domain