|
|
|
|
| Wolfgang Schreiner is an associate professor at the Research Institute for Symbolic Computation (RISC) of the Johannes Kepler University Linz in Austria. His research areas are formal methods; concurrency; and parallel, distributed, and grid computing. Wolfgang Schreiner was born in 1967 in Austria. In 1994, he earned his PhD at the Johannes Kepler University Linz under the auspices of the federal president with a thesis on parallel functional programming for computer algebra. In 2001, he earned habilitation in practical computer science for his work on parallel software and algorithms for symbolic computation. From 2001 to 2004, he was the director of the degree program "Engineering for Computer-based Learning" at the Upper Austria University of Applied Sciences campus Hagenberg, where he still serves as a lecturer. Since 2004, he has been an associate professor at the RISC institute, where he served as vice-chair from 2004 to 2007. During his career, Schreiner has participated in and directed various research projects funded by the Austrian Science Foundation, the Austrian Ministry for Science and Research, and the European Union. These projects include "Distributed Supercomputing in the Grid," "MathBroker I+II: Brokering Distributed Mathematical Services," and "HPGP: High-Performance Generic Programming." He has developed various software systems such as the para-functional language compiler pD, the parallel computer algebra software Distributed Maple, and the proving assistant RISC ProofNavigator. Currently, Schreiner is participating in the doctoral program for computational mathematics at the Johannes Kepler University with a project on formally specified computer algebra software. He is also building the RISC ProgramExplorer, a software environment for program specification, exploration, and verification. --Read our Q&A with Wolfgang Schreiner here. |
|
|
|
Date Reviewed |
|
|
1 - 10 of 12
reviews
|
|
|
|
|
|
|
|
Vitruvius+: an area-efficient RISC-V decoupled vector coprocessor for high performance computing applications Minervini F., Palomar O., Unsal O., Reggiani E., Quiroga J., Marimon J., Rojas C., Figueras R. ACM Transactions on Architecture and Code Optimization 20(2): 1-25, 2023. Type: Article Vector processors had their heyday in the 1980s, before classical supercomputers were mostly replaced by multiprocessors. Today, however, vector processors are experiencing a renaissance: their efficient exploitation of data-level parallelism has ...
|
Aug 2 2023 |
|
|
|
|
|
|
Logic functions and equations: binary models for computer science (2nd ed.) Posthoff C., Steinbach B., Springer International Publishing, New York, NY, 2019. 508 pp. Type: Book (978-3-030024-19-2)
Logic functions, commonly known as Boolean functions, arise in many areas of computer science and information technology. On a fundamental technological level, every digital circuit can be modeled as a Boolean function. Design, optimiz...
|
Aug 6 2019 |
|
|
|
|
|
|
A verified SAT solver framework with learn, forget, restart, and incrementality Blanchette J., Fleury M., Lammich P., Weidenbach C. Journal of Automated Reasoning 61(1-4): 333-365, 2018. Type: Article
SAT solvers are automatic decision procedures for the propositional satisfiability problem; they play an important role in planning, scheduling, optimization, and especially the formal verification of hardware and software systems. Thu...
|
Dec 10 2018 |
|
|
|
|
|
|
Regular language representations in the constructive type theory of Coq Doczkal C., Smolka G. Journal of Automated Reasoning 61(1-4): 521-553, 2018. Type: Article
Theoretical computer science is traditionally presented using paper and pencil, with little emphasis on formal correctness and completeness in detail. This provides a backdoor for ambiguities, gaps, and errors. However, nowadays, power...
|
Aug 16 2018 |
|
|
|
|
|
|
Model checking learning agent systems using Promela with embedded C code and abstraction Kirwan R., Miller A., Porr B. Formal Aspects of Computing 28(6): 1027-1056, 2016. Type: Article
Model checking is a formal method that decides whether a system satisfies a property formulated in temporal logic. While model checking is typically applied to hardware/software systems, it may be used to analyze any system that reache...
|
Mar 29 2017 |
|
|
|
|
|
|
Logics for approximate entailment in ordered universes of discourse Vetterlein T., Esteva F., Godo L. International Journal of Approximate Reasoning 71(C): 50-63, 2016. Type: Article
In many applications, logical reasoning is necessarily approximate in that an entailment “A implies B” only holds to a certain degree c. For such scenarios, a...
|
Jun 15 2016 |
|
|
|
|
|
|
Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics Caleiro C., Marcos J., Volpe M. Theoretical Computer Science 603(C): 84-110, 2015. Type: Article
More and more computer science applications demand the extension of classical logic with its bivalent (two-valued) semantics to “many-valued” logics that provide larger sets of truth values. Among these, the class o...
|
Jan 13 2016 |
|
|
|
|
|
|
Formalizing and reasoning about quality Almagor S., Boker U., Kupferman O. ICALP 2013 (Proceedings of the 40th International Conference on Automata, Languages, and Programming, Riga, Latvia, Jul 8-12, 2013) 15-27, 2013. Type: Proceedings
Traditionally, the goal of formal methods is to determine whether a system satisfies its specification. In other words, the outcome is a yes/no answer. This yields the important practical result of model checkers that verify whether a ...
|
Dec 6 2013 |
|
|
|
|
|
|
Variants of Mersenne twister suitable for graphic processors Saito M., Matsumoto M. ACM Transactions on Mathematical Software 39(2): 1-20, 2013. Type: Article
Generating sequences of pseudorandom numbers is a prerequisite for many applications, such as Monte Carlo simulations. Since such applications are often executed on parallel computers, the parallel computation of pseudorandom numbers i...
|
Jun 5 2013 |
|
|
|
|
|
|
Comparing and analyzing the computational complexity of FCA algorithms Strok F., Neznanov A. SAICSIT 2010 (Proceedings of the 2010 Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists, Bela Bela, South Africa, Oct 11-13, 2010) 417-420, 2010. Type: Proceedings
The development of a semantic Web with data that machines can understand depends crucially on the formal representation of knowledge in suitable ontologies (that is, sets of concepts within certain domains). The goal of formal concept ...
|
Jul 22 2011 |
|
|
|
|
|
|
|
|
|
|
|