21 research outputs found
Optimizing Canonical Structures
No full textInternational audienceWhile expanding Mathematical Components, a library of formalized mathematics for Rocq, we observed scalability issues in the latter’s unification algorithm. We found that the performance issue comes from the handling of Canonical Structures and proposed a patch, which has been integrated into Rocq 9.0
Décomposition Algébrique Cylindrique en Coq/Rocq
No full textLa Décomposition Algébrique Cylindrique (ou CAD) est un outil fondamental de la géométrie semi-algébrique. C'est un algorithme doublement exponentiel dont l'application phare est l'élimination des quantificateurs dans les formules de la théorie des corps réels clos. En particulier, il permet de décider si des systèmes d'inéquations polynomiales sont satisfiables. Cet article décrit une formalisation de la correction de cet algorithme dans l'assistant de preuve Coq/Rocq. Si l'algorithme n'est pas implémenté de façon à être exécuté, il s'agit d'une étape vers une implémentation vérifiée de la CAD, où les seuls éléments manquant sont des implémentations efficaces des structures de données et des algorithmes requis. MathComp, et plus précisément son extension à la géométrie semi-algébrique [MC12, Dja18]. Certaines des primitives que nous utilisons, comme l'isolation des racines d'un polynôme réel ont déjà été formalisée, tandis que d'autres, comme l'obtention de points entre deux racines d'un polynôme, ne le sont pas
Optimizing Canonical Structures
No full textInternational audienceWhile expanding Mathematical Components, a library of formalized mathematics for Rocq, we observed scalability issues in the latter’s unification algorithm. We found that the performance issue comes from the handling of Canonical Structures and proposed a patch, which has been integrated into Rocq 9.0
Optimizing Canonical Structures
No full textInternational audienceWhile expanding Mathematical Components, a library of formalized mathematics for Rocq, we observed scalability issues in the latter’s unification algorithm. We found that the performance issue comes from the handling of Canonical Structures and proposed a patch, which has been integrated into Rocq 9.0
Décomposition Algébrique Cylindrique en Coq/Rocq
No full textInternational audienceLa Décomposition Algébrique Cylindrique (ou CAD) est un outil fondamental de la géométrie semi-algébrique. C’est un algorithme doublement exponentiel dont l’application phare est l’élimination des quantificateurs dans les formules de la théorie des corps réels clos. En particulier, il permet de décider si des systèmes d’inéquations polynomiales sont satisfiables. Cet article décrit la première formalisation de la correction de cet algorithme dans un assistant de preuve. Si l’algorithme n’est pas implémenté de façon à être exécuté, il s’agit d’une étape vers une implémentation vérifiée de la CAD, où les seuls éléments manquants sont des implémentations efficaces des structures de données et des algorithmes requis
De Pékin à Paris (1900-1904) : les tribulations d’une collection de peintures chinoises
No full textFrom Peking to Paris, 1900-1904 : the tribulations of a collection of Chinese paintings.
The French School of the Far East (Ecole française d’Extrême-Orient, E.F.E.O.) was founded on 20 January 1900 in Saigon. One of its principal missions was to build up a collection of intellectual tools (a library, a museum) for the archaeological and philological study of the Indonesian peninsula and of its nearby civilisations : China, India and Malaya. One of the earliest young students sent from France was Paul Pelliot, who, in 1900, was despatched to Peking where he collected a considerable number of books, manuscripts and art objects for the school. In 1902, the school moved to Hanoi, the collections being stored in a building of the Exhibition pavilion. This building was severely damaged during a cyclone on 7 June 1903, and, since the projected museum had not yet been realised, in 1904 the collections were sent to Paris, to the Louvre and to the National Library. Ten of the Chinese paintings from the Pelliot collection were exhibited to the public at the Louvre. The comments of the contemporary specialists are indicative of the difference between that time and our own with regards to our appreciation and understanding of Chinese painting. Furthermore, the common Chinese custom of copying paintings led to many errors in attribution and dating. Only one inventory register, apparently drawn up on two separate occasions, survives today. In 1922, the Chinese paintings from the Pelliot collection were transferred from the Louvre to the Musée Guimet. They are 125 scrolls, representing three incomplete series of liturgical paintings. These paintings are presently being restored. According to the author of the present article, some of the mould on them date from the cyclone damage of 1903. A new appraisal of these works is also under way. They have long been underestimated, and their interest for the study of Buddhist and Taoist ritual is considerable.Gyss-Vermande Caroline. De Pékin à Paris (1900-1904) : les tribulations d’une collection de peintures chinoises. In: Histoire de l'art, N°21-22, 1993. Collections et collectionneurs. pp. 71-79
Data Cache Analysis by Counting Integer Points
No full textInternational audienceThe scheduling of reliable real-time systems require a precise and sound analysis of the execution times of their tasks. Part of these execution times is spent fetching data from the main memory to the cache memories. These fetch events occur on cache misses, but cache misses are hard to predict when the program accesses an array. An imprecise cache miss analysis can lead to an imprecise but still sound Worst-Case Execution Time (WCET) analysis. In this article we present a framework for deriving an upper bound to the number of times a data-accessing instruction triggers a cache miss. Backed by this framework, we present an analysis that produces numeric or symbolic bounds, by reasoning on a short history of accesses and by counting the number of integer points in a volume with an existing tool (Barvinok). Using such bounds will improve the precision of the estimations delivered by the WCET analyses.L'ordonnancement de systèmes temps-réel fiables nécessite une analyse précise et correcte du temps d'exécution de leurs tâches. Un partie de ces temps d'exécution est passée à rapatrier des données depuis la mémoire centrale vers les mémoires caches. Cet événements ont lieu lorsque se produit un défaut de cache, mais ces défauts de cache sont difficiles à prédire quand le programme accède à un tableau. Une analyse de défaut de cache imprécise peut mener à une analyse imprécise, quoique correcte, du pire temps d'exécution. Dans cet article, nous présentons un cadre théorique pour dériver une borne supérieure au nombre de fois qu'une instruction accédant aux données peut déclencher un défaut de cache. En s'appuyant sur ce cadre, nous présentons une analyse qui produit des bornes numériques ou symboliques en raisonnant sur un bref historique des accès et en comptant un nombre de points à coordonnées entières dans un volume, à l'aide d'un outil existant (Barvinok). L'utilisation de ces bornes améliorera la précision des estimations réalisées par les analyses de temps d'exécution
Financiele haalbaarheid van meervoudig ruimtegebruik bij infrastructurele knooppunten
No full textTransport & PlanningCivil Engineering and Geoscience
Physarum-Inspired Multi-Commodity Flow Dynamics
No full textIn wet-lab experiments, the slime mold Physarum polycephalum has demonstrated
its ability to solve shortest path problems and to design efficient networks.
For the shortest path problem, a mathematical model for the evolution of the
slime is available and it has been shown in computer experiments and through
mathematical analysis that the dynamics solves the shortest path problem. In
this paper, we introduce a dynamics for the network design problem. We
formulate network design as the problem of constructing a network that
efficiently supports a multi-commodity flow problem. We investigate the
dynamics in computer simulations and analytically. The simulations show that
the dynamics is able to construct efficient and elegant networks. In the
theoretical part we show that the dynamics minimizes an objective combining the
cost of the network and the cost of routing the demands through the network. We
also give alternative characterization of the optimum solution.Comment: to appear in Theoretical Computer Scienc
