## 2008

Luc Rutten, and M.C.J.D. van Eekelen. Efficient and Formally Proven Reduction of Large Integers by Small Moduli. Technical report: ICIS-R08001, February, Radboud University Nijmegen, 2008.

On $w$-bit processors which are much faster at multiplying two $w$-bit integers than at dividing $2w$-bit integers by $w$-bit integers, reductions of large integers by moduli $M$ smaller than $2^{w-1}$ are often implemented sub-optimally, leading applications to take excessive processing time. We present a modular reduction algorithm implementing division by a modulus through multiplication by a reciprocal of that modulus, a well-known method for moduli larger than $2^{w-1}$. We show that application of this method to smaller moduli makes it possible to express certain modular sums and differences without having to compensate for word overflows. By embedding the algorithm in a loop and applying a few transformations to the loop, we obtain an algorithm for reduction of large integers by moduli up to $2^{w-1}$. Implementations of this algorithm can run considerably faster than implementations of similar algorithms that allow for moduli up to $2^w$. This is substantiated by measurements on processors with relatively fast multiplication instructions. It is notoriously hard to specify efficient mathematical algorithms on the level of abstract machine instructions in an error-free manner. In order to eliminate the chance of errors as much as possible, we have created formal correctness proofs of our algorithms, checked by a mechanized proof assistant.

[ PDF ] [ Bibtex ]

T. Heskes, and M.A.J. van Gerven. Stability Conditions for L1/Lp Regularization. Technical report: ICIS-R08002, February, Radboud University Nijmegen, 2008.

This working note derives the stability conditions for L1/Lp regularization.

[ PDF ] [ Bibtex ]

S.J. Overbeek, P. van Bommel, and H.A. (Erik) Proper. Embedding Knowledge Exchange and Cognitive Matchmaking in a Dichotomy of Markets. Technical report: ICIS-R08003, February, 2008.

Actors require knowledge to improve or gain competencies in order to work successfully. Competencies are improved or gained by executing qualifying tasks. A knowledge market paradigm is introduced to improve the fit between supply and demand of knowledge required by actors performing such qualifying tasks. The eventual work performed by actors can be atomically divided into execution tasks. Discrepancies may exist in the suitability match of actors and the execution tasks that have been allocated to them. Therefore, a knowledge workers market paradigm is introduced as a possible solution to improve the fit between actors and execution tasks.

[ Missing PDF ] [ Bibtex ]

Bernard van Gastel, Leonard Lensink, Sjaak Smetsers, and M.C.J.D. van Eekelen. Reentrant Readers-Writers: A Case Study Combining Model Checking and Theorem Proving. Technical report: ICIS-R08005, April, Radboud University Nijmegen, 2008.

The classic readers-writers problem has been extensively studied. This holds to a lesser degree for the reentrant version, where it is allowed to nest locking actions. Such nesting is useful when a library is created with various procedures that each start and end with a lock. Allowing nesting makes it possible for these procedures to call each other. We considered an existing widely used industrial implementation of the reentrant readers-writers problem. We modeled it using a model checker revealing a serious error: a possible deadlock situation. The model was improved and checked satisfactorily for a fixed number of processes. To achieve a correctness result for an arbitrary number of processes the model was converted to a theorem prover with which it was proven.

[ PDF ] [ Bibtex ]

Alejandro Tamalet, Olha Shkaravska, and Marko van Eekelen. A Size-Aware Type System with Algebraic Data Types. Technical report: ICIS-R08006, April, Radboud University Nijmegen, 2008.

We present a size-aware type system for a first-order functional language with algebraic data types, where types are annotated with polynomials over size variables. We define how to generate typing rules for each data type, provided its user defined size function meets certain requirements. As an example, a program for balancing binary trees is type checked. The type system is shown to be sound with respect to the operational semantics in the class of shapely functions. Type checking is shown to be undecidable, however, decidability for a large subset of programs is guaranteed.

[ PDF ] [ Bibtex ]

Peter Achten, Pieter Koopman, and Marco T. MorazÃ¡n. Draft Proceedings of The Ninth Symposium on Trends in Functional Programming (TFP). Technical report: ICIS-R08007, May, Radboud University Nijmegen, 2008.

Draft proceedings TFP 2008.

[ PDF ] [ Bibtex ]

Pieter Koopman, Rinus Plasmeijer, and Doaitse Swierstra. Draft Proceedings of the Sixth Advanced Functional Programming school (AFP 2008). Technical report: ICIS-R08008, May, Radboud University Nijmegen, 2008.

Draft proceedings of AFP 2008.

[ PDF ] [ Bibtex ]

M.A.J. van Gerven, and T. Heskes. L1/Lp regularization of Differences. Technical report: ICIS-R08009, May, Radboud University Nijmegen, 2008.

In this paper, we introduce $L_1/L_p$ regularization of differences as a new regularization approach that can directly regularize models such as the naive Bayes classifier and (autoregressive) hidden Markov models. An algorithm is developed that selects values of the regularization parameter based on a derived stability condition. for the regularized naive Bayes classifier, we show that the method performs comparably to a filtering algorithm based on mutual information for eight datasets that have been selected from the UCI machine learning repository.

[ PDF ] [ Bibtex ]

H. Tews, Tjark Weber, E. Poll, and M.C.J.D. van Eekelen. Formal Nova interface specification. Technical report: ICIS-R08011, May, 2008, Robin deliverable D12.

This document contains one major result of work package 4 (kernel specification and verification): a formal specification of the Nova interface. The specification consists of three main parts: (1) a definition of an abstract internal state for the Nova micro-hypervisor, (2) a description of the operations of the hypervisor in imperative pseudo-code that accesses and modifies the internal state, and (3) a combination of big-step denotational and small-step operational semantics to give semantics to the pseudo code as state modifying functions.

[ PDF ] [ Bibtex ]

Hendrik Tews, Tjark Weber, Marcus VÃ¶lp, Erik Poll, M.C.J.D. van Eekelen, and Peter van Rossum. Nova Micro-Hypervisor Verification. Technical report: ICIS-R08012, May, Radboud University Nijmegen, 2008, Robin deliverable D13.

In this document we describe the work performed in the Robin project towards verifying the Nova micro-hypervisor operating-system kernel. In particular, we describe in detail the Robin verification environment and the results obtained with it. The Robin verification environment consists of the interactive theorem prover PVS, an IA32 (x86) hardware model in PVS, a semantics of (a rich subset of) C++, and a semantics compiler translating C++ sources into their semantics in PVS.

[ PDF ] [ Bibtex ]

Marieke Huisman, and Erik Poll. Formal Techniques for Java-like Pograms (FTfJP08). Technical report: ICIS-R08013, June, Radboud University Nijmegen, 2008.

This report contains the papers presented at FTfJP08: the 10th workshop on Formal Techniques for Java-like Programs held on July 8th, 2008 in Paphos, Cyprus. This workshop is the tenth in a series of workshops aimed at applying formal techniques to improve modern object-oriented languages. Newer languages such as Java and C# provide good platforms to bridge the gap between formal techniques and practical program development, because of their reasonably clear semantics and standardized libraries. It is our hope that this workshop will encourage the further deployment of well-considered formal techniques.

[ PDF ] [ Bibtex ]

Christian Haack, Marieke Huisman, and Clement Hurlin. Reasoning about Javas Reentrant Locks. Technical report: ICIS-R08014, July, Radboud University Nijmegen, 2008.

This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permission-accounting separation logic. As usual, each lock is associated with a resource invariant, when acquiring the lock the resources are obtained by the thread holding the lock, and when releasing the lock, the resources are released. To accommodate for reentrancy, the notion of lockset is introduced: a multiset of locks held by a thread. Keeping track of the lockset enables the logic to ensure that resources are not re-acquired upon reentrancy, thus avoiding the introduction of new resources in the system. To be able to express flexible locking policies, we combine the verification logic with value-parametrized classes. Verified programs satisfy the following properties: data race freedom, absence of null-dereferencing and partial correctness. The verification technique is illustrated on several examples, including a challenging lock-coupling algorithm.

[ PDF ] [ Bibtex ]

J. Nabukenya, P. van Bommel, and H.A. (Erik) Proper. A Theory-Driven Design Approach to Collaborative Policy Making Processes. Technical report: ICIS-R08015, July, Radboud University Nijmegen, 2008.

In this paper, we consider improving collaborative policy making processes. We suggest Collaboration Engineering (CE) as an approach that can be useful in enhancing these processes. However, CE needs a theoretical basis to guide the design. This basis is provided by the quality dimensions and the causal theory. We therefore present a theory that provides an understanding of what makes good policies in policy making. This understanding should lead to design choices that should be taken into account to design quality collaborative policy making processes. To determine the quality dimensions of good policies, we use field exploratory studies and literature in the policy making domain research. Furthermore, we consider cause and effect relationships for these quality dimensions to derive the theory.

[ PDF ] [ Bibtex ]

Cezary Kaliszyk, Femke van Raamsdonk, Freek Wiedijk, Hanno Wupper, Maxim Hendriks, and Roel de Vrijer. Deduction using the ProofWeb system. Technical report: ICIS-R08016, September, Radboud University Nijmegen, 2008.

This is the manual of the ProofWeb system that was implemented at the Radboud University Nijmegen and the Free University Amsterdam in the SURF education innovation project Web deduction for education in formal thinking.

[ PDF ] [ Bibtex ]

Rinus Plasmeijer, Sjaak Smetsers, and Arjen van Weelden. Interactive Combining of Typed Object Code. Technical report: ICIS-R08019, November, Radboud University Nijmegen, 2008.

The functional language Clean includes a hybrid type system: in addition to the traditional static type system it offers support for dynamically typed values, so called \emph{dynamics}. An expression of arbitrary static type can be packed into a dynamic, and via pattern matching on types a dynamic can be converted back to a value of statically known type. The most important aspect of dynamics is that they can be serialized, written to file, and exchanged between independently compiled applications in a type-safe way. Since dynamics may contain functions and closures, they can be regarded as type-safe plugins. An application can combine plugins in a type safe way to new ones, without having to know what the actual contents and types of the original plugins are. In this paper we explain the underlying implementation and the architecture of the run-time system needed to make this all possible. To show the expressive power of Clean`s dynamics we present an interactive shell, called Esther. The command line language of this shell provides the basic functionality of a strongly typed lazy functional language. Esther behaves like an interpreter (direct response) yet its resulting performance is comparable to compiled code. This is achieved by using the dynamic facility of Clean. The shell actually combines compiled code; no help from a compiler is needed. Moreover, type checking is for free using the run-time type unification of dynamics. In this way we have obtained a novel architectural framework in which one can freely mix functionality created by the compiler, functionality stored in dynamics by compiled applications, and functionality interactively created by using the shell command line interpreter.

[ PDF ] [ Bibtex ]

O. Shkaravska, M. van Eekelen, and A. Tamalet. Polynomial Size Complexity Analysis with Families of Piecewise Polynomials (with soundness proof and examples in detail). Technical report: ICIS-R08020, November, Radboud University Nijmegen, 2008.

Size analysis can play an important role in optimising memory management and in preventing failure due to memory exhaustion. Static size analysis can be performed using size-aware type systems. In size-aware type systems types express output-on-input size dependencies where sizes of outputs depend on sizes of inputs but they do not depend directly on the actual values. We present a novel type system for a strict functional language. We introduce size annotations that are indexed families of piecewise polynomials. Families are de?ned using indices. They collect possible different size dependencies of a single function. With families compositionality becomes straightforward, even for non-monotonic size dependencies. Lower and upper size bounds can be expressed in a natural way as members of the family. Furthermore, families make it possible to allow non matrix-like structures where inner lists have different lengths. The type system is proven to be sound with respect to a standard operational semantics. Type checking in our type system is not fully decidable. However, we identify two large decidable subclasses. Moreover, the type system admits a semi-automatic inference procedure.

[ PDF ] [ Bibtex ]

O. Shkaravska, M. van Eekelen, and A. Tamalet. Collected Size Semantics for Functional Programs over Lists. Technical report: ICIS-R08021, November, 2008.

This work introduces collected size semantics of strict functional programs over lists. The collected size semantics of a function definition is a multivalued size function that collects the dependencies between every possible output size and the corresponding input sizes. Such functions annotate standard types and are defined by conditional rewriting rules generated during type inference. We focus on the connection between the rewriting rules and lower and upper bounds on the multivalued size functions, when the bounds are given by piecewise polynomials. We show how, given a set of conditional rewriting rules, one can infer bounds that define an indexed family of polynomials that approximates the multivalued size function. Using collected size semantics we are able to infer non-monotonic and non-linear lower and upper polynomial bounds for many functional programs. As a feasibility study, we use the procedure to infer lower and upper polynomial size-bounds on typical functions of a list library.

[ PDF ] [ Bibtex ]

Sjaak Smetsers, and Erik Barendsen. Formalizing Type Theory in PVS: a case study. Technical report: ICIS-R08022, December, Radboud University Nijmegen, 2008.

In this case study we investigate the use of PVS for developing type theoretical concepts and verifying the correctness of a typing algorithm. PVS turns out to be very useful for efficient development of a sound basic theory about polymorphic typing. This research contributes to the PoplMark challenge on mechanizing metatheory

[ PDF ] [ Bibtex ]

Peter Achten, Marko van Eekelen, Maarten de Mol, and Rinus Plasmeijer. A Common Arrow Based Semantics for GEC and iData Applications. Technical report: ICIS-R08023, December, Radboud University Nijmegen, 2008.

State-based interactive applications, whether they run on the desktop or as a web application, can be considered as collections of interconnected editors of structured values that allow users to manipulate data. This is the view that is advocated by the GEC and iData toolkits, which offer a high level of abstraction to programming desktop and web GUI applications respectively. Special features of these toolkits are that editors have shared, persistent state, and that they handle events individually. In this paper we cast these toolkits within the Arrow framework and present a single, uniÃ‚Â¯ed semantic model that defines shared state and event handling. We study the properties of this EditorArrow model, and of editors in particular. Furthermore, we present the definedness properties of the combinators. A reference implementation of the EditorArrow model is given with some small program examples. We discuss formal reasoning about the model using the proof assistant Sparkle.

[ PDF ] [ Bibtex ]