MiniMaple is a novel framework for the formal specification and verification of computer algebra programs and its application to a non-trivial computer algebra package. The programs are written in the language MiniMaple, which is a substantial subset of the language of the commercial computer algebra system Maple. The main goal of a corresponding PhD thesis was the application of light-weight formal methods to MiniMaple programs (annotated with types and behavioral specifications) for finding internal inconsistencies and violations of methods preconditions by employing static program analysis.

Towards this goal, we have defined and formalized a syntax, semantics, type system and specification language for MiniMaple. For verification, we automatically translate the (types and specification) annotated MiniMaple program into (a behaviorally equivalent program in) the intermediate language Why3ML of the verification tool Why3; from the translated program, Why3 generates verification conditions whose correctness can be proved by various automated and interactive theorem provers (e.g. Z3 and Coq).