RISC Publications and Technical Reports of research area 'Formal Methods'
2018
Wolfgang Schreiner, Alexander Brunhuemer, Christoph Fürst.Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models. In: Post-Proceedings ThEdu'17, Pedro Quaresma and Walther Neuper (ed.), Proceedings of 6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science (EPTCS)267, pp. 120-139.2018.Open Publishing Association,ISSN 2075-2180.[doi][pdf][bib]
David M. Cerna and Temur Kutsia.Idempotent Generalization is Infinitary. RISC. Technical report, RISC Report, 2018.[pdf][bib]
Wolfgang Schreiner, Tamás Bérczes, János Sztrik, Hamza Nemouchi.On the Probabilistic Model Checking of Cognitive Radio Networks and Cognitive Infocommunication Systems. Technical report no. 18-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2018.[pdf][bib]
Wolfgang Schreiner, William Steingartner.Visualizing Execution Traces in RISCAL. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, March2018.[pdf][bib]
Wolfgang Schreiner.Validating Mathematical Theories and Algorithms with RISCAL. In: Intelligent Computer Mathematics, F. Rabe, W. Farmer, G. Passmore, A. Youssef (ed.), Proceedings of CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 13-17, 2018, Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence11006, pp. 248-254.2018.Springer,Berlin,ISBN 978-3-319-96811-7.The final authenticated version is available online at Springer.[doi][pdf][bib]
Wolfgang Schreiner, William Steingartner.Visualizing Logic Formula Evaluation in RISCAL. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, July2018.[pdf][bib]
2017
David M. Cerna , Wolfgang Schreiner.Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications. In: Epic series in computer science, Mohamed Mosbah, Michaël Rusinowitch (eds). (ed.), Proceedings of SCSS 2017, 8th International Symposium on Symbolic Computation in Software Science, Epic45, pp. 1-15.April2017.Easy chair,ISSN 2398-7340.[url][pdf][bib]
David Cerna, Alexander Leitsch, Giselle Reis, Simon Wolfsteiner.Ceres in Intuitionistic Logic.Annals of Pure and Applied Logic, pp. 1783-1836.October2017.Elsevier, ISSN 0168-0072.[url][bib]
Besik Dundua, Temur Kutsia, Klaus Reisenberger-Hagmayr.An overview of PρLog. In: Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017, Y. Lierler and W. Taha (ed.), Lecture Notes in Computer Science10137, pp. 34-49.2017.Springer,ISBN 978-3-319-51675-2.[pdf][bib]
Manfred Schmidt-Schauss, Temur Kutsia, Jordy Levy, Mateu Villaret.Nominal Unification of Higher Order Expressions with Recursive Let. In: Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016, M. Hermenegildo and P. Lopez-Garcia (ed.), LNCS10184, pp. 328-344.2017.Springer,ISBN 978-3-319-63138-7.[pdf][bib]
Johannes Blömer, Ilias Kotsireas, Temur Kutsia, Dimitris E. Simos, editors.Mathematical Aspects of Computer and Information Sciences.Lecture Notes in Computer Science10693,2017.Springer,ISBN 978-3-319-72452-2.[doi][bib]
Wolfgang Schreiner.The RISC Algorithm Language - Tutorial and Reference Manual. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, January2017.[pdf][bib]
Manfred Droste, Temur Kutsia, George Rahonis, Wolfgang Schreiner.MK-fuzzy Automata and MSO Logics. In: 8th Symposium on Games, Automata, Logics and Formal Verification (GandALF’17), P. Bouyer, A. Orlandini, P. San Pietro (ed.), Electronic Proceedings in Theoretical Computer Science (EPTCS)256, pp. 106-120.September2017.Rome, Italy, September 22-27,ISSN 2075-2180.[pdf][bib]
Ovidiu Constantin Novac, Tamás Bérczes, Attila Kuki, Ádám Tóth, Wolfgang Schreiner.Modeling RF-Based Sensor Networks by Using Dual-Source Retrial Queueing Systems. In: ICEMES 2017, 14th International Conference on Engineering of Modern Electric Systems, Oradea, Romania, June 1–2, 2017, Mircea Gordan, Teodor Leuca, Florin Constantinescu (ed.), pp. 149-153.2017.IEEE Xplore,ISBN 978-1-5090-6073-3.[doi][bib]
Alexander Brunhuemer.Validating the Formalization of Theories and Algorithms of Discrete Mathematics by the Computer-Supported Checking of Finite Models. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Bachelor Thesis.September2017.[pdf][bib]
2016
Wolfgang Schreiner, David Cerna, Temur Kutsia, Michael Krieger, Bashar Ahmad, Helmut Otto, Martin Rummerstorfer, Thomas Gössl.Practical Event Monitoring in the LogicGuard Framework. In: embedded world Conference 2016, February 23-25 2016, Nürnberg, Germany, Matthias Sturm et al. (ed.), pp. -.February2016.Design & Elektronik,Haar, Germany,ISBN 978-3-645-50159-0.[pdf][bib]
Bashar Ahmad, Michael Krieger.Benchmarks and Performance Analysis of the LogicGuard Framework. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, June2016.[pdf][bib]
David M. Cerna, Wolfgang Schreiner, and Temur Kutsia.Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors. In: SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science, James H. Davenport and Fadoua Ghourabi (ed.), Proceedings of The 7th International Symposium on Symbolic Computation in Software Science, EPiC Series in Computing39, pp. 29-41.2016.EasyChair,ISSN 2040-557X.[url][pdf][bib]
David M. Cerna and Wolfgang Schreiner, Temur Kutsia.Predicting Space Requirements for a Stream Monitor Specification Language. In: Runtime Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30, 2016, Proceedings, Yliès Falcone and César Sánchez (ed.), Proceedings of Runtime Verification, pp. 135-151.September2016.Springer International Publishing,978-3-319-46981-2.[doi][pdf][bib]
Boris Konev, Temur Kutsia.Anti-Unification of Concepts in Description Logic EL. In: Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning, KR 2016, Chitta Baral, James P. Delgrande, Frank Wolter (ed.), pp. 227-236.April 25-292016.AAAI Press,Cape Town, South Africa,978-1-57735-755-1.[url][bib]
Adam Toth, Tamas Berczes, Attila Kuki, Bela Almasi, Wolfgang Schreiner, Jinting Wang, Fang Wang.Analysis of Finite-Source Cluster Networks.Creative Mathematics and Informatics25(2), pp. 223-235.2016.SINUS Association,ISSN 1584 - 286X.[bib]
Temur Kutsia, George Rahonis, Wolfgang Schreiner.MK-fuzzy automata. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, May2016.[pdf][bib]
Daniela Ritirc.Formally Modeling and Analyzing Mathematical Algorithms with Software Specification Languages & Tools. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Master Thesis.January2016.[pdf][bib]
2015
Wolfgang Schreiner, Temur Kutsia, Michael Krieger, Bashar Ahmad, Helmut Otto, Martin Rummerstorfer.Securing Device Communication by Predicate Logic Specifications. In: embedded world Conference 2015, February 24-26 2015, Nürnberg, Germany, Matthias Sturm et al. (ed.), pp. -.February2015.Design&Elektronik,Haar, Germany,ISBN 978-3-645-50144-6.[pdf][bib]
Wolfgang Schreiner, Temur Kutsia, Davic Cerna, Michael Krieger, Bashar Ahmad, Helmut Otto, Martin Rummerstorfer, Thomas Gössl.The LogicGuard Stream Monitor Specification Language Tutorial and Reference Manual. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, October2015.Technical Report.[pdf][bib]
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.Nominal Anti-Unification. RISC. Technical report no. 15-03, April2015.[pdf][bib]
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.Nominal Anti-Unification. In: Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA'15, Maribel Fernandez (ed.), Leibniz International Proceedings in Informatics (LIPIcs), pp. 57-73.2015.ISSN 1868-8969.[pdf][bib]
Alexander Baumgartner.Anti-Unification Algorithms: Design, Analysis, and Implementation. RISC, JKU Linz. PhD Thesis.September2015.[pdf][bib]
Franz Lichtenberger.Making Formal Methods Popular: The Crux is Math Education!. In: Formal Methods in Software Engineering Education Teaching and Training, Andreas Bollin, Tiziana Margaria, Isabelle Perseil (ed.), Proceedings of 1st Workshop on Formal Methods in Software Engeneering Education and Training - FMSEET'15, CEUR Workshop Proceedings1385, pp. 27-34.June2015.Sun SITE Central Europe,RWTH Aachen,ISSN 1613-0073.[url][pdf][bib]
Wolfgang Schreiner, Tamas Berczes, Janos Sztrik, Adam Toth.Modeling RF Communication in Sensor Networks by Probabilistic Model Checking. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report no. 15-21, October2015.[pdf][bib]
Wolfgang Schreiner, Tamas Berczes, Janos Sztrik, Adam Toth.Analyzing Cluster Scheduling Schemes by Probabilistic Model Checking (Addendum). Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, October2015.[pdf][bib]
2014
Wolfgang Schreiner, Temur Kutsia, Michael Krieger, Ahmad Bashar, Helmut Otto, Martin Rummerstorfer.Monitoring Network Traffic by Predicate Logic. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, September2014.[pdf][bib]
Alexander Baumgartner, Temur Kutsia.Unranked Second-Order Anti-Unification. RISC, JKU Linz. Technical report no. 14-05, March2014.[pdf][bib]
Alexander Baumgartner, Temur Kutsia.Unranked Second-Order Anti-Unification. In: Proceedings of the 21st Workshop on Logic, Language, Information and Computation, WoLLIC 2014 , Ulrich Kohlenbach (ed.), Lecture Notes in Computer Science8652, pp. 66- 80.2014.Springer,ISBN 978-3-662-44144-2.[pdf][bib]
Alexander Baumgartner, Temur Kutsia.A Library of Anti-Unification Algorithms. Technical report no. 14-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2014.[url][pdf][bib]
Alexander Baumgartner, Temur Kutsia.A library of anti-unification algorithms. In: Proceedings of the 14th European Conference on Logics in Artificial Intelligence, JELIA 2014, Eduardo Ferme and Joao Leite (ed.), Lecture Notes in Computer Science, pp. 543-557.2014.Springer,ISBN 978-3-319-11557-3.[pdf][bib]
David M. Cerna.A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata. In: Intelligent Computer Mathematics - International Conference, {CICM} 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings, Stephen M. Watt and James H. Davenport and Alan P. Sexton and Petr Sojka and Josef Urban (ed.), Proceedings of CICM, pp. 61-75.2014.10.1007/978-3-319-08434-3\_6.[bib]
Besik Dundua, Mario Florido, Temur Kutsia, Mircea Marin.Constraint Logic Programming for Hedges: A Semantic Reconstruction. In: Proceedings of the Twelfth International Symposium on Functional and Logic Programming, FLOPS 2014, Michael Codish and Eijiro Sumii (ed.), LNCS8475, pp. 285-301.2014.Springer,ISBN 978-3-319-07150-3.[pdf][bib]
Muhammad Taimoor Khan.On the Soundness of the Translation of MiniMaple to Why3ML. Technical report no. 14-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2014.[pdf][bib]
Muhammad Taimoor Khan.Formal Specification and Verification of Computer Algebra Software. 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,April2014.[pdf][bib]
Bashar Ahmad and Michael Krieger.LogicGuard Type System. RISC Software GmbH, Unit Advanced Computing Technologies, Hagenberg, Austria. Technical report, February2014.[pdf][bib]
Temur Kutsia, Jordi Levy, Mateu Villaret.Anti-Unification for Unranked Terms and Hedges. Journal of Automated Reasoning52(2), pp. 155-190.2014.ISSN 0168-7433.[doi][bib]
Temur Kutsia, Christophe Ringeissen.Proceedings of the 28th International Workshop on Unification, UNIF 2014. Technical report no. 14-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2014.[url][pdf][bib]
Temur Kutsia, Wolfgang Schreiner.Verifying the Soundness of Resource Analysis for LogicGuard Monitors (Revised Version) . Technical report no. 14-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2014.[pdf][bib]
Wolfgang Schreiner, Tamas Berczes, Janos Sztrik.Probabilistic Model Checking on HPC Systems for the Performance Analysis of Mobile Networks.Annales Mathematicae et Informaticae43, pp. 123-144.2014.Líceum University Press,ISSN 1787-5021, ISSN 1787-6117.[bib]
Wolfgang Schreiner, Tamas Berczes, Adam Toth.Analyzing Cluster Scheduling Schemes by Probabilistic Model Checking. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, September2014.[pdf][bib]
Wolfgang Schreiner.Some Lessons Learned on Writing Predicate Logic Proofs in Isabelle/Isar. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, October2014.[pdf][bib]
Wolfgang Schreiner, Tamas Berczes, Adam Toth.Analyzing the Energy Efficiency of Cluster Scheduling Schemes by Probabilistic Model Checking. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, December2014.[pdf][bib]
2013
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.A Variant of Higher-Order Anti-Unification. In: Proceedings of the 24th International Conference on Rewriting Techniques and Applications, RTA 2013, Femke van Raamsdonk (ed.), Leibniz International Proceedings in Informatics21, pp. 113-127.2013.ISBN 978-3-939897-53-8, ISSN 1868-8969.[url][bib]
Alexander Baumgartner, Temur Kutsia.Unranked Anti-Unification with Hedge and Context Variables. In: Proceedings of the 27th International Workshop on Unification, UNIF 2013, Barbara Morawska, Konstantin Korovin (ed.), pp. 13-21.2013.[url][bib]
Sandra Alves, Besik Dundua, Mario Florido, Temur Kutsia.A Confluent Pattern Calculus with Hedge Variables. In: Proceedings of the 2nd International Workshop on Confluence, IWC 2013, Nao Hirokawa, Vincent van Oostrom (ed.), pp. 41-45.2013.[url][bib]
Muhammad Taimoor Khan.Translation of MiniMaple to Why3ML. Technical report no. 13-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2013.[pdf][bib]
Muhammad Taimoor Khan.On the Formal Verification of Maple Programs. Technical report no. 13-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2013.[pdf][bib]
Laura Kovacs, Temur Kutsia (ed.).Proceedings of the Fifth International Symposium on Symbolic Computation in Software Science, SCSS 2013. Technical report no. 13-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2013.[pdf][bib]
Janos Sztrik, Wolfgang Schreiner, Tamas Berczes, Gabor Kusper, Nikolaj Popov.Project "85öu8": Final Report - Evaluating Process Algebra Models versus State-oriented Models for the Performance Analysis of Real-time Systems and Software Designs. Technical report no. 13-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2013.[bib]
Wolfgang Schreiner, Tamas Berczes, Janos Sztrik, Gabor Kusper.A Case Study on Exploring the Performance Limits of PRISM. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, September2013.[pdf][bib]
Wolfgang Schreiner.Initial Results on Modeling in PRISM Mobile Cellular Networks with Spectrum Renting. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, April 92013.[pdf][bib]
Wolfgang Schreiner.Experiments with Measuring Time in PRISM 4.0. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, March2013.Technical Report.[pdf][bib]
Wolfgang Schreiner.Experiments with Measuring Time in PRISM 4.0 (Addendum). Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, April2013.[pdf][bib]
Andrii Kryvolap, Mykola Nikitchenko, Wolfgang Schreiner.Program Algebras with Monotone Floyd-Hoare Composition. In: ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer 2013, Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky, Grygoriy Zholtkevych, Mikhail Zavileysky, Hennadiy Kravtsov, Vitaliy Kobets, Vladimir Peschanenko (ed.), Proceedings of ICTERI 2013: 9th International Conference, Kherson, Ukraine, CEUR-WS.org CEUR Workshop Proceedings1000, pp. 533-549.June 19-222013.CEUR-WS.org,ISSN 1613-0073.[pdf][bib]
Wolfgang Schreiner, Nikolaj Popov, Tamas Berczes, Janos Sztrik, Gabor Kusper.Applying High Performance Computing to Analyzing by Probabilistic Model Checking Mobile Cellular Networks with Spectrum Renting. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, July2013.[pdf][bib]
Wolfgang Schreiner and Tamas Berczes and Janos Sztrik.Probabilistic Model Checking on HPC Systems for the Performance Analysis of Mobile Networks. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, September2013.[pdf][bib]
Andrii Kryvolap, Mykola Nikitchenko, Wolfgang Schreiner.Extending Floyd-Hoare Logic for Partial Pre- and Postconditions. In: ICTERI 2013: 9th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer, Kherson, Ukraine, June 19-22, 2013, Revised Selected Papers, Vadim Ermolayev et al (ed.), Communications in Computer and Information Science, pp. 0-23.2013.Springer,Berlin,ISBN 978-3-319-03997-8 (Print) 978-3-319-03998-5 (Online).[pdf][bib]
Temur Kutsia, Wolfgang Schreiner.Verifying the Soundness of Resource Analysis for LogicGuard Monitors, Part 1. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, December 162013.[pdf][bib]
Wolfgang Schreiner, Temur Kutsia.A Resource Analysis for LogicGuard Monitors. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, December 172013.[pdf][bib]
2012
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.A Variant of Higher-Order Anti-Unification. Technical report no. 12-19 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
Sandra Alves, Besik Dundua, Mario Florido, Temur Kutsia.A Dynamic Pattern Calculus with Hedge Variables. Technical report no. 12-20 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
Gabor Guta.Model-to-Text Transformation Modification by Examples. Research Institute for Symbolic Computation. PhD Thesis.2012.[pdf][bib]
Muhammad Taimoor Khan.Formal Semantics of MiniMaple. Technical report no. 12-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).January2012.[pdf][bib]
Muhammad Taimoor Khan.Formal Semantics of a Specification Language for MiniMaple. Technical report no. 12-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2012.[pdf][bib]
Muhammad Taimoor Khan, Wolfgang Schreiner.Towards the Formal Specification and Verification of Maple Programs. 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.July2012.Springer-Verlag,Berlin/Heidelberg,ISBN 978-3-642-31373-8.Awarded with a Best Student Paper Award.[url][pdf][bib]
Muhammad Taimoor Khan, Wolfgang Schreiner.On Formal Specification of Maple Programs. 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. 442-446.July2012.Springer-Verlag,Berlin/Heidelberg,ISBN 978-3-642-31373-8.[url][pdf][bib]
Muhammad Taimoor Khan.On the Formal Semantics of MiniMaple and its Specification Language. In: Proceedings of the 10th International Conference on Frontiers of Information Technology (FIT 2012), xxx (ed.), pp. 00-00.December2012.IEEE Digital Library,xxx.[bib]
Temur Kutsia, Mircea Marin.Solving, Reasoning, and Programming in Common Logic. Technical report no. 12-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
Temur Kutsia, Mircea Marin.Solving, Reasoning, and Programming in Common Logic. In: Proc. 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012, Andrei Voronkov (ed.), pp. 119-126.2012.IEEE Computer Society,ISBN 978-0-7695-4934-7.[pdf][bib]
Temur Kutsia, Mircea Marin.Regular Expression Order-Sorted Unification and Matching. Technical report no. 12-14 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
Temur Kutsia, Wolfgang Schreiner.LogicGuard Abstract Language. Technical report no. 12-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
Wolfgang Schreiner.Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs. 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.February2012.Wroclaw, Poland, July 31, 2011,ISSN: 2075-2180.[doi][bib]
Wolfgang Schreiner.Computability and Complexity. Technical report no. 2012-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2012.Lecture Notes Winter Semester 2012/2013 (last revision: February 4, 2013).[pdf][bib]
Temur Kutsia, Wolfgang Schreiner.Translation Mechanism for the LogicGuard Abstract Language. Technical report no. 12-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
2011
Gabor Guta.A Graph Annotation Based Algorithm for Transducer Modification Inference. Technical report no. 11-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).052011.[pdf][bib]
Muhammad Taimoor Khan.A Type Checker for MiniMaple. Technical report no. 11-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2011.[pdf][bib]
Muhammad Taimoor Khan, Wolfgang Schreiner.Towards a Behavioral Analysis of Computer Algebra Programs (Extended Abstract). In: Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11), Paul Pettersson and Cristina Seceleanu (ed.), pp. 42-44.October2011.Vasteras, Sweden,Doktoratskolleg,Research Institute for Symbolic Computation,ISSN 1404-3041.[pdf][bib]
Muhammad Taimoor Khan.Towards a Behavioral Analysis of Computer Algebra Programs. Technical report no. 11-13 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).November2011.[pdf][bib]
Wolfgang Schreiner.Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs (Extended Abstract). In: THedu'11, CTP Components for Educational Software, Workshop associated to CADE-23, Pedro Quaresma and Ralph-Johan Back (ed.), CISUC Technical Report 2011/001, pp. 55-59.2011.Wroclaw, Poland, July 31,Center for Informatics and Systems, University of Coimbra, Portugal,ISSN 0874-338X.[pdf][bib]
Wolfgang Schreiner.The RISC ProgramExplorer - Tutorial and Manual. Technical report no. 11-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).October2011.[pdf][bib]
Wolfgang Schreiner.Program Reasoning Based on a Relational Semantics of Programs (Extended Abstract). In: Specification and Verification of Hybrid Systems, Proceedings of the First International Seminar, Louis Feraud and Ievgen Ivanov and Mykola Nikitchenko and Martin Strecker (ed.), pp. 64-69.2011.Taras Shevchenko National University of Kyiv and Paul Sabatier University of Tolouse,October 10-12, 2011, Kyiv, Ukraine,ISBN 0000.[bib]
2010
Tamas Berczes, Gabor Guta, Gabor Kusper, Wolfgang Schreiner, Janos Sztrik.Evaluating a Probabilistic Model Checker for Modeling and Analyzing Retrial Queueing Systems .Annales Mathematicae et Informaticae, pp. -.December2010.Liceum University Press,ISSN 1787-5021.[url][bib]
Gabor Guta.Finite State Transducer Modification by Examples. Technical report no. 10-18 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2010.[pdf][bib]
Gabor Guta, Andras Pataricza, Wolfgang Schreiner, Daniel Varro.Semi-Automated Correction of Model-to-Text Transformations. In: Preliminary Proceedings of International Workshop on Models and Evolution (ME 2010), - (ed.), pp. 43-52.2010.-.[url][bib]
Wolfgang Schreiner.The RISC ProgramExplorer: Tutorial and Manual. Technical report no. 10-23 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2010.[pdf][bib]
Wolfgang Schreiner.The RISC ProgramExplorer: Reasoning about Programs as State Relations (Extended Abstract) . In: SCSS 2010, Mohamed Mosbah and Tudor Jebelean (ed.), Proceedings of Symbolic Computation in Software Science, Hagenberg, Austria, July 29-30, pp. -.2010.ISBN XXX-X-XXXXXX-XXX-X.[pdf][bib]
Wolfgang Schreiner.A JML Specification of the Design Pattern "Visitor". Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Technical report, September2010.[pdf][bib]
Gergely Kovasznai.Implementing Design Patterns in AspectJ and JavaMOP. Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Technical report, December2010.[pdf][bib]
Wolfgang Schreiner.From Types to Contracts: Supporting by Light-Weight Specifications the Liskov Substitution Principle. Technical report no. 10-22 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2010.[pdf][bib]
2009
Tudor Jebelean, Bruno Buchberger, Temur Kutsia, Nikolaj Popov, Wolfgang Schreiner, Wolfgang Windsteiger.Automated Reasoning. 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]
Tamás Bérczes, Gábor Guta, Gábor Kusper, Wolfgang Schreiner, János Sztrik.Analyzing a Proxy Cache Server Performance Model with the Probabilistic Model Checker PRISM. In: WWV'09, 5th Int'l Workshop on Automated Specification and Verification of Web Systems, Demis Ballis, Temur Kutsia (ed.), pp. -.July2009.Hagenberg, Austria,-.[pdf][bib]
Gábor Guta, Wolfgang Schreiner, Dirk Draheim.A Lightweight MDSD Process Applied in Small Projects. In: Proc. of 35th EuroMicro Conference, Software Engineering and Advanced Applications (SEEA), - (ed.), pp. -.2009.-.[bib]
Demis Ballis and Temur Kutsia.WWV'09 - Automated Specification and Verification of Web Systems. Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Technical report no. 09-10, July2009.5th Int'l Workshop on Automated Specification and Verification of Web Systems, Castle of Hagenberg, Austria July 17, 2009.[pdf][pdf][bib]
Wolfgang Schreiner.A JML Specification of the Design Pattern "Proxy". Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, April2009.[pdf][bib]
Andreas Müller.VDM - The Vienna Development Method. Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Technical report, April2009.Bachelor thesis in "Formal Methods in Software Engineering".[pdf][bib]
Wolfgang Schreiner.On Proving Assistants in the Classroom (and Elsewhere). In: CADGME 2009, Computer Algebra and Dynamic Geometry Systems in Mathematics Education , Csaba Sarvari et al. (ed.), pp. XX-XX.2009.ISBN XXXXXXXX.RISC, Castle of Hagenberg, Austria, July 11-13, 2009.[pdf][bib]
Gergely Kovasznai.Java Framework Implementing Design Patterns by the Use of JML and Contract4J. Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Technical report, 2009.[pdf][bib]
Wolfgang Schreiner.Supporting the Design Pattern "Object Structures as Plain Values". Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Technical report, September2009.[pdf][bib]
Wolfgang Schreiner.How to Write Postconditions with Multiple Cases. Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Technical report, November2009.[pdf][bib]
2008
Gabor Guta, Barnabas Szasz, Wolfgang Schreiner.A Lightweight Model Driven Development Process based on XML Technology. Technical report no. 08-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).March2008.Draft.[ps][pdf][bib]
Tamas Berczes, Gabor Guta, Gabor Kusper, Wolfgang Schreiner, Janos Sztrik.Analyzing Web Server Performance Models with the Probabilistic Model Checker PRISM. Technical report no. 08-17 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).November2008.[pdf][bib]
Wolfgang Schreiner.The RISC ProofNavigator: A Proving Assistant for Program Verification in the Classroom.Formal Aspects of Computing, pp. -.April2008.Springer,London,ISSN 0934-5043.The original publication is available at www.springerlink.com. DOI 10.1007/s00165-008-0069-4.[doi][pdf][bib]
Markus Stadlbauer.Integration von Entscheidungsprozeduren in einen interaktiven Beweisassistenten. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Diploma Thesis.June2008.[pdf][bib]
Markus Stadlbauer.Integration von Entscheidungsprozeduren in einen interaktiven Beweisassistenten. Technical report no. 08-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria,June2008.[pdf][bib]
Wolfgang Schreiner.Understanding Programs. Research Institute for Symbolic Computation (RISC). Technical report, Johannes Kepler University, Linz, Austria, July2008.[pdf][bib]
Wolfgang Schreiner.A Program Calculus. Research Institute for Symbolic Computation (RISC). Technical report, Johannes Kepler University, Linz, Austria, September2008.[pdf][bib]
2007
Andreas Duscher.A Pattern-based Interaction Language for Mathematical Services. Research Institute for Symbolic Computation (RISC). Technical report, Johannes Kepler University, Linz, Austria, December2007.[pdf][bib]
Tamas Berczes, Gabor Guta, Gabor Kusper, Wolfgang Schreiner, Janos Sztrik.Comparing the Performance Modeling Environment MOSEL and the Probabilistic Model Checker PRISM for Modeling and Analyzing Retrial Queueing Systems. Technical report no. 07-17 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December2007.Project Report.[pdf][bib]
2006
Rebhi Baraka, Wolfgang Schreiner.Querying Registry-Published Mathematical Web Services. In: Proceedings of the IEEE 20th International Conference on Advanced Information Networking and Applications (AINA 2006), Vienna, Austria, Roland Wagner, Jianhua Ma, Arjan Durresi (ed.), pp. 767-772.April 18 - 202006.IEEE Computer Society,Los Alamitos,ISBN-13: 978-0-7695-2466-4.[pdf][bib]
Rebhi Baraka, Wolfgang Schreiner.Semantic Querying of Mathematical Web Service Descriptions. Submitted to the RISC Report Series. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report,April2006.[ps][pdf][bib]
Rebhi Baraka, Wolfgang Schreiner.Semantic Querying of Mathematical Web Service Descriptions. In: Proceedings of the Third International Workshop on Web Services and Formal Methods (WS-FM 2006), Vienna, Austria, M. Bravetti, M. Nunez, and Gianluigi Zavattaro (ed.), Lecture Notes in Computer ScienceLNCS/4184, pp. 73-87.September 8-92006.Springer-Verlag,Berlin Heidelberg,3-540-38862-1.[bib]
Rebhi Baraka.A Framework for Publishing and Discovering Mathematical Web Services. Technical report no. 06-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).August2006.PhD Thesis.[pdf][bib]
Andreas Duscher.An Execution Environment for Mathematical for Services based on WSRF and WS-BPEL. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, March2006.[pdf][bib]
Gabor Guta.Towards error-free software.IT-Business (Hungary)4(38), pp. 26-27.2006.Vogel Burda Communications,ISSN 1589-3464.[bib]
Wolfgang Schreiner.Modellierung und Theorie verteilter Systeme. In: Informatik-Handbuch, Peter Rechenberg, Gustav Pomberger (ed.), Chapter A7, pp. 167-186.2006.Hanser,ISBN 3-446-40185-7.4. Auflage.[bib]
Wolfgang Schreiner.The RISC ProofNavigator - Tutorial and Manual. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, July2006.[url][bib]
Wolfgang Schreiner.Program Verification with the RISC ProofNavigator. In: Teaching Formal Methods: Practice and Experience, David Duce and Paul Boca (ed.), Proceedings of BCS-FACS Christmas Meeting, Electronic Workshops in Computing (eWiC), pp. 1-6.2006.British Computer Society,London, UK, December 15,ISBN.[pdf][bib]
2005
Rebhi Baraka, Wolfgang Schreiner.Querying Registry-Published Mathematical Web Services. Research Institute for Symbolic Computation (RISC). Technical report, Johannes Kepler University, September2005.[pdf][bib]
Rebhi Baraka.Mathematical Services Query Language: Design, Formalization, and Implementation. Research Institute for Symbolic Computation (RISC). Technical report, Johannes Kepler University, September2005.[ps][pdf][bib]
Andreas Duscher.An Execution Environment for Mathematical Services based on WSRF and WS-BPEL. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, December2005.[pdf][bib]
2000
W. Schreiner, C. Mittermaier, F. Winkler.Plotting Algebraic Space Curves by Cluster Computing. In: Computer Mathematics (ASCM 2000), X.-S. Gao and D. Wang (ed.), Proceedings of Proc. of ASCM 2000, pp. 49-58.2000.World Scientific Publishers, Singapore/River Edge,ISBN 9-81024-498-3.[25_paper][bib]
1998
B. Buchberger, T. Ida, W. Schreiner.Knowledge Web: A Design and Feasibilty Study. Institute of Information Sciences and Electronics, University of Tsukuba. Technical report, 1998.ISE-TR-98-151.[bib]
1995
Wolfgang Schreiner.Parallel Functional Programming for Computer Algebra. RISC, Johannes Kepler University Linz. PhD Thesis.1995.[bib]
1985
F. Winkler, B. Buchberger, F. Lichtenberger, H. Rolletschek.Algorithm 628: An Algorithm for Constructing Canonical Bases of Polynomial Ideals.ACM Transactions on Mathematical Software11(1), pp. 66-78.March1985.ACM,no.[pdf][bib]
F. Lichtenberger, B. Buchberger.Mathematik fuer Informatiker: Ein algorithmenorienter Ansatz an der Universitaet Linz (Mathematics for Computer Scientists: An Algorithm Oriented Approach at the University of Linz). In: Special issue: Proceedings of the Symposium "Lehr- und Lernprozesse in der Ingenieurausbildung", Technische Universitaet Graz, Austria, October 8-9, 1985, - (ed.), Zeitschrift fuer Hochschuldidaktik9/10, pp. 103-110.1985.ISBN 3-900386-10-2.[pdf][bib]
1981
B. Buchberger, F. Lichtenberger.Mathematik für Informatik I – Die Methode der Mathematik (Mathematics for Computer Science I – The Method of Mathematics).Second edition,1981.Springer-Verlag, Berlin - Heidelberg - New York,ISBN 3-540-11150-6.[pdf][bib]
1980
Franz Lichtenberger.PL/ADT: Ein System zur Verwendung algebraisch spezifizierter abstrakter Datentypen in PL/I. RISC, Johannes Kepler University Linz. PhD Thesis.1980.[bib]
