Formally Specified Computer Algebra Software

Project Lead

Project Duration

01/10/2008 - 30/09/2011

Project URL

Go to Website

Publications

2014

On the Soundness of the Translation of MiniMaple to Why3ML

Muhammad Taimoor Khan

Technical report no. 14-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. February 2014. [pdf]
[bib]
@techreport{RISC4950,
author = {Muhammad Taimoor Khan},
title = {{On the Soundness of the Translation of MiniMaple to Why3ML}},
language = {english},
number = {14-01},
year = {2014},
month = {February},
keywords = {soundness, denotational semantics, operational semantics, principle of rule induction},
sponsor = {The research was funded by the Austrian Science Fund (FWF): W1214-N15, project DK10.},
length = {0},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Formal Specification and Verification of Computer Algebra Software

Muhammad Taimoor Khan

Technical report no. 14-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. PhD Thesis, April 2014. [pdf]
[bib]
@techreport{RISC4981,
author = {Muhammad Taimoor Khan},
title = {{Formal Specification and Verification of Computer Algebra Software}},
language = {english},
number = {14-04},
year = {2014},
month = {April},
howpublished = {PhD Thesis},
sponsor = {The research was funded by the Austrian Science Fund (FWF): W1214-N15, project DK10.},
length = {0},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

2013

Translation of MiniMaple to Why3ML

Muhammad Taimoor Khan

Technical report no. 13-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. February 2013. [pdf]
[bib]
@techreport{RISC4678,
author = {Muhammad Taimoor Khan},
title = {{Translation of MiniMaple to Why3ML}},
language = {english},
abstract = {In this paper, we give the complete definition of the translation of MiniMaple and its speci fication language to an intermediate language Why3ML of veri fication calculus Why3. For the veri fication, we first translate MiniMaple annotated program into a semantically equivalent Why3ML program, then veri fication conditions are generated by using Why3 corresponding verifi cation conditions generator. Finally, the correctness of the generated veri fication conditions can be proved by various Why3 back-end supported automatic and interactive theorem provers},
number = {13-01},
year = {2013},
month = {February},
sponsor = {FWF},
length = {58},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

On the Formal Verification of Maple Programs

Muhammad Taimoor Khan

Technical report no. 13-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. June 2013. [pdf]
[bib]
@techreport{RISC4734,
author = {Muhammad Taimoor Khan},
title = {{On the Formal Verification of Maple Programs}},
language = {english},
number = {13-07},
year = {2013},
month = {June},
sponsor = {FWF},
length = {0},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

2012

Formal Semantics of MiniMaple

Muhammad Taimoor Khan

Technical report no. 12-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. January 2012. [pdf]
[bib]
@techreport{RISC4414,
author = {Muhammad Taimoor Khan},
title = {{Formal Semantics of MiniMaple}},
language = {english},
abstract = {In this paper, we give the complete definition of a formal (denotational) semantics of a subset of the language of the computer algebra systems Maple which we call MiniMaple. As a next step we will develop a verification calculus for this language. The verification conditions generated by the calculus must be sound with respect to the formal semantics.},
number = {12-04},
year = {2012},
month = {January},
length = {72},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Formal Semantics of a Specification Language for MiniMaple

Muhammad Taimoor Khan

Technical report no. 12-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. April 2012. [pdf]
[bib]
@techreport{RISC4532,
author = {Muhammad Taimoor Khan},
title = {{Formal Semantics of a Specification Language for MiniMaple}},
language = {english},
number = {12-05},
year = {2012},
month = {April},
sponsor = {Austrian Science Fund (FWF)},
length = {60},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

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

A Type Checker for MiniMaple

Muhammad Taimoor Khan

Technical report no. 11-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. April 2011. [pdf]
[bib]
@techreport{RISC4325,
author = {Muhammad Taimoor Khan},
title = {{A Type Checker for MiniMaple}},
language = {english},
number = {11-05},
year = {2011},
month = {April},
sponsor = {FWF},
length = {105},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

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}
}

Towards a Behavioral Analysis of Computer Algebra Programs

Muhammad Taimoor Khan

Technical report no. 11-13 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. November 2011. [pdf]
[bib]
@techreport{RISC4402,
author = {Muhammad Taimoor Khan},
title = {{Towards a Behavioral Analysis of Computer Algebra Programs}},
language = {english},
number = {11-13},
year = {2011},
month = {November},
sponsor = {Austrian Science Fund (FWF)},
length = {21},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

2009

How to Write Postconditions with Multiple Cases

Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Technical report, November 2009. [pdf]
[bib]
@techreport{RISC3927,
author = {Wolfgang Schreiner},
title = {{How to Write Postconditions with Multiple Cases}},
language = {english},
abstract = {We investigate and compare the two major styles of writing program/function postconditions with multiple cases: as conjunctions ofimplications or as disjunctions of conjunctions. We show that bothstyles not only have different syntax but also different semantics andpragmatics and give recommendations for their use.},
year = {2009},
month = {November},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {formal methods, program specification, program verification},
length = {3}
}

Loading…