Kim Bruce | 7 Dec 20:34 1998
Picon

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 
http://www.cs.williams.edu/~kim/FOOL/FOOL6.html.  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
Picon
Picon

Positions in Programming Theory, University of Bergen

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

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
Amsterdam.

For more information on the conference, please consult its URL:
http://www.csc.ncsu.edu/tacas99.

Rance Cleaveland
TACAS '99 PC Chair

-------------------------
TACAS '99 ACCEPTED PAPERS
-------------------------

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

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
        Russia

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
        Finland

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

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

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
        Korea

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
        USA

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

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

On the Benefits of Using the Up To Techniques for Bisimulation
Verification
    Daniel Hirschkoff
        CERMICS-ENPC
        INRIA
        France

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

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

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

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

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
            Canada
        (2) Department of Computing and Software
            McMaster University
            Canada

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

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

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

Timed Diagnostics for Reachability Properties
    Stavros TRIPAKIS
        Verimag
        France

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

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
        USA

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
            Sweden
        (2) Verimag
            France

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

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

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

--

-- 
Rance Cleaveland (rance@...)
Tel:   (516) 632-8448 (voice), (516) 632-8334 (fax)
WWW:   http://www.cs.sunysb.edu/~rance
Post:  Dept. of Comp. Sci., SUNY at Stony Brook, Stony Brook, NY 11794-4400

Daniele Turi | 16 Dec 19:26 1998
Picon
Picon

abstract syntax and variable binding

The preprint

	Abstract Syntax and Variable Binding 

by 

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

is available as

	http://www.dcs.ed.ac.uk/~dt/abstractsyn.ps

Synopsis:

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
Picon
Picon

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"
                              (1998)
[Abstract below]

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

     <http://www.dcs.ed.ac.uk/lfcsreps/>

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,
UK.

---------------------------- 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
implementation.

Sjouke Mauw | 21 Dec 09:52 1998
Picon
Picon

CONCUR'99 CFP

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
students.  

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
  properties.

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
  http://www.cis.ksu.edu/santos
For information about application for advanced degree studies, see
  http://www.cis.ksu.edu/Programs/Grad/info.html


Gmane