Formal Proof of SCHUR Conjugate Function

Details Formal Proof of SCHUR Conjugate Function Formal Proof of SCHUR Conjugate Function

2010-04-28

arxiv.org/abs/1004.5034v1

Computer Science

Logic in Computer Science

To appear in CALCULEMUS 2010

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Formal Proof of SCHUR Conjugate Function does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Formal Proof of SCHUR Conjugate Function, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Formal Proof of SCHUR Conjugate Function will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-68961