Suède Norvège Lithuanie Lettonie Islande les Iles Féroé Groenland Finlande Estonie Danemark Chine Åland Suède
NWPT'99
The 11th Nordic Workshop on Programming Theory
Uppsala University, Sweden, October 6-8, 1999

Proceedings


Preface

The objective of the Nordic Workshop on Programming Theory is to bring together researchers from (but not limited to) the Nordic and Baltic countries interested in programming theory, in order to improve mutual contacts and cooperation.

The previous workshops were held in Uppsala (1989), Aalborg (1990), Göteborg (1991 and 1995), Bergen (1992), Åbo (1993 and 1998), Aarhus (1994), Oslo (1996), and Tallinn (1997). In 1999 the workshop again took place at the MIC campus of Uppsala University, hosted by the Department of Computer Systems.

The programme committee consisted of: Magne Haveraaen (Bergen, NO), Hannu-Matti Järvinen (Tampere, FI), Kim G. Larsen (Aalborg, DK), Bengt Nordstrom (Chalmers, SE), Olaf Owe (Oslo, NO), Hans Rischel (DTU, Lyngby, DK), Kaisa Sere (Åbo Akademi, FI), Jüri Vain (Inst. of Cybernetics, EE), and Wang Yi (Uppsala, SE).

We would like to thank the authors of the submitted papers, the invited speakers, and the members of the program committee for their contribution to both the workshop and these proceedings. We are also very grateful for the financial support of ASTEC, the Advanced Software Technology competence centre.

The organizing committee:
Johan Bengtsson, Jakob Engblom, Björn Victor, and Wang Yi (chair)

(This is the online version of the proceedings, also available as Technical report 1999-008 from the Department of Information Technology.)

Invited presentations

Validation of Synchronous Reactive Systems: from Formal Verification to Automatic Testing
Nicolas Halbwachs (VERIMAG, France)
Data-Flow Analysis as Model-Checking of Abstract Interpretations
Bernhard Steffen (Dortmund University, Germany)
Stålmarck's method with extensions to first order logic
Gunnar Stålmarck (Prover Technology AB, Sweden)
Industrial-Strength Functional Programming: Experiences from the Ericsson AXD 301 Project
Ulf Wiger (Ericsson Telecom)

Accepted submissions

Testing
Conformance Testing of Real-Time Systems with Timed Automata
Rachel Cardell-Oliver
Automated Generation of Test Oracles from Temporal Logic Specifications
John Håkansson, Bengt Jonsson, Ola Lundkvist
Synchronous Programming
Synchronous Data-flow Programming in ML
M. Pouzet
Correct Implementations of Abstractions of Location
Pertti Kellomäki
Verification 1
Partial Order Reduction for Region Automata
Dragan Bosnacki
Parametric model-checking in PMC
Giosué Bandini, Ronald Lutje Spelberg, Hans Toetenel
Binary Communication in Parameterized System Verification
Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson
Syntactic Action Refinement in the Modal Mu-Calculus and its Applications to the Verification of Reactive Systems
Mila Majster-Cederbaum, Frank Salger
Semantics
On Semantics and Correctness of Reactive Rule-based Systems
Man Lin, Jacek Malec, Simin Nadjm-Tehrani
Formal Models of Dynamic Programming Constructs
Nisse Husberg
On Shivers's Aggressive Cutoff Method A Study of the 0-CFA
Daniel Damian
Correctness of Unfold/Fold-transformations for Nondeterministic Programs
Björn Lisper
Verification 2
Verification of Sequential Erlang Programs
Gennady Chugunov, Lars-åke Fredlund
Verification of State/Event Systems with Acyclic Dependencies by Quotienting
Nicky O. Bodentien, Jacob Vestergaard, Jakob Friis, Kåre J. Kristoffersen, Kim G. Larsen
Programming Languages
Distributed Implementation of a Process Algebra-Based Programming Language for Embedded Systems
Simon Mørk
Symmetry and Logic Programming
Jinzhao Wu
Logics and Semantics
Branching-Time Logic and Semantisc for Probabilistic Open Systems
Purush Iyer
The Automata-Theoretic Approach Works for Global Trace Logics
Jesper Gulmann Henriksen, Martin Leucker
Linking DC together with TRSL
Anne Haxthausen, Xia Yong
Software Technology
Formal Software Development using Generic Development Steps
Axel Dold
On Modelling Feature Interaction in Telecommunications
Bengt Jonsson, Tiziana Margaria, Gustaf Naeser, Jan Nyström, Bernhard Steffen
A generic tool for expressing the development of validations
J.-P. Bodeveix, M. Filali
Case Studies
Verifying Distributed LEGO RCX Programs Using UPPAAL
Morten Laursen, Rune Gee Madsen, Steffen Kondrup Mortensen
Modeling and Analysis of a Field Bus Protocol Using Uppaal
Alexandre David, Ulf Hammar, Wang Yi
Guided Synthesis of Control Programs using Uppaal for an Industrial Batch Plant
Thomas Hune, Kim G. Larsen, Paul Pettersson
Type and Proof Theory
Incorporating tuple types to C++
Jaakko Järvi
Programming in Martin-Löf Type Theory Unification - A non-trivial Example
Ana Bove
Extending the Window Inference Method
Jeanette Heidenberg
Hybrid Systems
General Hybrid Action Systems
Ralph-Johan Back, Luigia Petre, Iván Porres Paltor
Linear Hybrid Action Systems
Mauno Rönkkö, Xuandong Li
Case Study : A Temperature Control System Modeling and Verification Using Action Systems Formalism Parallel Composition of Two or More Control Systems Simultaneous Control
Ralph-Johan Back, Cristina Cerschi, Iván Porres Paltor
Component based technique for hybrid control systems design
Jüri Vain, Alar Kuusik, Marko Kääramees
UML
An Outline of UML Class Diagram Semantics Using PVS-SL
Demissie B. Aredo, Issa Traoré, Ketil Stølen
An Implementation of UML State Machine Semantics for Model Checking
Johan Lilius, Henri Sara
Code Generation for Hierarchical Systems
Gerd Behrmann, Kåre Kristoffersen, Kim G. Larsen
Specifying the Abstract Layer of a Graphical Editor
Orieta Celiku
Propositional Logics & SAT
An Analogue of Stålmarck's Method for Intuitionistic Propositional Logic
Tarmo Uustalu
Symbolic Reachability Analysis Based on SAT Solvers
Parosh Aziz Abdulla, Per Bjesse, Niklas Een
Object-Oriented Techniques
OUN: A Formalism for Open, Object Oriented, Distributed Systems
Olaf Owe, Isabelle Ryl
Object Integrity & Sharing <= True Object-Orientation
Harri Hakonen, Ville Leppänen, Timo Raita, Tapio Salakoski, Jukka Teuhola
Logics and Semantics
The Decision Procedure for Finitely-Valued Modal Propositional Logics
Jurate Sakalauskaite
Correctness of migration in a subset of Obliq
Hans Hüttel, Josva Kleist, Uwe Nestmann
Action Systems
Mobile Components as Topological Action Systems
L. Petre, M. Waldén
An Action Systems Approach to the FEAL-8 Algorithm
Tiberiu Seceleanu, Sören Holmström


Björn Victor
[Valid HTML 4.0!]