Technical Reports of research area 'Formal Methods'
2018
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, 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
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]
2016
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]
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]
2015
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]
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.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]
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, 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, 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
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]
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]
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]
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]
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.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.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.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.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]
2010
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]
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.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
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]
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]
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.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.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]
Wolfgang Schreiner.The RISC ProofNavigator - Tutorial and Manual. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, July2006.[url][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]
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]
