[All BiBTeX entries for this year]

J.G. Beney, N. Gietema, and C.H.A. Koster. * Strength Normalisation and Weight Initialisation for Winnow Algorithm. *Technical report, University of Nijmegen, 2000, To appear..

[ Missing PDF ] [ Bibtex ]

F.W. Vaandrager. * Quality of Software - Formal Methods and Tools. *Technical report: CSI-N0001, March, Radboud University Nijmegen, 2000.

[ Missing PDF ] [ Bibtex ]

J. Simons, A.T. Arampatzis, B.C.M. Wondergem, L.R.B. Schomaker, P. van Bommel, E.C.M. Hoenkamp, Th.P. van der Weide, and C.H.A. Koster. * PROFILE - A Multi-Disciplinary Approach to Information Discovery. *Technical report: CSI-R0001, January, Radboud University Nijmegen, 2000.

This document describes the Profile project, a multi-disciplinary project aiming at the development of a proactive information filter for dynamic information environments. The goal of this paper is threefold. First, the suitability of an agent-based architecture for the Profile project is evaluated. Second, this article provides an overview of the research done in the Profile project. Third, it describes the integration of this research, which has led to the implementation of a prototype. The architecture and workings of the prototype are illustrated.

[ Missing PDF ] [ Bibtex ]

A. Fehnker. * Bounding and heuristics in forward reachability algorithms. *Technical report: CSI-R0002, February, Radboud University Nijmegen, 2000.

Recently timed automata models have been used to solve realistic scheduling problems. In this paper we want to establish the relation between timed automata and job shop scheduling problems. The timed automata models of the scheduling problems can serve as input for a forward reachability checker. In contrast to job shop algorithms theforward reachability algorithms will usually not yield an optimalsolution. There are also only few ways to direct the exploration of the state space. Starting from job shop problem we will describe how forward reachability can be equipped with two concepts from branch and bound methods: heuristics and bounding. This extended algorithm is then applicable to all kinds of timed automata models.

P.M. Achten, and M. Wierich. * A Tutorial to the CLEAN Object I/O Library. *Technical report: CSI-R0003, February, Radboud University Nijmegen, 2000.

M. Huisman, and B.P.F. Jacobs. * Inheritance in Higher Order Logic: Modeling and Reasoning. *Technical report: CSI-R0004, February, Radboud University Nijmegen, 2000.

This paper describes a way of modeling inheritance(in object-oriented programming languages) in higher order logic. This particular approach is used in the LOOP project forreasoning about Java classes, with the proof tools PVS andISABELLE. It relies on nested interface types to capturethe superclasses, fields, methods, and constructors of classes, together with suitable casting functions incorporating the difference between hiding of fields and overriding of methods. This leads to the proper handling of late binding, as illustrated in several examples.

E. Poll, J.A.G.M. van den Berg, and B.P.F. Jacobs. * Specification of the JavaCard API in JML. *Technical report: CSI-R0005, March, Radboud University Nijmegen, 2000.

This paper reports on an effort to increase the reliabilityof JavaCard-based smart cards by means of formal specification and verification of JavaCard source code.As a first step, lightweight formal interface specifications,written in the specification language JML, have been developed for all the classes in the JavaCard API (version 2.1). They make many of the implicit assumptionsunderlying the current implementation explicit, and thusfacilitate the use of this API and increase the reliability of the code that is based on it. Furthermore, the formal specifications are amenable to tool support, for verificationpurposes.

M. Huisman, B.P.F. Jacobs, and J.A.G.M. van den Berg. * A Case Study in Class Library Verification: Java's Vector Class. *Technical report: CSI-R0007, March, Radboud University Nijmegen, 2000.

This paper presents a verification of an invariant property for the Vector class from Java's standard library (API). The property says (essentially) that the actual size of a vector is less than or equal to its capacity. It is shown that this �safety'' or �data integrity'' property is maintained by all methods of the Vector class, and that it holds for all objects created by the constructors of the Vector class. The verification of the Vector class invariant is done with the proof tool PVS. It is based on a semantics of Java in higher order logic. The latter is incorporated in a special purposecompiler, the LOOP tool, which translates Java classes intological theories. It has been applied to the Vector class for this case study.The actual verification takes into account the object-orientedcharacter of Java: (non-final) methods may always beoverridden, so that one cannot rely on a particular implementation. Instead, one has to reason from method specifications in such cases.This project demonstrates the feasibility of tool-assisted verification of non-trivial properties for non-trivial Java classes.

[ Missing PDF ] [ Bibtex ]

H. Wupper, and H. Meijer. * Wat is informatica eigenlijk?. *Technical report: CSI-R0008, March, Radboud University Nijmegen, 2000.

Begripsverwarring op het gebied van de informatie- en communicatietechnologie leidt ertoe dat beslissers hoofd- en bijzaken door elkaar halen en daardoor niet goed weten welke rol de informatica in onze maatschappij moet spelen. Dit artikel analyseert waar het eigenlijk om gaat zonder in te gaan op bijzaken en de waan van de dag.Het bespreekt wat er komt kijken bij het professioneel ontwikkelen van ICT-systemen. Het geeft de belangrijkste aspecten en hun relaties weer in een diagram. Het stelt tevens een consistente terminologie voor. De problemen waar het vooral om gaat zijn die van de geschiktheid en de complexiteit van de systemen. Het is de taak van wetenschappelijk onderzoek de ontwikkeling te ondersteunen met theorie�n, talen, methoden en gereedschappen.Een maatschappij die geen technologische achterstand wil oplopen, heeft beide kanten van de in formatica nodig: een ingenieursdiscipline met een gedegen opleiding en een exacte wetenschap die voor deze ingenieursdiscipline het nodige fundament ontwikkelt.

[ Missing PDF ] [ Bibtex ]

D.P.L. Simons, and M.I.A. Stoelinga. * Mechanical Verification of the IEEE 1394aRoot Contention Protocol using Uppaal2k. *Technical report: CSI-R0009, May, Radboud University Nijmegen, 2000.

This paper reports a mechanical verification of the IEEE 1394 root contention protocol. This is an industrial leader election protocol, in which timing parameters play an essential role.In this case study, we used the Uppaal2k tool and stepwise verification to investigate the timing constraints on the parameters which are necessary and sufficient for correct protocol operation. A manual verification of this protocol using I/O automata has been published in [19]. We improve the communication model from that paper andby analyzing large numbers of protocol instances with Uppaal, we derive the required timing constraints.

[ Missing PDF ] [ Bibtex ]

D.C. van Leijenhorst. * ""Symmetric functions, Latin Squares. *Technical report: CSI-R0011, June, Radboud University Nijmegen, 2000.

We shall present a complete, elementary derivation of MacMahon's beautiful formula for the number of Latin squares of order n. Part of the proof, dealing with the combinatorial theory of Hammond differential operators, follows the lines of an ancient ""Scriptum"" by Van der Corput. Some implementation issues in Maple will be discussed briefly.

[ Missing PDF ] [ Bibtex ]

D.C. van Leijenhorst. * Some Software For Symmetric Functions . *Technical report: CSI-R0012, June, Radboud University Nijmegen, 2000.

Some Maple software is presented that was used in a study of the symmetric functions: in particular, MacMahon's method of counting Latin squares, anditerative behavior. Some background of various algorithms has been provided as well.

[ Missing PDF ] [ Bibtex ]

W.O.D. Griffioen, and F.W. Vaandrager. * A Theory of Normed Simulations. *Technical report: CSI-R0013, July, Radboud University Nijmegen, 2000.

In existing simulation proof techniques, a single step in a lower-level specification may be simulated by an extended execution fragment in a higher-level one.As a result, it is cumbersome to mechanize these techniques using general purpose theorem provers.Moreover, it is undecidable whether a given relation is a simulation, even if tautology checking is decidable for the underlying specification logic.This paper introduces various types of normed simulations.In a normed simulation, each step in a lower-level specification can be simulated by at most one step in the higher-level one, for any related pair of states.We show that, under some reasonable assumptions, it is decidable whether a given relation is a normed forward simulation, provided tautology checking is decidable for the underlying logic.We also prove that, at the semantic level, normed forward and backward simulations together form a complete proof method for establishing behavior inclusion, provided that the higher-level specification has finite invisible nondeterminism.Apart from their pleasant theoretical properties, normed simulations also have turned out to be quite useful as a vehicle for the formalization of refinement proofs via theorem provers.

J.A.G.M. van den Berg, B.P.F. Jacobs, and E. Poll. * Formal Specification and Verification of JavaCard's Application Identifier Class. *Technical report: CSI-R0014, September, Radboud University Nijmegen, 2000.

This note discusses a verification in PVS of the AID(Application Identifier) class from JavaCard's API. The properties that are verified are formulated in the interface specification language JML. This language is also used to express the properties that are assumed about the native methods from the Util class that are used in the AID class.

[ Missing PDF ] [ Bibtex ]

B.P.F. Jacobs. * A Formalisation of Java's Exception Mechanism. *Technical report: CSI-R0015, October, Radboud University Nijmegen, 2000.

This paper examines Java's exception mechanism, and formalises its main operations (throw, try-catch and try-catch-finally) in a type-theoretic settting. This formalisation uses coalgebras for modeling statements and expressions, thus providing a convenient setting for handling the various termination options that may arise in exception handling (closely following the Java Language Specification). This semantics of exceptions is used within the LOOP project on Java program verification. It is illustrated in two example verifications in PVS.

[ Missing PDF ] [ Bibtex ]

E. Poll, J.A.G.M. van den Berg, and B.P.F. Jacobs. * Formal Specification of the JavaCard API in JML: the APDU class. *Technical report: CSI-R0016, October, Radboud University Nijmegen, 2000.

This paper reports on an effort to increase the reliabilityof JavaCard-based smart cards by means of formal specification and verification of \mbox{JavaCard} source code. As a first step, formal interface specifications,written in the specification language JML, have been developed for all the classes that make up the JavaCard API. These specifications are ``lightweight'' in the sense that they are incomplete and specify only some aspects of the API, but they already provide a useful addition to the existing informal API specifications. Moreover, the fact that these specification are written in a formal language makes them amenable to tool support, for verificationpurposes. As an illustration, the JML specifications of the APDU (Application Protocol Data Unit) class in the JavaCard API are discussed in detail.

[ Missing PDF ] [ Bibtex ]

A.L. de Groot, and J.J.M. Hooman. * Analyzing the Light Control System with PVS. *Technical report: CSI-R0017, November, Radboud University Nijmegen, 2000.

The interactive theorem prover PVS is used to formalize the user needs of the Light Control system. The Light Control System is meant to control the room lighting in an office building. We handle a simplified system that controls the lighting in a single room. First the system is modeled at a high level of abstraction, in terms of properties the user can observe. After resolving ambiguities and conflicts, a refinement is defined, using dimmable light actuators. The dimmable light actuator is a model of ""real"" lights with ideal behavior. Correctness of the refinement has been proved in PVS, under the assumption that there are no internal delays. Next these internal delays are taken into account, leading to a new notion of delay-refinement which allows abstraction from delays such that systems with delays can be seen as an approximation of an undelayed specification.

[ Missing PDF ] [ Bibtex ]

B.P.F. Jacobs, and E. Poll. * A Logic for the Java Modeling Language JML. *Technical report: CSI-R0018, November, Radboud University Nijmegen, 2000.

This paper describes a specialised logic for proving specifications in the Java Modeling Language (JML). JML is an interface specification language for Java. It allows assertions like invariants, constraints, pre- and post-conditions, and modifiable clauses as annotations to Java classes, in a design-by-contract style. Within the LOOP project at the University of Nijmegen JML is used for specification and verification of Java programs. A special compiler has been developed which translates Java classes together with their JML annotations into logical theories for a theorem prover (PVS or Isabelle). The logic for JML that will be described here consists of tailor-made proof rules in the higher order logic of the back-endtheorem prover for verifying translated JML specifications. The rules efficiently combine partial and total correctness (like in Hoare logic) for all possible termination modes in Java, in a single correctness formula.

[ Missing PDF ] [ Bibtex ]

J.A.G.M. van den Berg, and B.P.F. Jacobs. * The LOOP compiler for Java and JML. *Technical report: CSI-R0019, December, Radboud University Nijmegen, 2000.

This paper describes the architecture of the LOOP tool, which is used for reasoning about sequential Java. The LOOP tool translates Java and JML (a specification language tailored to Java) classes into their semantics in higher order logic. It serves as a front-end to a theorem prover in which the actual verification of the desired properties takes place. Also, the paper discusses issues related to logical theory generation.

[ Missing PDF ] [ Bibtex ]

B.P.F. Jacobs. * Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study. *Technical report: CSI-R0020, December, Radboud University Nijmegen, 2000.

This paper gives a semantical underpinning for a many-sorted modal logic associated with certain dynamical systems, like transition systems, automata or classes in object-oriented languages. These systems will be described as coalgebras of so-called polynomial functors, built up from constants and identities, using products, coproducts and powersets. The semantical account involves Booleanalgebras with operators indexed by polynomial functors, called MBAOs, for Many-sorted Boolean Algebras with Operators, combining standard (categorical) models of modal logic and of many-sorted predicate logic. In this setting we will see Lindenbaum MBAO models as initial objects, and canonical coalgebraic models of maximallyconsistent sets of formulas as final objects. They will be used to (re)prove completeness results, and Hennessey-Milner style characterisation results for the modal logic, first established byR��iger.

[ Missing PDF ] [ Bibtex ]