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