Program Verification using Algebraic Methods

Project Lead

Project Duration

01/01/2007 - 31/12/2007

Project URL

Go to Website

Publications

2011

Sound and Complete Verification Condition Generator for Functional Recursive Programs.

N. Popov, T. Jebelean

In: Numerical and Symbolic Scientific Computing: Progress and Prospects, U. Langer and P. Paule (ed.), pp. 219-256. 2011. Springer, Wien, ISBN 978-3-7091-0793-5.
[bib]
@incollection{RISC4342,
author = {N. Popov and T. Jebelean},
title = {{Sound and Complete Verification Condition Generator for Functional Recursive Programs.}},
booktitle = {{Numerical and Symbolic Scientific Computing: Progress and Prospects}},
language = {english},
pages = {219--256},
publisher = {Springer},
address = {Wien},
isbn_issn = {ISBN 978-3-7091-0793-5},
year = {2011},
editor = {U. Langer and P. Paule},
refereed = {yes},
length = {38}
}

2010

From Program Verification to Automated Debugging

N. Popov, T. Jebelean, B. Buchberger

In: Workshop on Symbolic Computation in Software Science, T. Jebelean and M. Mosbah and N. Popov (ed.), Proceedings of SCSS 2010, pp. 55-65. July 2010. RISC-Linz Report Series, Johannes Kepler University of Linz, Austria, ..
[bib]
@inproceedings{RISC4192,
author = {N. Popov and T. Jebelean and B. Buchberger},
title = {{From Program Verification to Automated Debugging}},
booktitle = {{Workshop on Symbolic Computation in Software Science}},
language = {english},
pages = {55--65},
publisher = {RISC-Linz Report Series},
isbn_issn = {.},
year = {2010},
month = {July},
annote = {2010-07-00-A},
editor = {T. Jebelean and M. Mosbah and N. Popov},
refereed = {yes},
institution = {Johannes Kepler University of Linz, Austria},
length = {11},
conferencename = {SCSS 2010}
}

Proceedings of SCSS 2010 Symbolic Computation in Software Science

T. Jebelean, M. Mosbah, N. Popov (eds.)

Technical report no. 10-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. August 2010. [pdf]
[bib]
@techreport{RISC4191,
author = {T. Jebelean and M. Mosbah and N. Popov (eds.)},
title = {{Proceedings of SCSS 2010 Symbolic Computation in Software Science}},
language = {english},
number = {10-10},
year = {2010},
month = {August},
length = {160},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Projects of Evidence Algorithm and Theorema

A. Anisimov, T. Jebelean, A. Lyaletski, N. Popov

In: Theoretical and Applied Aspects of Program Systems Development, A. Anisimov, V. Redko (ed.), pp. 54-58. October 2010. Kiev, Ukraine, ..
[bib]
@inproceedings{RISC4195,
author = {A. Anisimov and T. Jebelean and A. Lyaletski and N. Popov},
title = {{Projects of Evidence Algorithm and Theorema}},
booktitle = {{Theoretical and Applied Aspects of Program Systems Development}},
language = {russian},
pages = {54--58},
address = {Kiev, Ukraine},
isbn_issn = {.},
year = {2010},
month = {October},
editor = {A. Anisimov and V. Redko},
refereed = {yes},
length = {5}
}

Proving Partial Correctness and Termination of Mutually Recursive Programs

N. Popov, T. Jebelean

In: SYNASC 2010, T. Ida, V. Negru, T. Jebelean, D. Petcu, S. Watt, and, D. Zaharie (ed.), Proceedings of Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 153-158. September 2010. IEEE , ISBN 978-0-7695-4324-6. [pdf]
[bib]
@inproceedings{RISC4287,
author = {N. Popov and T. Jebelean},
title = {{Proving Partial Correctness and Termination of Mutually Recursive Programs}},
booktitle = {{SYNASC 2010}},
language = {english},
pages = {153--158},
publisher = {IEEE },
isbn_issn = {ISBN 978-0-7695-4324-6},
year = {2010},
month = {September},
editor = {T. Ida and V. Negru and T. Jebelean and D. Petcu and S. Watt and and and D. Zaharie},
refereed = {yes},
length = {5},
conferencename = {Symposium on Symbolic and Numeric Algorithms for Scientific Computing}
}

2009

Automated Reasoning

Tudor Jebelean, Bruno Buchberger, Temur Kutsia, Nikolaj Popov, Wolfgang Schreiner, Wolfgang Windsteiger

In: Hagenberg Research, B. Buchberger, M. Affenzeller, A. Ferscha, M. Haller, T. Jebelean, E.P. Klement, P. Paule, G. Pomberger, W. Schreiner, R. Stubenrauch, R. Wagner, G. Weiss, W. Windsteiger (ed.), pp. 63-101. 2009. Springer Dordrecht Heidelberg London New York, ISBN 978-3-642-02126-8. [url]
[bib]
@incollection{RISC3844,
author = {Tudor Jebelean and Bruno Buchberger and Temur Kutsia and Nikolaj Popov and Wolfgang Schreiner and Wolfgang Windsteiger},
title = {{Automated Reasoning}},
booktitle = {{Hagenberg Research}},
language = {english},
pages = {63--101},
publisher = {Springer Dordrecht Heidelberg London New York},
isbn_issn = {ISBN 978-3-642-02126-8},
year = {2009},
annote = {2009-00-00-B},
editor = {B. Buchberger and M. Affenzeller and A. Ferscha and M. Haller and T. Jebelean and E.P. Klement and P. Paule and G. Pomberger and W. Schreiner and R. Stubenrauch and R. Wagner and G. Weiss and W. Windsteiger},
refereed = {no},
length = {39},
url = {http://www.springer.com/computer/programming/book/978-3-642-02126-8}
}

Verification of Mutual Recursive Functional Programs

N. Popov, T. Jebelean

In: Proceedings of Workshop on Symbolic Computation in Software Science SCSS'09, T. Ida, A. Bouhoula (ed.), pp. 120-122. September 2009. Carthage, Tunisia, .. [pdf]
[bib]
@inproceedings{RISC3912,
author = {N. Popov and T. Jebelean},
title = {{Verification of Mutual Recursive Functional Programs}},
booktitle = {{Proceedings of Workshop on Symbolic Computation in Software Science SCSS'09}},
language = {english},
pages = {120--122},
address = {Carthage, Tunisia},
isbn_issn = {.},
year = {2009},
month = {September},
editor = {T. Ida and A. Bouhoula},
refereed = {yes},
length = {15}
}

Functional Program Verification in Theorema. Soundness and Completeness

N. Popov, T. Jebelean

In: Proceedings of 15th Biennial Workshop on Programmiersprachen und Grundlagen der Programmierung KPS'09, J. Knoop, A. Prantl (ed.), pp. 221-229. October 2009. Maria Taferl, Austria, .. [pdf]
[bib]
@inproceedings{RISC3913,
author = {N. Popov and T. Jebelean},
title = {{Functional Program Verification in Theorema. Soundness and Completeness}},
booktitle = {{Proceedings of 15th Biennial Workshop on Programmiersprachen und Grundlagen der Programmierung KPS'09}},
language = {english},
pages = {221--229},
address = {Maria Taferl, Austria},
isbn_issn = {.},
year = {2009},
month = {October},
editor = {J. Knoop and A. Prantl},
refereed = {yes},
length = {9}
}

A Complete Method for Algorithm Validation

N. Popov, T. Jebelean

In: Proceedings of the Workshop on Automated Mathematical Theory Exploration AUTOMATHEO'09, B. Buchberger, R. McCasland, A. Craciun (ed.), pp. 21-25. June 2009. Hagenberg, Austria, -. [pdf]
[bib]
@inproceedings{RISC3915,
author = {N. Popov and T. Jebelean},
title = {{A Complete Method for Algorithm Validation}},
booktitle = {{Proceedings of the Workshop on Automated Mathematical Theory Exploration AUTOMATHEO'09}},
language = {english},
pages = {21--25},
address = {Hagenberg, Austria},
isbn_issn = {-},
year = {2009},
month = {June},
editor = {B. Buchberger and R. McCasland and A. Craciun},
refereed = {yes},
length = {5}
}

2008

A Prototype Environment for Verification of Recursive Programs

N. Popov, T. Jebelean

In: FORMED'08, Z. Istenes (ed.), Proceedings of Formal Methods in Computer Science Education, Budapest, Hungary, ENTCS , pp. 121-130. March 2008. Elsevier, .. [pdf]
[bib]
@inproceedings{RISC3399,
author = {N. Popov and T. Jebelean},
title = {{A Prototype Environment for Verification of Recursive Programs}},
booktitle = {{FORMED'08}},
language = {english},
series = {ENTCS},
pages = {121--130},
publisher = {Elsevier},
isbn_issn = {.},
year = {2008},
month = {March},
editor = {Z. Istenes},
refereed = {yes},
length = {10},
conferencename = {Formal Methods in Computer Science Education, Budapest, Hungary}
}

Functional Program Verification in Theorema

Nikolaj Popov

RISC, Johannes Kepler University. PhD Thesis. July 2008. Technical report no. 08-12 in RISC Report Series. [pdf]
[bib]
@phdthesis{RISC3450,
author = {Nikolaj Popov},
title = {{Functional Program Verification in Theorema}},
language = {english},
year = {2008},
month = {July},
note = {Technical report no. 08-12 in RISC Report Series},
translation = {0},
school = {RISC, Johannes Kepler University},
length = {150}
}

Verification of Functional Programs Containing Nested Recursion

N. Popov, T. Jebelean

In: SCSS'08, B. Buchberger, T. Ida and T. Kutsia (ed.), Proceedings of Austrian-Japan Workshop on Symbolic Computation in Software Science, Hagenberg, Austria, pp. 163-175. July 2008. .. [pdf]
[bib]
@inproceedings{RISC3451,
author = {N. Popov and T. Jebelean},
title = {{Verification of Functional Programs Containing Nested Recursion }},
booktitle = {{SCSS'08}},
language = {english},
pages = {163--175},
isbn_issn = {.},
year = {2008},
month = {July},
editor = {B. Buchberger and T. Ida and T. Kutsia},
refereed = {yes},
length = {13},
conferencename = {Austrian-Japan Workshop on Symbolic Computation in Software Science, Hagenberg, Austria}
}

Loading…