Kim Bruce | 7 Dec 20:34 1998

Final program for FOOL 6

The final program for the sixth international workshop on Foundations of
Object-Oriented Languages (FOOL 6) is available on-line at  Information on registration
is also available there.  The advance registration deadline is December 23.

The workshop is co-located with POPL '99 and will be held on Saturday, 
January 23, 1999, in San Antonio, Texas.

	Kim Bruce

Magne Haveraaen local | 9 Dec 19:42 1998

Positions in Programming Theory, University of Bergen

Attachment: application/octet-stream, 1168 bytes
Rance Cleaveland | 10 Dec 17:46 1998

TACAS '99 Accepted Papers

Below, please find the list of papers that have been accepted for prese=ntation
at the 1999 Conference on Tools and Algorithms for the Construction and
Analysis of Systems (TACAS '99).  TACAS '99 is a constituent of the European
Joint Symposia on Theory and  Practice of Software (ETAPS '99), to be held in

For more information on the conference, please consult its URL:

Rance Cleaveland
TACAS '99 PC Chair


Modular State Level Analysis of Distributed Systems - Techniques and
Tool Support
    Peter Buchholz, Peter Kemper
        Informatik IV
        University of Dortmund

DYANA: An Environment for Embedded System Design and Analysis
    R.L. Smeliansky, A.G. Bakhmurov, A.P. Kapitonova
        Dept. of Computational Mathematics and Cybernetics
        Moscow State University

Using Logic Programs with Stable Model Semantics to Solve Deadlock and
Reachability Problems for 1-Safe Petri Nets
    Keijo Heljanko
        Laboratory for Theoretical Computer Science
        Helsinki University of Technology

On Proving Safety Properties by Integrating Static Analysis, Theorem
Proving and Abstraction
    Vlad Rusu, Eli Singerman
        Computer Science Laboratory
        SRI International

Path Exploration Tool
    Elsa L. Gunter, Doron Peled
        Bell Laboratories

Scheduling System Verification
    Pao-Ann Hsiung, Farn Wang, Yue-Sun Kuo
        Institute of Information Science
        Academia Sinica
        Taiwan, R.O.C.

A Period Assignment Algorithm for Real-Time System Design
    Minsoo Ryu, Seongsoo Hong
        School of Electrical Engineering and ERC-ACI
        Seoul National University

Process Algebra in PVS
    Twan Basten, Jozef Hooman
        Dept. of Computing Science
        Eindhoven University of Technology
        The Netherlands

A theorem prover-based analysis tool for object-oriented databases
    David Spelt, Susan Even
        Center for Telematics and Information Technology
        University of Twente
        The Netherlands

Automated Fast-Track Reconfiguration of Group Communication Systems
    Christoph Kreitz
        Dept. of Computer Science
        Cornell University

Proving the Soundness of a Java Bytecode Verifier Specification in
    Cornelia Pusch
        Institute fuer Informatik
        Technische Universitaet Muenchen

Symbolic Model Checking without BDDs
    Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu
        Computer Science Dept.
        Carnegie-Mellon University

On the Benefits of Using the Up To Techniques for Bisimulation
    Daniel Hirschkoff

Specifications and Proofs for Ensemble Layers
    Jason Hickey (1), Nancy Lynch (2), Robbert van Renesse (1)
        (1) Dept. of Computer Science
            Cornell University
        (2) Laboratory for Computer Science
            Massachusetts Institute of Technology

Ping-Pong Interactions in E-mail Services
    A. Bergeron, J.C. Manzoni
        Universite' du Que'bec a` Montre'al

Hardware testing using a communication protocol conformance testing
    César Viho (1), Hakim Kahlouche (2) , Massimo Zendri (3)
        (1) IRISA/IFSIC
            University de Rennes I
        (2) INRIA, Campus de Beaulieu
        (3) Bull R&D

Automatic verification of cryptographic protocols through
compositional analysis techniques
    Davide Marchignoli (1), Fabio Martinelli (2)
        (1) Dipartimento di Informatica
            Universita di Pisa
        (2) Dipartimento di Matematica
            Universita di Pisa

An Easily Extensible Toolset for Tabular Mathematical Expressions
    Dennis K. Peters (1,2), David Lorge Parnas (2)
        (1) Faculty of Engineering and Applied Sciences
            Memorial University of Newfoundland
        (2) Department of Computing and Software
            McMaster University

A Light-Weight Framework for Hardware Verification
    Christoph Kern, Tarik Ono-Tesfaye, Mark R. Greenstreet
        Dept. of Computer Science
        University of British Columbia

>From DFA-Frameworks to DFA-Generators: A Unifying Multiparadigm
    Jens Knoop
        University of Dortmund

Verification of Hierarchical State/Event Systems using Reusability and
    Gerd Behrmann (1), Kim G. Larsen (1), Henrik R. Andersen (2),
    Henrik Hulgaard (2), Jorn Lind-Nielsen (2)
        (1) BRICS
            Aarhus University
        (2) Department of Information Technology
            Danish Technical University

Timed Diagnostics for Reachability Properties
    Stavros TRIPAKIS

Analyzing Stochastic Fixed-Priority Real-Time Systems
    Mark K. Gardner, Jane W.S. Liu
        Department of Computer Science
        University of Illinois at Urbana-Champaign

Fighting Livelock in the i-Protocol: A Comparative Study of
Verification Tools
    Yifei Dong, Xiaoqun Du, Y.S. Ramakrishna, C.R. Ramakrishnan, I.V.
    Ramakrishnan, Scott A. Smolka, Oleg Sokolsky, Eugene W. Stark, David
    S. Warren
        Dept. of Computer Science
        SUNY at Stony Brook

Symbolic Verification of Lossy Channel Systems: Application to the
Bounded Retransmission Protocol
    Parosh Abdulla (1), Aurore Annichni (2), Ahmed Bouajjani (2)
        (1) Dept. of Computer Systems
            Uppsala University
        (2) Verimag

Finite State Verification for the Asynchronous pi-Calculus
    Ugo Montanari, Marco Pistore
        Computer Science Department
        University of Pisa

Computing Strong/Weak Bisimulation Equivalences and Observation
Congruence for Value-Passing Processes
    Zhoujun Li, Huowang Chen
        Dept. of Computer Science
        Changsha Institute of Technology

Model Checking in CLP
    Giorgio Delzanno, Andreas Podelski
        Max-Planck-Institut fuer Informatik


Rance Cleaveland (rance@...)
Tel:   (516) 632-8448 (voice), (516) 632-8334 (fax)
Post:  Dept. of Comp. Sci., SUNY at Stony Brook, Stony Brook, NY 11794-4400

Daniele Turi | 16 Dec 19:26 1998

abstract syntax and variable binding

The preprint

	Abstract Syntax and Variable Binding 


	M. Fiore, G. Plotkin, and D. Turi

is available as


We develop a theory of abstract syntax with variable binding.
To every binding signature we associate a category of models
consisting of \emph{variable sets} endowed with both a (binding) 
algebra and a substitution structure compatible with each other.
The syntax generated by the signature is the initial model.
This gives a notion of initial algebra semantics encompassing
the traditional one; besides compositionality, it automatically 
verifies the semantic substitution lemma.

Dilip Sequeira | 17 Dec 13:48 1998

Thesis Announcement: Type Inference with Bounded Quantification

I am pleased to announce the availability of my (slightly misleadingly
titled) PhD thesis:

              "Type Inference with Bounded Quantification"
[Abstract below]

The thesis is available electronically from the LFCS on-line
repository of technical reports:


Paper copies can be ordered from: 

Kendal Reid <reports@...>,
Laboratory for Foundations of Computer Science (LFCS),
The University of Edinburgh,
JCMB, The Kings Buildings,
Mayfield Road,
Edinburgh EH9 3JZ,

---------------------------- Abstract --------------------------

In this thesis we study some of the problems which occur when type
inference is used in a type system with subtyping. An underlying poset of
atomic types is used as a basis for our subtyping systems. We argue that
the class of Helly posets is of significant interest, as it includes
lattices and trees, and is closed under type formation not only with
structural constructors such as function space and list, but also any of
records, tagged variants, Abadi-Cardelli object constructors, top, and
bottom. We develop a general theory relating consistency, solvability, and
solution of sets of constraints between regular types built over Helly
posets with these constructors, and introduce semantic notions of
simplification and entailment for sets of constraints over Helly posets of
base types. We extend Helly posets with inequalities of the form a <= tau,
where tau is not necessarily atomic, and show how this enables us to deal
with bounded quantification. 

Using bounded quantification we define a subtyping system which combines
structural subtype polymorphism and predicative parametric polymorphism,
and use this to extend with subtyping the type system of Laufer and
Odersky for ML with type annotations. We define a complete algorithm which
infers minimal types for our extension, using factorisations, solutions of
subtyping problems analogous to principal unifiers for unification
problems. We give some examples of typings computed by a prototype

Sjouke Mauw | 21 Dec 09:52 1998


Attachment: application/octet-stream, 3881 bytes
Dave Schmidt | 30 Dec 00:53 1998

studentship positions

The Laboratory for Specification, Analysis and Transformation of 
Software (SAnToS) at Kansas State University announces openings
for several funded Ph.D. studentships for Autumn 1999.  

The laboratory consists of 5 faculty members, Matthew Dwyer, John 
Hatcliff, Michael Huth, David Schmidt, and Allen Stoughton, as well 
as several visiting and post-doctoral researchers, doctoral and masters

The lab's research is devoted to theory and application of such topics as
program logics, static analysis, semantics, abstract interpretation,
partial evaluation, and model checking. 

Current projects include:
- Development and application of a common framework for expressing
  data-flow analyses, abstract interpretations, and model checking,
  where temporal logic is used as the common language for discourse.

- Application of partial evaluation to naive static analysis algorithms
  so as to generate useful implementations of slicing, code inlining,
  flow analysis, etc.

- Design and implementation of tools for compiling Java source code to 
  abstracted transition systems that can be used by non-formal methods
  experts to model check rudimentary safety properties. 

- Comparative empirical evaluation of existing approaches to finite-state
  verification to characterize effectiveness of automated
  verification with regards to classes of systems and correctness

The lab has strong ties to both the programming languages and software 
engineering research communities.  Laboratory members, including students,
actively participate through publication, presentation, and committee
membership in top international conferences.

Students with interests in either foundational or systems aspects of
program analysis will find the lab an excellent place to further their
studies and are encouraged to apply.

For more information about the work in SAnToS, consult the web-site
For information about application for advanced degree studies, see