Butelle, Franck; Hivert, Florent; Mayero, Micaela; Toumazet, Frédéric Formal proof of SCHUR conjugate function. (English) Zbl 1286.68392 Autexier, Serge (ed.) et al., Intelligent computer mathematics. 10th international conference, AISC 2010, 17th symposium, Calculemus 2010, and 9th international conference, MKM 2010, Paris, France, July 5–10, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14127-0/pbk). Lecture Notes in Computer Science 6167. Lecture Notes in Artificial Intelligence, 158-171 (2010). Summary: The 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. It allows us to annotate C functions and to generate proof obligations, which are proved using several automated theorem provers. In this paper, we also draw on methodology, discussing on how to formally prove this kind of program.For the entire collection see [Zbl 1194.68011]. Cited in 1 Document MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 05-04 Software, source code, etc. for problems pertaining to combinatorics 05E05 Symmetric functions and generalizations 22-04 Software, source code, etc. for problems pertaining to topological groups 22E99 Lie groups Software:Isabelle/HOL; SCHUR; PVS; Frama-C; SIMPLIFY; z3; cvc3 PDFBibTeX XMLCite \textit{F. Butelle} et al., Lect. Notes Comput. Sci. 6167, 158--171 (2010; Zbl 1286.68392) Full Text: DOI arXiv