From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=BAYES_00, PP_MIME_FAKE_ASCII_TEXT autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII X-Google-Thread: 106582,1eecf40e3bdf7a8d,start X-Google-Attributes: gid106582,public X-Google-Thread: f8362,1eecf40e3bdf7a8d,start X-Google-Attributes: gidf8362,public X-Google-Thread: 103376,1eecf40e3bdf7a8d,start X-Google-Attributes: gid103376,public X-Google-Thread: 115aec,1eecf40e3bdf7a8d,start X-Google-Attributes: gid115aec,public X-Google-Thread: f7888,1eecf40e3bdf7a8d,start X-Google-Attributes: gidf7888,public X-Google-Thread: 101ec5,1eecf40e3bdf7a8d,start X-Google-Attributes: gid101ec5,public X-Google-Thread: f43e6,1eecf40e3bdf7a8d,start X-Google-Attributes: gidf43e6,public From: matkin@Owein.docs.uu.se (Matz Kindahl) Subject: Call For Registration - FTRTFT'96 Date: 1996/06/17 Message-ID: X-Deja-AN: 160624998 distribution: world organization: DoCS, Uppsala University followup-to: comp.theory newsgroups: comp.theory,comp.specification.z,comp.specification.larch,comp.specification.misc,comp.software-eng,comp.realtime,comp.lang.ada Date: 1996-06-17T00:00:00+00:00 List-Id: FTRTFT'96 4th International School and Symposium Formal Techniques in Real Time and Fault Tolerant Systems Sept 9-10 (School) and Sept 11-13 (Symposium) 1996, Uppsala, Sweden PROGRAMME and CALL FOR REGISTRATION OBJECTIVES Computer systems are becoming increasingly widespread in real-time and safety-critical applications. Such systems are characterized by the crucial need to manage their complexity in order to produce reliable designs. Formal techniques offer a foundation for systematic design of complex systems. They have beneficial applications throughout the engineering process, from the capture of requirements through specification, design, coding and compilation, down to the hardware which embeds the system into its environment. Their use may presuppose novel system architectures and design principles. The school and symposium are devoted to considering the problems and the solutions in safe system design, and to examining how well the use of advanced design techniques and formal methods for design, analysis and verification serves in relating theory to practical realities. This is the fourth in a line of International Schools and Symposia, previous were held at Warwick 1989, at Nijmegen 1992, and at L�beck 1994. Proceedings of these symposia are published as volumes 331, 571, and 863 in the LNCS series by Springer Verlag. PROGRAM COMMITTEE A. Burns (Univ. of York, UK), C. Dwork (IBM Almaden, USA), T. Henzinger (Cornell Univ., Ithaca, N.Y., USA), J. Hooman (Eindhoven Univ. of Technology), B. Jonsson (co-chair) (Uppsala Univ., SE), M. Joseph (Univ. of Warwick, UK), B. Kurshan (AT&T/Bell Labs, New Jersey, USA), K. Larsen (Aalborg Univ., DK), N. Leveson (Univ. of Washington, USA), A. Mok (Univ. of Texas, Austin, USA), E.R. Olderog (Univ. of Oldenburg, USA), J. Parrow (co-chair) (Royal Inst. of Technology, Stockholm, SE), Z. Peng (Link�ping University, SE) A. Pnueli (Weizmann Inst., Rehovot, IL), A.P. Ravn (DTU, Lyngby, DK), W.-P. de Roever (Univ. of Kiel, DE), F. Schneider (Cornell Univ., Ithaca, N.Y., USA), J. Sifakis (IMAG-LGI, Grenoble, FR), J. Torin (Chalmers Univ. of Technology, SE), J. Vytopil (Kath. Univ., Nijmegen, NL) K.-E. �rz�n (Lund Univ. of Technology, SE) ORGANIZING COMMITTEE Parosh Abdulla: Publicity Per Gunningberg: Local Organization Hans Hansson: Sponsorship Wang Yi: Tools Demonstrations STEERING COMMITTEE M. Joseph (Univ. of Warwick, UK), A. Pnueli (Weizmann Inst., Rehovot, IL), H. Rischel (DTU, Lyngby, DK), W.-P. de Roever (Univ. of Kiel, DE), J. Vytopil (Kath. Univ., Nijmegen, NL) SPEAKERS AT SCHOOL (Sept 9-10) A. Burns (Univ. of York, UK), K. Larsen (Aalborg Univ., DK), E.R. Olderog (Univ. of Oldenburg, DE), D. Powell (LAAS-CNRS, FR), K. Tindell (Northern Real-Time Technologies, UK), Presentations by commercial companies will be given by speakers from: Praxis (UK), NP Logikkonsult (SE) INVITED SPEAKERS AT SYMPOSIUM (Sept 11-13) F. Cristian (UCSD, San Diego, USA), G. Holzmann (AT&T, USA), A. Pnueli (Weizmann Inst., IL), N. Shankar (SRI International, USA), P. Zave (AT&T, USA) TOOLS DEMONSTRATIONS Demonstrations of software tools that support formal approaches to the development of distributed and/or embedded systems are invited for the school and symposium. Proposers should contact the Tools Demonstration at address: Wang Yi, Uppsala University, Dept. of Computer Systems, Box 325, S-751 05 Uppsala, Sweden. E-mail: yi@docs.uu.se FOR MORE INFORMATION http://www.docs.uu.se/ftrtft96/ ---------------------------------------------------------------------- PROGRAMME AT SCHOOL, SEPT 8-10 Sunday, September 8 19:00- Reception, Polacksbacken Monday, September 9 08:00- Registration 08:50-08:00 Welcome Tutorials 09:00-10:30 Scheduling in Real-Time Systems: Theory and practise Alan Burns (Univ. of York, UK) 10:30-11:00 Coffee and refreshments 11:00-12:30 Scheduling in Real-Time Systems (continued) K. Tindell (Northern Real-Time Technologies, UK) 12:30-14:00 Lunch 14:00-15:30 Design of Real-Time Systems E.R. Olderog (Univ. of Oldenburg, DE) 15:30-16:00 Coffee and refreshments 16:00-18:00 Model Checking Real Time Systems K. Larsen (Aalborg Univ., DK) Tuesday, September 10 Tutorials 08:30-10:00 Testing the coverage of Fault-Tolerant and Safety-Critical Systems D. Powell (LAAS-CNRS, FR) 10:00-10:30 Coffee and refreshments Tutorials / Industrial Practise 10:30-12:30 Static Analysis with SPARK: Theory and Practice Mel Jackson (Praxis, USA) 12:30-14:00 Lunch 14:00-16:00 Verification of Safety-Critical Systems using Fast Automated Theorem Proving Lars-Henrik Eriksson (Logikkonsult NP AB, SE) 15:30-16:00 Coffee and refreshments PROGRAMME AT SYMPOSIUM, SEPT 11-13 Wednesday, September 11 08:00- Registration 08:25-08:30 Welcome Invited Lecture 08:30-09:30 Verifying the Correctness of Real-Time Compilers A. Pnueli (Weizmann Inst. IL) 09:30-10:00 Coffee and refreshments State Charts 10:00-10:30 Retiming techniques for statecharts A. Maggiolo-Schettini, A. Peron (Univ. of Pisa, IT) 10:30-11:00 Compiling ARGOS into boleean equations F. Maraninchi, N. Halbwachs (VERIMAG, FR) 11:00-11:30 Real-time mode-machines S. Paynter (British Aerospace Dynamics Ltd., UK) 11:30-11:45 Break 11:45-12:30 Tool Presentations and Demos 12:30-14:00 Lunch Invited Lecture 14:00-15:00 On the Semantics of Group Communication Services in Distributed Systems Flaviu Cristian (UCSD, USA) Timed Automata 15:00-15:30 A calculus for timed automata P.R. D'Argenio, E. Brinskma (Univ. of Twente, NL) 15:30-16:00 Minimizable timed automata J. Springintveld, F. Vaandrager (UNiv. of Njimegen, NL) 16:00-16:30 Coffee and refreshments Duration Calculus 16:30-17:00 Weak chop inverses and liveness in mean-value calculus P.K. Pandya (Tata Institute of Fundamental Research, IN) 17:00-17:30 Synthesizing controllers from duration calculus M. Fr�nzle (Christian-Albrechts Univ. of Kiel, DE) 17:30-18:00 Sampling semantics of duration calculus D.V. Hung, P.H. Giang (United Nations Univ., Macau) 18:30- Reception Thursday, September 12 Invited Lecture 08:30-09:30 Decomposition Techniques for Telecommunications Specifications P. Zave (AT&T, USA) Case Studies 09:30-10:00 The production cell: A verified real-time system H. Dierks (Univ. of Oldenburg, DE) 10:00-10:30 Verification-driven development of a collision- avoidance protocol for the Ethernet K. Karsisto, A. Valmari (Tampere Univ., SF) 10:30-11:00 Coffee and refreshments Scheduling 11:00-11:30 Exhaustive computation of the scheduled task execution sequences of a real-time application A. Choquet-Geniet, D. Geniet, F. Cottet (LISI-ENSMA, FR) 11:30-12:00 Scheduling data flow programs in hard real-time environments R. Davoli, F. Tamburini, L-A. Giachini (Univ. of Bologna, IT) 12:00-12:30 Dynamic scheduling in the presence of faults: specification and verification T. Janowski, M. Joseph (Univ. of Warwick, UK) 12:30-14:00 Lunch Invited Lecture 14:00-15:00 A Unified Approach to Computer-Aided Specification and Verification N. Shankar (SRI International, USA) Fault Tolerance 15:00-15:30 Efficient broadcasting on faulty star networks A. Mei, Y. Igarashi, N. Shimizu (Gunma Univ., JP) 16:00- Excursion and Conference Dinner Friday, September 13 Invited Lecture 08:30-09:30 Formal Methods for Early Fault Detection G. Holzmann (AT&T, USA) Model Checking 09:30-10:00 Model-Checking for extended timed temporal logics A. Bouajjani, Y. Lakhnech, S. Yovine (VERIMAG, FR) 10:00-10:30 Partial orders and verification of real time systems F. Pagani (CERT-ONERA, FR) 10:30-11:00 Coffee and refreshments Specification 11:00-11:30 Toward a modal theory of types for the pi-calculus R.M. Amadio, M. Dam (SiCS, SE) 11:30-12:00 Graphical formalization of real-time requirements C. Dietz (Univ. of Oldenbutg, DE) 12:00-12:30 On specifying real-time systems in a causality-based setting J-P. Katoen, R. Langerak, D. Latella, E. Brinksma (Univ. of Twente, NL) 12:30-14:00 Lunch Verification 14:00-14:30 Verification of embedded systems using synchronous observers M. Westhead, S. Nadjm-Tehrani (Univ. of Edinburgh, UK) 14:30-15:00 Compositionality in real-time shared variable concurency F. de Boer, H. Tej, W-P. de Roever, M. van Hulst (Univ. Kiel, DE) 15:00-15:30 Formal analysis of a real-time kernel specification S. Fowler, A. Wellings (Univ. of York, UK) ---------------------------------------------------------------------- ABSTRACTS FOR THE LECTURES AT THE SCHOOL Scheduling in Real-Time Systems Alan Burns, Univ. of York, UK K. Tindell, Northern Real-Time Technologies, UK The temporal behaviour of any hard real-time system is critically dependent upon the order in which application modules use system resources. A scheduling method defines an ordering and provides appropriate mathematical analysis which allows the worst case behaviour of the application to be predicted. This tutorial will focused upon priority-based scheduling. Single processors and distributed systems will be addressed. Fixed priority scheduling has a number of advantages over the more traditional use of a cyclic executive. In particular sporadic tasks can be easily accommodated and periodic tasks with wide varieties of cycle times and other temporal characterisitcs can be supported in a straightforward way. The tutorial will be in two parts. The first will consider a theoretical framework; the second will illustrate the application of this theory in an industrial setting. For the theoretical part the following topics will be addressed: - computational models for fixed priority scheduling - response time analysis - priority allocation algorithms - resource sharing protocols - cooperative (non-preemptive) scheduling - jitter control and analysis - extensions to facilitate more flexible scheduling Illustration of industrialisation of this theory will look at the automotive industry and consider kernel technology and also the priority-based network communication protocol CAN. A demonstration will be given of some recent developments. The following issues will be addressed: - the CAN network protocol - analysing CAN - support for atomic multicast on CAN - real-time kernel structures (e.g. stack based or not) - scheduling and timing control (i.e. tick driven or event driven) -------------------------------- Design of Real-Time Systems: From Requirements to Programs E.-R. Olderog, University of Oldenburg, DE We present a transformational approach to the stepwise design of correct real-time systems. The design starts from requirements formulated in a subset of Duration Calculus and aims at the specification of distributed communicating programs implementing the real-time requirements. The approach is based on mixed term techniques where syntax pieces of Duration Calculus and the program specification language SL are mixed in a semantically correct manner. The transformation rules are applied to such mixed terms and replace more and more parts of the original requirements by parts of SL. The approach is illustrated by examples. -------------------------------- Model Checking Real Time Systems Kim Larsen, Aalborg Univ., DK In the last few years, a number of logics and formal techniques have been developed to specify, model and analyze quantitative aspects of real-time systems. In particular, several process algebras have found natural real-time extensions, which by now have been thoroughly investigated. A partial result of this study has been the identification of a variety of interesting time-sensitive behavioural relationships. Closely related is the simultaneously developed theory of timed automata due to Alur and the corresponding timed extended temporal logics. This tutorial will address state-of-the-art modelling, specification and automatic verification techniques for real-time systems in the framework of timed automata and will present the state of the verification tool UPPAAL, its applications and foundation. Our tutorial will consist of three parts: - A survey of the theory of timed automata and the relationship to timed process calculi. This part will include a brief survey of interesting time-sensitive behavioural relationships (between timed automata), timed modal logics and their relationship. - A presentation of the tool UPPAAL, an automatic verification tool for timed (and certain hybrid) automata. This part will include a survey of the algorithmic principles (efficient constraint-solving and on-the-fly techniques) underlying the current implementation as well as indications of new promising techniques. - A detailed presentation of some of the various applications of UPPAAL, including an automatic verification of the Philips Audio Protocol with two senders and handling of bus collision. This part will be accompanied with a demonstration of the tool. -------------------------------- Fault-Tolerance Coverage: its Importance and its Statistical Assessment by Fault-Injection David Powell, LAAS, Toulouse, FR Fault-tolerance mechanisms, like any other human-engineered artefact, are never perfect. Residual imperfections in their design are usually the limiting factor to the degree of dependability that can be achieved by a fault-tolerant system. If such a system is to be used in critical applications, it is particularly important to assess the efficiency of the underlying mechanisms. One measure of this efficiency is their fault-tolerance coverage, defined as the probability of system recovery given that a fault exists. This seminar will first give some examples to illustrate the importance of coverage in the dependability that can be achieved by a fault-tolerant system. Then, we will address the issue of evaluating coverage by injecting faults into a prototype system (or a simulation thereof). In particular, details will be given on the statistical techniques that can be used to process the observations collected during a set of fault-injection experiments. The seminar will cover both frequentist and Bayesian methods applied to non-partitioned and partitioned sampling spaces. -------------------------------- Static Analysis with SPARK: Theory and Practice Mel Jackson, Praxis, USA The session will start by explaining the role of static analysis techniques in the validation of safety critical software. These are techniques which, by examination of the program source code, can establish the presence of particular classes of error, or indeed demonstrate their absence. There are two major types of approach, flow analysis and semantic analysis, and the key concepts of each will be explained. The talk will then introduce SPARK, an Ada sublanguage designed for the development of high integrity software. SPARK source code can be subjected to flow analysis using a proprietary tool, the SPARK Examiner. The SPARK Examiner can also generate verification conditions from the source code which can then be manipulated by proprietary verification tools. These establish by semantic analysis the proof of various desirable properties, such as the absence of run-time exceptions. This part of the talk will be illustrated with demonstrations of the various analysis tools. The final part of the talk will discuss full-scale industrial applications of the technology, including the application of SPARK to the mission computer software for the new Lockheed Martin C130J Hercules aircraft. Verification of Safety-Critical Systems using Fast Automated Theorem Proving Lars-Henrik Eriksson, Logikkonsult NP AB, SE Logikkonsult NP AB specialises in consulting and tool development in the area of formal methods. Our consulting tasks range from the development of formal specifications through complete formal verification of software and hardware systems. We concentrate on tasks that can be solved using propositional logic (or predicate logic--as well as arithmetic--with finite domains). Although this might seem restrictive, in practise it has quite large applicability. In our work, we make use of tools based on a very fast proprietary algorithm for solving the satisfiability problem in propositional logic. In this lecture we will present a full scale industrial case, where formal methods are used to validate and verify safety requirements of a railway interlocking system. The lecture will cover formalisation and validation of requirements, as well as formalisation and verification of system implementations. The methodology used will be outlined. In addition the principles of the theorem prover with some basic theoretical notions will be outlined. ABSTRACTS FOR INVITED LECTURES Verifying the Correctness of Real-Time Compilers Amir Pnueli, Weizmann Institute, Rehovot, IL We consider methods for verifying the correctness of compilers for real-time languages. The basic paradigm is essentially the same as for compilers for transformational and sequential languages, based on showing commutation between the compilation syntactic transformation and the semantic mappings of the source and target languages. That is, if we denote the semantic mapping by S and the compiling transformation by C, we have to show, for every source program P the refinement S(C(P)) refines S(P), where "refines" is an appropriate refinement relation, defined over a real-time semantic domains. The proposed method is intended to cover cases in which the compiler cannot be proven correct for all syntactically error-free inputs, because some of them may impose unrealizably stringent timing constraints. Rather than performing a one-shot verification effort, we propose to construct an on-line verifier which will construct and check a proof of correctness for every input individually as it is compiled. The advantages and disadvantages of this method of this approach will be discussed. -------------------------------- On the Semantics of Group Communication Services in Distributed Systems Flaviu Cristian, UCLA, USA In distributed systems, high service availability can be achieved by letting a group of servers replicate the service state. Group communication services, such as membership and atomic broadcast, have been proposed to solve the problem of maintaining server state replica consistency. Group membership groups active servers that can communicate in a timely manner into dynamic groups, while atomic broadcast keeps the replicated state maintained by group members `consistent', despite concurrency, failures and recoveries. This talk investigates what `consistency' means in synchronous systems that are not subject to communication partitions as well as asynchronous systems in which communication partitions can occur. While in synchronous systems, group members are able to roughly know the same state information at the same local clock times, in asynchronous systems the situation is more complex. For such systems, we discuss three different replica consistency criteria: strict agreement, majority agreement and group agreement. The interface issues between the underlying membership services and the broadcast protocols that provide the above semantics are also addressed. -------------------------------- Decomposition Techniques for Telecommunications Specifications Pamela Zave, AT T, USA Telecommunications systems are extremely complex. Features are added continually, despite the fact that their interactions with existing features are poorly understood. Thus the need for modular, incremental specifications of telecommunications systems is particularly acute. This talk describes several decomposition techniques--some new, some newly applied--hat are proving to be successful in this domain. -------------------------------- A Unified Approach to Computer-Aided Specification and Verification Natarajan Shankar, SRI International, USA The field of formal methods is blessed with an overabundance of formalisms (functional, relational, automata-theoretic, modal, temporal), techniques (resolution, rewriting, induction, model checking), and application areas (reactive, fault-tolerant, real-time, hybrid systems). No single verification approach has proven convincingly superior to the others. We argue that it is both necessary and desirable to develop a unified framework within which different approaches can coexist. We also sketch some preliminary efforts in this direction in the context of SRI's PVS system. These efforts include the embedding of special-purpose formalisms (e.g., the duration calculus) into the general-purpose PVS logic, the integration of theorem proving with various forms of model checking, and the application of theorem proving and model checking to the analysis of tabular specifications. -------------------------------- Formal Methods for Early Fault Detection Gerard J. Holzmann, Computing Principles Research, Bell Laboratories, USA A traditional formal verification method becomes an effective weapon in the arsenal of a designer only when he/she has developed a sufficient insight into the design problem to be solved: sufficient to verbalize at least a draft solution to the problem, and to formalize an adequate set of correctness requirements. The irony of this approach is that the larger part of the design problem must be solved before true benefit can be derived from the formal method. I will report on work that aims to develop a new suite of tools for a different design method, based on the paradigm of "Early Fault Detection." It is essential that tools of this type can be applied to incomplete, and possibly inconsistent designs, literally from the first moment that a design process starts. I will report on our first experiences with the introduction of these tools in some large-scale industrial design projects. GENERAL INFORMATION Conference Venue The conference will be held in the conference facilities in "Folkets Hus", Dragarbrunnsgatan 46, in central Uppsala (see the enclosed map in center fold). The majority of accommodation possibilities are located within 5-20 minutes walk from the conference site. Uppsala, situated 70 km north of Stockholm, is the fourth largest city in Sweden with almost 160.000 inhabitants and a decidedly academic atmosphere. Uppsala has always been the religious centre of Sweden. The cathedral is the largest in Scandinavia. Uppsala University, founded in 1477, is the oldest university in Scandinavia and has more than 20.000 students. The weather in Uppsala in August is warm, with a temperature around 15-20 degrees Celsius, ranging between very sunny and rain. A pullover and a rain coat or umbrella can at times be useful. Travel Information Uppsala can be conveniently reached from Stockholm Arlanda airport, which is situated 35 km south of Uppsala. Stockholm Arlanda Airport is served by most major airlines. There is a regular bus service (No. 801) directly from Arlanda Airport to Uppsala city centre every half hour. There are train connections between Stockholm and Uppsala every hour (45 min. ride). By car it takes approx. 45 minutes along the E4 highway. A Taxi from Arlanda to Uppsala costs approximately 300 SEK (ask for fixed price). REGISTRATION Please register for FTRTFT'96 by filling in the attached registration and accommodation form and mailing it to the Conference Secretariat, by regular mail or fax. Note that forms cannot be sent by e-mail. Fees are as follows. Before August 1 After August 1 Regular School 1.000 SEK 1.300 SEK Symposium 1.900 SEK 2.200 SEK Combined 2.700 SEK 3.200 SEK Student School 800 SEK 1.100 SEK Symposium 900 SEK 1.200 SEK Combined 1.500 SEK 2.000 SEK Industry School 3.000 SEK Symposium 1.900 SEK Combined 4.500 SEK The regular fee includes attendance to all sessions, a copy of the proceedings, conference dinner, lunches, refreshments, and excursion. The reduced student fee includes the same as the regular fee except for the conference dinner and excursion, which have to be paid for separately (450 SEK) when applying for the student fee. This should be indicated on the registration form. Requests for refunds will be honored until August 20, except for an administrative fee of 400 SEK. Payments All payments are to be made in SEK. Please effect payment either - By Postal Giro to No. 19 57 52 - 1, Uppsala Turist & Kongress, mark payment "FTRTFT'96". - By international money order, payable to Uppsala Turist & Kongress, mark payment "FTRTFT 96" (note that personal checks will not be accepted). - By money transfer to: F�reningsbanken Uppsala, No. 7124-14-403 79, Box 1014, S - 751 40 Uppsala, Sweden. - By credit card: Am. Express, Visa, Master Card, and Eurocard are accepted Accommodation To reserve your accommodation, please fill in the Hotel Reservations section on the registration form and return it to the Conference Secretariat, preferrably no later than August 1, 1996. We have made preliminary reservations until August 1 in Hotel Svava and Hotel H�rnan in central Uppsala (see the map on center fold). A less expensive alternative is Samariterhemmet, which are guest houses with limited service. At apartment hotel Plantan there are single rooms, double rooms, and rooms with 4-6 beds. Still cheaper are rooms in in private apartments which can be reserved through the conference registration service (Uppsala Turist & Kongress). Prices are as follows. Hotel Single room/night Double room/night -------------------------------------------------------------------- Svava 995 SEK 1185 SEK H�rnan 730 SEK 970 SEK Samariterhemmet 490 SEK 750 SEK Plantan (Breakfast: +50 SEK) 350 SEK 400 SEK Private room 210 SEK/person At Plantan, 4-bed rooms cost 150 SEK, and 6-bed rooms 125 SEK/person. If you wish to share a room, please indicate the name of your room-mate. Conference and Hotel Registration should be directed to the Congress secretariat: FTRTFT 96 Uppsala Turist & Kongress Fyris Torg 8, S-753 10 Uppsala, Sweden. Tel: +46 (0)18 27 48 07 Fax: +46 (0)18 69 24 77 E-mail: Kongress@utkab.se Correspondence on other matters should be directed to the scientific secretariat: FTRTFT 96 c/o Dept. of Computer Systems Uppsala University Box 325, S-751 05 Uppsala, Sweden Tel: +46 (0)18 18 30 21 Fax: +46 (0)18 55 02 25 e-mail: naresh@DoCS.UU.SE -- ---------------------------------------------------------------------- Mats Kindahl ! matkin@docs.uu.se Department of Computer Systems ! Box 325 ! Tel +46 18 18 10 66 S-751 05 Uppsala ! Fax +46 18 55 02 25 SWEDEN ! URL http://www.docs.uu.se/~matkin/ PGP Key fingerprint = 92 5C FC 39 32 A8 7F 91 01 56 A0 D3 9C A9 6C 81 PGP key available under finger matkin@kay.docs.uu.se "People do strange things when you give them money." -- Simple Minds