CLP-Translated Program

Concept

A CLP-translated program is a Constraint Logic Programming representation of an imperative program (such as Java) produced by a translation scheme that maps each method to a set of CLP rules. The translation preserves the control flow of the original program, transforms iteration into recursion, and augments each rule with an additional trace term argument of the form m(k, ⟨Tc_m^i, …, Tc_m^c⟩), where k indexes the rule and the variables hold trace terms for sub-calls. CLP-translated programs are used as the basis for symbolic execution, test case generation (TCG), trace-abstraction construction, and trace-guided (guided) TCG for structural coverage criteria such as all-local-paths and program-points.

First seen 7/7/2026

Last seen 7/7/2026

Evidence 5 chunks

Wiki v1

WIKI

CLP-Translated Program

Definition and Overview

A CLP-translated program is the result of translating an imperative program (e.g., a Java program) into an equivalent Constraint Logic Programming (CLP) program. The translation preserves the control flow of the original program, converts iteration into recursion, and represents each method as a set of CLP rules. Each Java method corresponds to a set of predicates in the CLP program; for example, in the motivating example the Java method lcm is translated into the predicates lcm, cont, check, and div.

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

2 connections

Guided Test Case Generation ← uses 100% 2e

Guided TCG uses CLP-translated programs as input for trace-guided symbolic execution.

Trace Abstraction ← derived from 100% 1e

The trace abstraction is derived from the CLP-translated program by removing non-trace arguments.

LINKED ENTITIES

2 links

Guided Test Case Generation USES Extracted graph relationship

Trace Abstraction DERIVED_FROM Extracted graph relationship

CITATIONS

8 sources

8 citations — click to expand

[1] A CLP-translated program preserves the control flow of the original imperative program, transforms iteration into recursion, and represents each method as a set of CLP rules. A Generic Framework for Guided Test Case Generation via CLP-based Symbolic Execution

[2] Each rule includes a trace term T of the form m(k, ⟨Tc_m^i, …, Tc_m^c⟩) as a supplementary argument, where k is the rule index and the variables hold trace terms for sub-call predicates. A Generic Framework for Guided Test Case Generation via CLP-based Symbolic Execution

[3] Symbolic execution of a CLP-translated program produces a CLP derivation tree Tm with root m(I, O, Hi, Ho, E, T) and initial empty constraint store, using the union of the program and built-in predicates for dynamic memory. A Generic Framework for Guided Test Case Generation via CLP-based Symbolic Execution

[4] A test case for m w.r.t. a termination criterion C is a tuple ⟨θ, T⟩ of the constraint store and trace term from a successful branch of the finite symbolic execution tree TmC, and TCG is the process of generating test cases for all such branches. A Generic Framework for Guided Test Case Generation via CLP-based Symbolic Execution

[5] A coverage criterion is a pair ⟨TC, SC⟩ with TC ensuring finiteness (the paper uses loop-k) and SC selecting paths/test cases; all-local-paths and program-points are the two structural criteria studied. A Generic Framework for Guided Test Case Generation via CLP-based Symbolic Execution

[6] The trace-abstraction of a CLP-translated program P is obtained by keeping only rule-call atoms in each body and retaining only the last (trace) argument in heads and surviving atoms, and essentially corresponds to the control-flow graph. A Generic Framework for Guided Test Case Generation via CLP-based Symbolic Execution

[7] Trace-guided TCG uses trace terms of the CLP-translated program as input arguments (possibly partially instantiated with free logic variables) to steer symbolic execution towards specific paths needed to satisfy the selection criterion. A Generic Framework for Guided Test Case Generation via CLP-based Symbolic Execution

[8] Soundness, completeness, and effectiveness of the guided TCG scheme depend solely on the trace generator; a sound trace generator yields traces satisfying the coverage criterion, a complete one over-approximates the set of satisfying traces, and effectiveness relates to the number of unfeasible traces generated. A Generic Framework for Guided Test Case Generation via CLP-based Symbolic Execution