Micaela Mayero
Formal Proof of a Wave Equation Resolution Scheme: the Method Error.
Mon, 05/10/2010 - 15:01 — SomNambulAuthors: Micaela Mayero, Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Guillaume Melquiond, Pierre Weis
Subjects: Logic in Computer Science
AbstractPopular 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 main difficulties lie in the proper definition of
asymptotic behaviors and the implicit way they are handled in the mathematical
pen-and-paper proofs. To our knowledge, this is the first time such kind of
mathematical proof is machine-checked.Formal Proof of SCHUR Conjugate Function.
Thu, 04/29/2010 - 15:01 — SomNambulAuthors: Florent Hivert, Franck Butelle, Micaela Mayero, Frédéric Toumazet
Subjects: Logic in Computer Science
AbstractThe main goal of our work is to formally prove the correctness of the key
commands of the SCHUR software, an interactive program for calculating with
characters of Lie groups and symmetric functions. The core of the computations
relies on enumeration and manipulation of combinatorial structures. As a first
"proof of concept", we present a formal proof of the conjugate function,
written in C. This function computes the conjugate of an integer partition. To
formally prove this program, we use the Frama-C software.
User login
