RISC Algorithm Language (Advisor: Wolfgang Schreiner).
RISCAL (RISC Algorithm Language) is a language and associated software system for formalizing mathematical models and algorithms and automatically checking the formalization over finite domains:
https://www.risc.jku.at/research/formal/software/RISCAL
Your task is to study a particular mathematical/computational problem from literature, to develop a formal model of this problem in the RISCAL language, and to validate this model with the RISCAL software. The model may be the specification of a computational problem by a pair of pre/post-conditions; these may be validated by analyzing the inputs/output pairs allowed by the specification and by checking the correctness of an algorithm with respect to this specification. The model may also describe a computational system by an initial state condition and a transition relation; these may be validated by analyzing the sequences of system states arising from this model. Your goal is to find a way to formalize the model and to validate this formalization that is adequate for the chosen problem.
The validation of the algorithm or system may then be extended to a full verification by providing appropriate invariants from which suitable verification conditions can be automatically generated and checked.
RISCAL (RISC Algorithm Language) is a language and associated software system for formalizing mathematical models and algorithms and automatically checking the formalization over finite domains:
https://www.risc.jku.at/research/formal/software/RISCAL
Your task is to study a particular mathematical/computational problem from literature, to develop a formal model of this problem in the RISCAL language, and to validate this model with the RISCAL software. The model may be the specification of a computational problem by a pair of pre/post-conditions; these may be validated by analyzing the inputs/output pairs allowed by the specification and by checking the correctness of an algorithm with respect to this specification. The model may also describe a computational system by an initial state condition and a transition relation; these may be validated by analyzing the sequences of system states arising from this model. Your goal is to find a way to formalize the model and to validate this formalization that is adequate for the chosen problem.
The validation of the algorithm or system may then be extended to a full verification by providing appropriate invariants from which suitable verification conditions can be automatically generated and checked.
