Marko van Eekelen, Rachid Ben Moussa, Engelbert Hubbers, and Roel Verdult. Blackboard Security Assessment. Technical report: ICIS-R13004, April, Radboud University Nijmegen, 2013.
A security assessment is given of the BlackBoard Learn electronic learning environment. As a result of this assessment the board of the Radboud University Nijmegen has decided to stop with summative testing using BlackBoard, to quit using Blackboard Grade Center and to use the Blackboard discussion forum for non-privacy-sensitive topics only.
Ken Madlener, Sjaak Smetsers, and Marko van Eekelen. Modular Bialgebraic Semantics and Algebraic Laws. Technical report: ICIS-R13008, July, Radboud University Nijmegen, 2013.
The ability to independently describe operational rules is indispensable for a modular description of programming languages. This paper introduces a format for open-ended rules and proves that conservatively adding new rules results in well-behaved translations between the models of the operational semantics. Silent transitions in our operational model are truly unobservable, which enables one to prove the validity of algebraic laws between programs. We also show that algebraic laws are preserved by extensions of the language and that they are substitutive. The work presented in this paper is developed within the framework of bialgebraic semantics.
Paolo Parisen Toldin, Rody Kersten, Bernard van Gastel, and Marko van Eekelen. Soundness Proof for a Hoare Logic for Energy Consumption Analysis. Technical report: ICIS-R13009, October, Radboud University Nijmegen, 2013.
Energy inefficient software implementations may cause battery drain for small systems and high energy costs for large systems. Dynamic energy analysis is often applied to mitigate these issues. However, this is often hardware-specific and requires repetitive measurements using special equipment. We present a static analysis deriving upper-bounds for energy consumption based on an introduced energy-aware Hoare logic. Software is considered together with models of the hardware it controls. The Hoare logic is parametric with respect to the hardware. Energy models of hardware components can be specified separately from the logic. Parametrised with one or more of such component models, the analysis can statically produce a sound (over-approximated) upper-bound for the energy-usage of the hardware controlled by the software.