DROPS

Document

DOI: 10.4230/LIPIcs.CP.2021.59

Automated Random Testing of Numerical Constrained Types

Authors: Ghiles Ziat, Matthieu Dien, and Vincent Botbol

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract

We propose an automated testing framework based on constraint programming techniques. Our framework allows the developer to attach a numerical constraint to a type that restricts its set of possible values. We use this constraint as a partial specification of the program, our goal being to derive property-based tests on such annotated programs. To achieve this, we rely on the user-provided constraints on the types of a program: for each function f present in the program, that returns a constrained type, we generate a test. The tests consists of generating uniformly pseudo-random inputs and checking whether f’s output satisfies the constraint. We are able to automate this process by providing a set of generators for primitive types and generator combinators for composite types. To derive generators for constrained types, we present in this paper a technique that characterizes their inhabitants as the solution set of a numerical CSP. This is done by combining abstract interpretation and constraint solving techniques that allow us to efficiently and uniformly generate solutions of numerical CSP. We validated our approach by implementing it as a syntax extension for the OCaml language.

Cite as

Ghiles Ziat, Matthieu Dien, and Vincent Botbol. Automated Random Testing of Numerical Constrained Types. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 59:1-59:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ziat_et_al:LIPIcs.CP.2021.59,
  author =	{Ziat, Ghiles and Dien, Matthieu and Botbol, Vincent},
  title =	{{Automated Random Testing of Numerical Constrained Types}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{59:1--59:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.59},
  URN =		{urn:nbn:de:0030-drops-153502},
  doi =		{10.4230/LIPIcs.CP.2021.59},
  annote =	{Keywords: Constraint Programming, Automated Random Testing, Abstract Domains, Constrained Types}
}

Document

DOI: 10.4230/LIPIcs.AofA.2018.14

Beyond Series-Parallel Concurrent Systems: The Case of Arch Processes

Authors: Olivier Bodini, Matthieu Dien, Antoine Genitrini, and Alfredo Viola

Published in: LIPIcs, Volume 110, 29th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2018)

Abstract

In this paper we focus on concurrent processes built on synchronization by means of futures. This concept is an abstraction for processes based on a main execution thread but allowing to delay some computations. The structure of a general concurrent process is a directed acyclic graph (DAG). Since the quantitative study of increasingly labeled DAG (directly related to processes) seems out of reach (this is a #P-complete problem), we restrict ourselves to the study of arch processes, a simplistic model of processes with futures. They are based on two parameters related to their sizes and their numbers of arches. The increasingly labeled structures seems not to be specifiable in the classical sense of Analytic Combinatorics, but we manage to derive a recurrence equation for the enumeration. For this model we first exhibit an exact and an asymptotic formula for the number of runs of a given process. The second main contribution is composed of a uniform random sampler algorithm and an unranking one that allow efficient generation and exhaustive enumeration of the runs of a given arch process.

Cite as

Olivier Bodini, Matthieu Dien, Antoine Genitrini, and Alfredo Viola. Beyond Series-Parallel Concurrent Systems: The Case of Arch Processes. In 29th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 110, pp. 14:1-14:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bodini_et_al:LIPIcs.AofA.2018.14,
  author =	{Bodini, Olivier and Dien, Matthieu and Genitrini, Antoine and Viola, Alfredo},
  title =	{{Beyond Series-Parallel Concurrent Systems: The Case of Arch Processes}},
  booktitle =	{29th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2018)},
  pages =	{14:1--14:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-078-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{110},
  editor =	{Fill, James Allen and Ward, Mark Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AofA.2018.14},
  URN =		{urn:nbn:de:0030-drops-89075},
  doi =		{10.4230/LIPIcs.AofA.2018.14},
  annote =	{Keywords: Concurrency Theory, Future, Uniform Random Sampling, Unranking, Analytic Combinatorics}
}

Search Results

Documents authored by Dien, Matthieu

Automated Random Testing of Numerical Constrained Types

Abstract

Cite as

Beyond Series-Parallel Concurrent Systems: The Case of Arch Processes

Abstract

Cite as

Thanks for your feedback!

Could not send message