An integrated approach to assertion-based random testing in Prolog

Casso, Ignacio de and Morales Caballero, José Francisco and López García, Pedro and Hermenegildo, Manuel V. (2019). An integrated approach to assertion-based random testing in Prolog. In: "Logic-Based Program Synthesis and Transformation". Lecture Notes in Computer Science (12042). Springer, Suiza, pp. 159-176. ISBN 978-3-030-45259-9.


Title: An integrated approach to assertion-based random testing in Prolog
  • Casso, Ignacio de
  • Morales Caballero, José Francisco
  • López García, Pedro
  • Hermenegildo, Manuel V.
Item Type: Book Section
Title of Book: Logic-Based Program Synthesis and Transformation
Date: 2019
ISBN: 978-3-030-45259-9
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview


We present an approach for assertion-based random testing of Prolog programs that is tightly integrated within an overall assertionbased program development scheme. Our starting point is the Ciao model, a framework that unifies unit testing and run-time verification, as well as static verification and static debugging, using a common assertion language. Properties which cannot be verified statically are checked dynamically. In this context, the idea of generating random test values from assertion preconditions emerges naturally since these preconditions are conjunctions of literals, and the corresponding predicates can in principle be used as generators. Our tool generates valid inputs from the properties that appear in the assertions shared with other parts of the model, and the run time-check instrumentation of the Ciao framework is used to perform a wide variety of checks. This integration also facilitates the combination with static analysis. The generation process is based on running standard predicates under non-standard (random) search rules. Generation can be fully automatic but can also be guided or defined specifically by the user. We propose methods for supporting (C)LP-specific properties, including combinations of shape-based (regular) types and variable sharing and instantiation, and we also provide some ideas for shrinking for these properties. We also provide a case study applying the tool to the verification and checking of the code of some of the abstract domains used by the Ciao system.

Funding Projects

Government of SpainTIN2015-67522-C3-1-RTRACESFundación IMDEA SoftwareTecnologías y herramientas para el desarrollo de software consciente de los recursos, correcto y eficiente (IMDEA)
Madrid Regional GovernmentP2018/TCS-4339BLOQUES-CMUnspecifiedContratos inteligentes y blockchains escalables y seguros mediante verificación y análisis

More information

Item ID: 64738
DC Identifier:
OAI Identifier:
DOI: 10.1007/978-3-030-45260-5
Official URL:
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 16 Oct 2020 14:20
Last Modified: 16 Oct 2020 14:20
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM