Formally Specified Computer Algebra Software
Project Lead
Project Duration
01/10/2008 - 30/09/2011Project URL
Go to WebsitePublications
2014
[Khan]
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, Austria. ISSN 2791-4267 (online). February 2014. [pdf]@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Khan]
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, Austria. ISSN 2791-4267 (online). PhD Thesis, April 2014. [pdf]@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
2013
[Khan]
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, Austria. ISSN 2791-4267 (online). February 2013. [pdf]@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Khan]
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, Austria. ISSN 2791-4267 (online). June 2013. [pdf]@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
2012
[Khan]
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, Austria. ISSN 2791-4267 (online). January 2012. [pdf]@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Khan]
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, Austria. ISSN 2791-4267 (online). April 2012. [pdf]@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Khan]
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]@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}
}
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}
}
[Khan]
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.@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}
}
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}
}
[Schreiner]
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. [doi]@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}
}
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
[Khan]
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, Austria. ISSN 2791-4267 (online). April 2011. [pdf]@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Khan]
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]@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}
}
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}
}
[Khan]
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, Austria. ISSN 2791-4267 (online). November 2011. [pdf]@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
2009
[Schreiner]
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]@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}
}
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}
}
