Formally Specified Computer Algebra Software

Project Lead

Project Duration

01/10/2008 - 30/09/2011

Project URL

Go to Website

Publications

2012

Towards the Formal Specification and Verification of Maple Programs

Muhammad Taimoor Khan, Wolfgang Schreiner

In: Intelligent Computer Mathematics, Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, Volker Sorge (ed.), Lecture Notes in Artificial Intelligence (LNAI) 7362, pp. 231-247. July 2012. Springer-Verlag, Berlin/Heidelberg, ISBN 978-3-642-31373-8. Awarded with a Best Student Paper Award. [url] [pdf]
[bib]
@incollection{RISC4538,
author = {Muhammad Taimoor Khan and Wolfgang Schreiner},
title = {{Towards the Formal Specification and Verification of Maple Programs}},
booktitle = {{Intelligent Computer Mathematics}},
language = {english},
series = {Lecture Notes in Artificial Intelligence (LNAI)},
volume = {7362},
pages = {231--247},
publisher = {Springer-Verlag},
address = {Berlin/Heidelberg},
isbn_issn = {ISBN 978-3-642-31373-8},
year = {2012},
month = {July},
annote = {The original publication is available at www.springerlink.com},
note = {Awarded with a Best Student Paper Award},
editor = {Johan Jeuring and John A. Campbell and Jacques Carette and Gabriel Dos Reis and Petr Sojka and Makarius Wenzel and Volker Sorge},
refereed = {yes},
sponsor = {Austrian Science Fund (FWF)},
length = {17},
url = {http://www.springerlink.com}
}

On the Formal Semantics of MiniMaple and its Specification Language

Muhammad Taimoor Khan

In: Proceedings of the 10th International Conference on Frontiers of Information Technology (FIT 2012), xxx (ed.), pp. 00-00. December 2012. IEEE Digital Library, xxx.
[bib]
@inproceedings{RISC4593,
author = {Muhammad Taimoor Khan},
title = {{On the Formal Semantics of MiniMaple and its Specification Language}},
booktitle = {{Proceedings of the 10th International Conference on Frontiers of Information Technology (FIT 2012)}},
language = {english},
pages = {00--00},
publisher = {IEEE Digital Library},
isbn_issn = {xxx},
year = {2012},
month = {December},
editor = {xxx},
refereed = {yes},
length = {0}
}

Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs

Wolfgang Schreiner

In: Proceedings First Workshop on CTP Components for Educational Software (THedu'11), Pedro Quaresma and Ralph-Johan Back (ed.), Electronic Proceedings in Theoretical Computer Science (EPTCS) 79, pp. 124-142. February 2012. Wroclaw, Poland, July 31, 2011, ISSN: 2075-2180. [url]
[bib]
@inproceedings{RISC4429,
author = {Wolfgang Schreiner},
title = {{Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs}},
booktitle = {{Proceedings First Workshop on CTP Components for Educational Software (THedu'11)}},
language = {english},
abstract = {We present an approach to program reasoning which inserts between a program and its verification conditions an additional layer, the denotation of the program expressed in a declarative form. The program is first translated into its denotation from which subsequently the verification conditions are generated. However, even before (and independently of) any verification attempt, one may investigate the denotation itself to get insight into the "semantic essence" of the program, in particular to see whether the denotation indeed gives reason to believe that the program has the expected behavior. Errors in the program and in the meta-information may thus be detected and fixed prior to actually performing the formal verification. More concretely, following the relational approach to program semantics, we model the effect of a program as a binary relation on program states. A formal calculus is devised to derive from a program a logic formula that describes this relation and is subject for inspection and manipulation. We have implemented this idea in a comprehensive form in the RISC ProgramExplorer, a new program reasoning environment for educational purposes which encompasses the previously developed RISC ProofNavigator as an interactive proving assistant.},
series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
number = {79},
pages = {124--142},
address = {Wroclaw, Poland, July 31, 2011},
isbn_issn = {ISSN: 2075-2180},
year = {2012},
month = {February},
editor = {Pedro Quaresma and Ralph-Johan Back},
refereed = {yes},
keywords = {formal methods, program verification, computer science education},
length = {19},
url = {http://dx.doi.org/10.4204/EPTCS.79.8}
}

2011

Towards a Behavioral Analysis of Computer Algebra Programs (Extended Abstract)

Muhammad Taimoor Khan, Wolfgang Schreiner

In: Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11), Paul Pettersson and Cristina Seceleanu (ed.), pp. 42-44. October 2011. Vasteras, Sweden, Doktoratskolleg, Research Institute for Symbolic Computation, ISSN 1404-3041. [pdf]
[bib]
@inproceedings{RISC4398,
author = {Muhammad Taimoor Khan and Wolfgang Schreiner},
title = {{Towards a Behavioral Analysis of Computer Algebra Programs (Extended Abstract)}},
booktitle = {{Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11)}},
language = {english},
pages = {42--44},
address = {Vasteras, Sweden},
isbn_issn = {ISSN 1404-3041},
year = {2011},
month = {October},
editor = {Paul Pettersson and Cristina Seceleanu},
refereed = {yes},
organization = {Doktoratskolleg},
institution = {Research Institute for Symbolic Computation},
sponsor = {Austrian Science Fund (FWF)},
length = {3}
}

Loading…