Concolic Testing in Logic Programming

TL;DR

This paper presents an automatic concolic testing approach for logic programming that combines concrete and symbolic execution to achieve full path coverage, supported by theoretical guarantees and a prototype implementation.

Contribution

It introduces the first systematic concolic testing method for logic programming, combining concrete and symbolic execution with proven properties and practical validation.

Findings

Achieves full path coverage when it terminates

Proves basic properties of the testing technique

Demonstrates practical usefulness through a prototype

Abstract

Software testing is one of the most popular validation techniques in the software industry. Surprisingly, we can only find a few approaches to testing in the context of logic programming. In this paper, we introduce a systematic approach for dynamic testing that combines both concrete and symbolic execution. Our approach is fully automatic and guarantees full path coverage when it terminates. We prove some basic properties of our technique and illustrate its practical usefulness through a prototype implementation.