Concolic testing in CLP

DOI10.1017/S1471068420000216MaRDI QIDQ5140007zbMATH OpenFDO

Authors Fred Mesnard, Étienne Payet, Germán Vidal

Publication date 13 December 2020

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2008.00421

zbMATH Keywords

CLPconcolic testingverification

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Concolic testing is a popular software verification technique based on a combination of concrete and symbolic execution. Its main focus is finding bugs and generating test cases with the aim of maximizing code coverage. A previous approach to concolic testing in logic programming was not sound because it only dealt with positive constraints (by means of substitutions) but could not represent negative constraints. In this paper, we present a novel framework for concolic testing of CLP programs that generalizes the previous technique. In the CLP setting, one can represent both positive and negative constraints in a natural way, thus giving rise to a sound and (potentially) more efficient technique. Defining verification and testing techniques for CLP programs is increasingly relevant since this framework is becoming popular as an intermediate representation to analyze programs written in other programming paradigms.

Recommendations

• Concolic testing in logic programming
• On the completeness of selective unification in concolic testing of logic programs
• Concolic execution in functional programming by program instrumentation
• Concolic execution and test case generation in Prolog
• Selective Unification in (Constraint) Logic Programming*

Cites work

• A linear operational semantics for termination and complexity analysis of ISO prolog
• Concolic execution and test case generation in Prolog
• Concolic execution in functional programming by program instrumentation
• Concolic testing in logic programming
• Horn clauses as an intermediate representation for program analysis and transformation
• scientific article; zbMATH DE number 1688810 (Why is no real title available?)
• scientific article; zbMATH DE number 25188 (Why is no real title available?)
• On the completeness of selective unification in concolic testing of logic programs
• Partial evaluation in logic programming
• Symbolic execution and program testing
• The execution algorithm of mercury, an efficient purely declarative logic programming language
• The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1
• Towards Typed Prolog

Cited in

(13)

• An SMT-based concolic testing tool for logic programs
• Sound and complete concolic testing for higher-order functions
• On the completeness of selective unification in concolic testing of logic programs
• Abstraction-driven concolic testing
• Concolic execution and test case generation in Prolog
• Test Data Generation of Bytecode by CLP Partial Evaluation
• Concolic testing in logic programming
• Resource-Driven CLP-Based Test Case Generation
• Towards testing concurrent objects in CLP
• Concolic execution in functional programming by program instrumentation
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Symbolic Model Construction for Saturated Constrained Horn Clauses
• Concolic testing heap-manipulating programs

Describes a project that uses

Uses Software

• SeaHorn
• CUTE
• DART
• Mercury
• jCUTE

This page was built for publication: Concolic testing in CLP

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5140007)