Source author record

Wim Vanhoof

Wim Vanhoof appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science Software Engineering Computational Complexity Databases

Catalog footprint

What is connected

5works

4topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2020arXiv

An SMT-Based Concolic Testing Tool for Logic Programs

Concolic testing mixes symbolic and concrete execution to generate test cases covering paths effectively. Its benefits have been demonstrated for more than 15 years to test imperative programs. Other programming paradigms, like logic programming, have received less attention. In this paper, we present a concolic-based test generation method for logic programs. Our approach exploits SMT-solving for constraint resolution. We then describe the implementation of a concolic testing tool for Prolog and validate it on some selected benchmarks.

preprint2019arXiv

Anti-unification in Constraint Logic Programming

Anti-unification refers to the process of generalizing two (or more) goals into a single, more general, goal that captures some of the structure that is common to all initial goals. In general one is typically interested in computing what is often called a most specific generalization, that is a generalization that captures a maximal amount of shared structure. In this work we address the problem of anti-unification in CLP, where goals can be seen as unordered sets of atoms and/or constraints. We show that while the concept of a most specific generalization can easily be defined in this context, computing it becomes an NP-complete problem. We subsequently introduce a generalization algorithm that computes a well-defined abstraction whose computation can be bound to a polynomial execution time. Initial experiments show that even a naive implementation of our algorithm produces acceptable generalizations in an efficient way. Under consideration for acceptance in TPLP.

preprint2015arXiv

A Direct Symbolic Execution of SQL Code for Testing of Data-Oriented Applications

Symbolic execution is a technique which enables automatically generating test inputs (and outputs) exercising a set of execution paths within a program to be tested. If the paths cover a sufficient part of the code under test, the test data offer a representative view of the program's actual behaviour, which notably enables detecting errors and correcting faults. Relational databases are ubiquitous in software, but symbolic execution of pieces of code that manipulate them remains a non-trivial problem, particularly because of the complex structure of such databases and the complex behaviour of SQL statements. In this work, we define a direct symbolic execution for database manipulation code and integrate it with a more traditional symbolic execution of normal program code. The database tables are represented by relational symbols and the SQL statements by relational constraints over these symbols and the symbols representing the normal variables of the program. An algorithm based on these principles is presented for the symbolic execution of Java methods that implement business use cases by reading and writing in a relational database, the latter subject to data integrity constraints. The algorithm is integrated in a test generation tool and experimented over sample code. The target language for the constraints produced by the tool is the SMT-Lib standard and the used solver is Microsoft Z3. The results show that the proposed approach enables generating meaningful test data, including valid database content, in reasonable time. In particular, the Z3 solver is shown to be more scalable than the Alloy solver, used in our previous work, for solving relational constraints.

preprint2015arXiv

A Symbolic Execution Algorithm for Constraint-Based Testing of Database Programs

In so-called constraint-based testing, symbolic execution is a common technique used as a part of the process to generate test data for imperative programs. Databases are ubiquitous in software and testing of programs manipulating databases is thus essential to enhance the reliability of software. This work proposes and evaluates experimentally a symbolic ex- ecution algorithm for constraint-based testing of database programs. First, we describe SimpleDB, a formal language which offers a minimal and well-defined syntax and seman- tics, to model common interaction scenarios between pro- grams and databases. Secondly, we detail the proposed al- gorithm for symbolic execution of SimpleDB models. This algorithm considers a SimpleDB program as a sequence of operations over a set of relational variables, modeling both the database tables and the program variables. By inte- grating this relational model of the program with classical static symbolic execution, the algorithm can generate a set of path constraints for any finite path to test in the control- flow graph of the program. Solutions of these constraints are test inputs for the program, including an initial content for the database. When the program is executed with respect to these inputs, it is guaranteed to follow the path with re- spect to which the constraints were generated. Finally, the algorithm is evaluated experimentally using representative SimpleDB models.

preprint2010arXiv

A Test Automation Framework for Mercury

This paper presents a test automation framework for Mercury programs. We developed a method that generates runnable Mercury code from a formalized test suite, and which code provides a report on execution about the success of test cases. We also developed a coverage tool for the framework, which identifies and provide a visualization of the reached parts of the program when executing a given test suite.