Towards the formal specification and verification of Maple programs

DOI10.1007/978-3-642-31374-5_16zbMATH Open1360.68590arXiv1207.2300OpenAlexW1601297445MaRDI QIDQ2907326FDOQ2907326

Authors: Muhammad Taimoor Khan, Wolfgang Schreiner 

Publication date: 7 September 2012

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: In this paper, we present our ongoing work and initial results on the formal specification and verification of MiniMaple (a substantial subset of Maple with slight extensions) programs. The main goal of our work is to find behavioral errors in such programs w.r.t. their specifications by static analysis. This task is more complex for widely used computer algebra languages like Maple as these are fundamentally different from classical languages: they support non-standard types of objects such as symbols, unevaluated expressions and polynomials and require abstract computer algebraic concepts and objects such as rings and orderings etc. As a starting point we have defined and formalized a syntax, semantics, type system and specification language for MiniMaple.

Full work available at URL: https://arxiv.org/abs/1207.2300

Recommendations

• On formal specification of Maple programs
• scientific article; zbMATH DE number 1262431
• scientific article; zbMATH DE number 516980
• Dealing with algebraic expressions over a field in Coq using Maple
• Partial evaluation of Maple

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (2)

• On formal specification of Maple programs
• Compiling dyadic first-order specifications into map algebra

Uses Software

• Maple
• LARCH
• Why3
• Spec#
• Miranda
• MiniMaple

This page was built for publication: Towards the formal specification and verification of Maple programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2907326)