PhD Defence: Formal Specification and Verification of Computer Algebra Software

Formal Specification and Verification of Computer Algebra Software

In this talk, we present 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 the corresponding thesis is 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. This task is more complex for a computer algebra language like Maple that for conventional programming languages as Maple supports non-standard types of objects and also requires abstract data types to model algebraic concepts and notions.

As a starting point, 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). Furthermore, we have defined a denotational semantics of MiniMaple and its specification language and proved the soundness of the translation with  respect to the operational semantics of Why3ML. Finally, we discuss the application of our verification framework to the Maple package DifferenceDifferential developed at our institute to compute bivariate difference-differential dimension polynomials using relative Gröbner bases.