Showing 1–3 of 3 results for author: Jourdan, J

Sparsity Preserving Algorithms for Octagons

Authors: Jacques-Henri Jourdan

Abstract: Known algorithms for manipulating octagons do not preserve their sparsity, leading typically to quadratic or cubic time and space complexities even if no relation among variables is known when they are all bounded. In this paper, we present new algorithms, which use and return octagons represented as weakly closed difference bound matrices, preserve the sparsity of their input and have better perf… ▽ More Known algorithms for manipulating octagons do not preserve their sparsity, leading typically to quadratic or cubic time and space complexities even if no relation among variables is known when they are all bounded. In this paper, we present new algorithms, which use and return octagons represented as weakly closed difference bound matrices, preserve the sparsity of their input and have better performance in the case their inputs are sparse. We prove that these algorithms are as precise as the known ones. △ Less

Submitted 1 December, 2016; originally announced December 2016.

Comments: in Isabella Mastroeni. Numerical and symbolic abstract domains, Sep 2016, Edinburgh, United Kingdom. Elsevier, Numerical and symbolic abstract domains, pp.14, 2016

Implementing and reasoning about hash-consed data structures in Coq

Authors: Thomas Braibant, Jacques-Henri Jourdan, David Monniaux

Abstract: We report on four different approaches to implementing hash-consing in Coq programs. The use cases include execution inside Coq, or execution of the extracted OCaml code. We explore the different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs not available in Coq. We discuss the possible consequences in terms of p… ▽ More We report on four different approaches to implementing hash-consing in Coq programs. The use cases include execution inside Coq, or execution of the extracted OCaml code. We explore the different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs not available in Coq. We discuss the possible consequences in terms of performances and guarantees. We use the running example of binary decision diagrams and then demonstrate the generality of our solutions by applying them to other examples of hash-consed data structures. △ Less

Submitted 25 September, 2015; v1 submitted 7 November, 2013; originally announced November 2013.

Journal ref: Journal of Automated Reasoning, Springer Verlag (Germany), 2014, 53 (3), pp.271-304

Implementing hash-consed structures in Coq

Authors: Thomas Braibant, Jacques-Henri Jourdan, David Monniaux

Abstract: We report on three different approaches to use hash-consing in programs certified with the Coq system, using binary decision diagrams (BDD) as running example. The use cases include execution inside Coq, or execution of the extracted OCaml code. There are different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs no… ▽ More We report on three different approaches to use hash-consing in programs certified with the Coq system, using binary decision diagrams (BDD) as running example. The use cases include execution inside Coq, or execution of the extracted OCaml code. There are different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs not available in Coq. We discuss the possible consequences in terms of performances and guarantees. △ Less

Submitted 22 April, 2013; originally announced April 2013.