Zobrazeno 1 - 10
of 28
pro vyhledávání: '"Weis, Pierre"'
Autor:
Boldo, Sylvie, Clément, François, Filliâtre, Jean-Christophe, Mayero, Micaela, Melquiond, Guillaume, Weis, Pierre
Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy
Externí odkaz:
http://arxiv.org/abs/1212.6641
Autor:
Boldo, Sylvie, Clement, Francois, Filliâtre, Jean-Christophe, Mayero, Micaela, Melquiond, Guillaume, Weis, Pierre
Publikováno v:
Journal of Automated Reasoning 50, 4 (2013) 423-456
We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and
Externí odkaz:
http://arxiv.org/abs/1112.1795
Publikováno v:
N° RR-7446 (2010)
We transpose an optimal control technique to the image segmentation problem. The idea is to consider image segmentation as a parameter estimation problem. The parameter to estimate is the color of the pixels of the image. We use the adaptive paramete
Externí odkaz:
http://arxiv.org/abs/1011.2292
Autor:
Boldo, Sylvie, Clément, François, Filliâtre, Jean-Christophe, Mayero, Micaela, Melquiond, Guillaume, Weis, Pierre
Publikováno v:
Interactive Theorem Proving 6172 (2010) 147-162
Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The
Externí odkaz:
http://arxiv.org/abs/1005.0824
Publikováno v:
Dans 16th European Symposium on Programming (2006)
Many algorithms use concrete data types with some additional invariants. The set of values satisfying the invariants is often a set of representatives for the equivalence classes of some equational theory. For instance, a sorted list is a particular
Externí odkaz:
http://arxiv.org/abs/cs/0701031
The estimation of distributed parameters in partial differential equations (PDE) from measures of the solution of the PDE may lead to under-determination problems. The choice of a parameterization is a usual way of adding a-priori information by redu
Externí odkaz:
http://arxiv.org/abs/math/0606747
Autor:
Boldo, Sylvie, Clément, François, Filliâtre, Jean-Christophe, Mayero, Micaela, Melquiond, Guillaume, Weis, Pierre
Publikováno v:
In Computers and Mathematics with Applications August 2014 68(3):325-352
Autor:
Weis, Pierre.
Th.--Inform.--Paris 7, 1987.
Externí odkaz:
http://catalogue.bnf.fr/ark:/12148/cb375938000
Autor:
Weis, Pierre.
Th.--Informatique--Paris VII, 1987.
1988 d'après la déclaration de dépôt légal. Bibliogr. p. 289-297.
1988 d'après la déclaration de dépôt légal. Bibliogr. p. 289-297.
Externí odkaz:
http://catalogue.bnf.fr/ark:/12148/cb34935244g
Autor:
Bonichon, Richard, Weis, Pierre
Publikováno v:
28ièmes Journées Francophones des Langages Applicatifs
28ièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
28ièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
International audience; Pretty-printing can be described as finding a good-looking solution to typeset data according to a set of formatting conventions. Oppen [6] pioneered the field with an algorithmic solution to pretty-printing, using the notions
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::0db6b39b6cf3de6b7ea603ec5107855b
https://hal.archives-ouvertes.fr/hal-01503081/document
https://hal.archives-ouvertes.fr/hal-01503081/document