Newsletter 115
April  1, 2008

* Past issues of the newsletter are available at
* Instructions for submitting an announcement to the newsletter
  can be found at
* To unsubscribe, send an email with "unsubscribe" in the
  subject line to

  Call for Short Talks
  Affiliated Workshops - Submission Deadlines
  Preliminary Program
  Invited Talks - Title and Abstracts
  Beth Dissertation Prize - Call for Submissions
  FCS-ARSPA-WITS 2008 - Call for Papers
  LFMTP 2008 - Call for Papers
  PCC 2008 - Call for Papers
  FORMATS'08 - Second Call for Papers
  FMCAD 2008 - Call for Papers
  PerMIS'08 - Call for Papers
  DDBP 2008  - Call for Papers
  ICLP'08 - Call for Workshop Proposals
  Principles of Model Checking - Christel Baier and Joost-Pieter Katoen

  Call for Short Talks
  Submission Deadline: April 21, 2008
* Following a now established tradition, there will be two short talk
  sessions during LICS 2008. You may submit a 1-2 page abstract to
  give a 5-10 minute talk during one of two sessions described
  below. You must clearly indicate which session you would like to
  speak at. Short talks may be trailers for longer presentations at
  one of the affiliated workshops, or stand entirely on their
  own. Abstracts are made available on the LICS website but are not
  published in the conference proceedings. Provocative and
  programmatic presentations are welcome! Note that speakers in either
  session must be registered for LICS or CSF.
* Session 1 (Tue Jun 24): Logic and Security (joint session with CSF)
  Talks should be of interest to the security and logic communities,
  ideally building bridges or proposing new points of intersection or
  applications of one area in the other.
* Session 2 (Thu Jun 26): Logic in Computer Science (LICS-only session)
  Talks can be of any topic related to logic in computer science as
  summarized in the LICS call for papers.
* Abstracts can be submitted at
  Please check the appropriate box, if you would like your talk to be
  considered for the joint CSF/LICS session.
* Important Dates
  Submission: April 21, 2008
  Notification: April 28, 2008
* Paper submission site
  The URL for submitting papers is
  This link will bring you to a page labelled Submission Page for
  LICS/CSF Shorts 2008.
* There are two zones: (1) Registered User and (2) New User. The first
  time you use the system you will have to use the New User
  fields. Shortly after that a password will be emailed to you. You can
  use this password to access the system thereafter as a registered
* On this page you can enter the title, authors, contact author
  information and plain text abstract. The plain text abstract has to be
  under 300 words. It can be typed in directly or pasted in with a
  browser. You can upload your talk abstract using the web page. Using
  this submission system you can manage your short talk abstract
  submitted to LICS 2008. You can submit new papers, resubmit previously
  submitted papers, or change information about authors.
* Abstracts for proposed short talks must be in pdf format and should be
  1-2 pages long.

  Deadlines for Submissions
  for links to the workshop homepages and call for papers.
  Foundations of Computer Security, Automated Reasoning for Security
  Protocol Analysis and Issues in the Theory of Security
  (L.Bauer, S.Etalle, J.den Hartog, L.Vigano)
  Submission deadline: April 10, 2008 (Deadline extended)
* Security and Rewriting, SecRet2008
  (Dan Dougherty, Santiago Escobar)
  Abstract Submission	   March 31, 2008 (passed)
  Full Paper Submission	   April 6, 2008
* Proof-Carrying Code (PCC08)
  (Ian Stark, David Aspinall)
  Abstract submission:	18	April	2008
  Paper submission:	25	April	2008
* Intuitionist Modal Logics and Applications (IMLA08)
  (Valeria de Paiva, Aleks Nanevski)
  Paper submission: April 25, 2008
  International Workshop on Logical Frameworks and MetaLanguages
  (Andreas Abel, Christian Urban)
  Abstracts: 14 April
  Submission: 21 April

  The preliminary propgram for LICS 2008 is now available at

  Title and abstracts of the invited talks at LICS 2008 are now
  available at

* Since 2002, FoLLI (the European Association for Logic,
  Language, and Information, awards the
  E. W. Beth Dissertation Prize to outstanding
  dissertations in the fields of Logic, Language, and
  Information. We invite submissions for the best
  dissertation which resulted in a Ph.D. degree in the
  year 2007. The dissertations will be judged on technical
  depth and strength, originality, and impact made in at
  least two of the three fields of Logic, Language, and
  Computation. Inter-disciplinarity is an important
  feature of the theses competing for the E. W. Beth
  Dissertation Prize.
* Who qualifies
  Nominations of candidates are admitted who were awarded
  a Ph.D. degree in the areas of Logic, Language, or
  Information between January 1st, 2007 and December
  31st, 2007. There is no restriction on the nationality
  of the candidate or the university where the Ph.D.
  was granted. After a careful consideration, FoLLI has
  decided to accept only dissertations written in
  English. Dissertations produced in 2007 but not written
  in English or not translated will be allowed for
  submission, after translation, also with the call
  next year (for 2008). Respectively, nominations of
  full English translations of theses originally
  written in other language than English and defended
  in 2006 and 2007 will be accepted for consideration
  this year, too.
* Prize
  The prize consists of:
  - a certificate
  - a donation of 2500 euros provided by the E. W. Beth
  - an invitation to submit the thesis (or a revised
    version of it) to the new series of books in Logic,
    Language and Information to be published by
    Springer-Verlag as part of LNCS or LNCS/LNAI. (Further
    information on this series is available on the FoLLI site)
* How to submit
  Only electronic submissions are accepted. The following
  documents are required:
  1. the thesis in pdf or ps format (doc/rtf not accepted);
  2. a ten page abstract of the dissertation in ascii or pdf format;
  3. a letter of nomination from the thesis supervisor.
     Self-nominations are not admitted: each nomination must
     be sponsored by the thesis supervisor. The letter of
     nomination should concisely describe the scope and
     significance of the dissertation and state when the
     degree was officially awarded;
  4. two additional letters of support, including at least one
     letter from a referee not affiliated with the academic
     institution that awarded the Ph.D. degree.
* All documents must be submitted electronically to Hard copy submissions are not
  In case of any problems with the email submission or a lack
  of notification within three working days after submission,
  nominators should write to or
* Important dates
  Deadline for Submissions: April 30th, 2008.
  Notification of Decision: July 15th, 2008.
* Committee :
  - Anne Abeill?? (Universit?? Paris 7)
  - Natasha Alechina (University of Nottingham)
  - Didier Caucal (IGM-CNRS)
  - Nissim Francez (The Technion, Haifa)
  - Valentin Goranko  (chair) (University of the Witwatersrand,
  - Alexander Koller (University of Edinburgh)
  - Alessandro Lenci (University of Pisa)
  - Gerald Penn (University of Toronto)
  - Alberto Policriti (Universit?? di Udine)
  - Rob van der Sandt (University of Nijmegen)
  - Colin Stirling (University of Edinburgh)

   Call for Papers
* Background, aim and scope
  Computer security is an established field of computer science of both
  theoretical and practical significance. In recent years, there has
  been increasing interest in logic-based foundations for various
  methods in computer security, including the formal specification,
  analysis and design of security protocols and their applications, the
  formal definition of various aspects of security such as access
  control mechanisms, mobile code security and denial-of-service
  attacks, and the modeling of information flow and its application to
  confidentiality policies, system composition, and covert channel
* WITS is the official annual workshop organised by the IFIP WG 1.7 on
  "Theoretical Foundations of Security Analysis and Design", established
  to promote the investigation on the theoretical foundations of
  security, discovering and promoting new areas of application of
  theoretical techniques in computer security and supporting the
  systematic use of formal techniques in the development of security
  related applications. This is the eighth meeting in the series.
* The workshop FCS continues a tradition, initiated with the Workshops
  on Formal Methods and Security Protocols (FMSP) in 1998 and 1999, then
  with the Workshop on Formal Methods and Computer Security (FMCS) in
  2000, and finally with the LICS satellite Workshop on Foundations of
  Computer Security (FCS) in 2002 through 2005, of bringing together
  formal methods and the security community.
* ARSPA is a series of workshops on Automated Reasoning for Security
  Protocol Analysis, bringing together researchers and practitioners
  from both the security and the formal methods communities, from
  academia and industry, who are working on developing and applying
  automated reasoning techniques and tools for the formal specification
  and analysis of security protocols. The first two ARSPA workshops were
  held as satellite events of the 2nd International Joint Conference on
  Automated Reasoning (IJCAR'04) and of the 32nd International
  Colloquium on Automata, Languages and Programming (ICALP'05),
* FCS and ARSPA have been joining forces since 2006: FCS-ARSPA'06 was
  affiliated with LICS'06, in the context of FLoC'06, and FCS-ARSPA'07
  was affiliated with LICS'07 and ICALP'07.
* The aim of the joint workshop FCS-ARSPA-WITS'08 is to provide a forum
  for continued activity in different areas of computer security,
  bringing computer security researchers in closer contact with the LICS
  community and giving LICS attendees an opportunity to talk to experts
  in computer security, on the one hand, and contribute to bridging the
  gap between logical methods and computer security foundations, on the
* Possible topics include, but are not limited to:
  Automated reasoning techniques
  Composition issues
  Formal specification
  Foundations of verification
  Information flow analysis
  Language-based security
  Logic-based design
  Program transformation
  Security models
  Static analysis
  Statistical methods
  Trust management	for	Access control and resource usage
  Availability and denial of service
  Covert channels
  Integrity and privacy
  Intrusion detection
  Malicious code
  Mobile code
  Mutual distrust
  Security policies
  Security protocols
* Submission
  Submissions should be at most 15 pages (a4paper, 11pt), including
  references. The cover page should include title, names of authors,
  co-ordinates of the corresponding author, an abstract, and a list of
  keywords. Submissions that are clearly too long may be rejected
  immediately. Additional material intended for the referees but not for
  publication in the final version - for example details of proofs - may
  be placed in a clearly marked appendix that is not included in the
  page limit.
  Authors are invited to submit their papers electronically, as portable
  document format (pdf) or postscript (ps); please, do not send files
  fomatted for work processing packages (e.g., Microsoft Word or
  Wordperfect files).
* The only mechanism for paper submissions is via the
  electronic submission web-site
  powered by easychair. Please, follow the instructions given there.
* Important dates
  Papers due:	April 10, 2008 (extended)
  Notification of acceptance:    May 16, 2008
  Final papers:	June 01, 2008

  Pittsburgh, PA, USA, 23 June 2008
  Affiliated with Logic in Computer Science (LICS 2008)
* Important dates:
  Abstract submission:     14 April 2008
  Paper submission:        21 April 2008
  Author notification:     19 May 2008
  Final version:            2 June 2008
  Workshop day:            23 June 2008
* The LFMTP workshop continues the International workshop on Logical
  Frameworks and Meta-languages (LFM) and the MERLIN workshop on
  MEchanized Reasoning about Languages with variable BIndingIN.
* Logical frameworks and meta-languages form a common substrate for
  representing, implementing, and reasoning about a wide variety of
  deductive systems of interest in logic and computer science. Their
  design and implementation on the one hand and their applications in
  for example proof-carrying code have been the focus of considerable
  research over the last two decades. This workshop will bring together
  designers, implementors, and practitioners to discuss all aspects of
  logical frameworks and variable binding.
* The broad subject areas of LFMTP'08 are:
  - The automation and implementation of the meta-theory of programming
    languages and related calculi, particularly work which involves
    variable binding and fresh name generation.
  - The theoretical and practical issues concerning the encoding of
    variable binding and fresh name generation, especially the
    representation of, and reasoning about, datatypes defined from
  - Case studies of meta-programming, and the mechanization of the
    (meta)theory of descriptions of programming languages and other
    calculi.  Papers focusing on logic translations and on experiences
    with encoding programming languages theory are particularly welcome.
* Topics include, but are not limited to
  - logical framework design
  - meta-theoretic analysis
  - applications and comparative studies
  - implementation techniques
  - efficient proof representation and validation
  - proof-generating decision procedures and theorem provers
  - proof-carrying code
  - substructural frameworks
  - semantic foundations
  - methods for reasoning about logics
  - formal digital libraries
* Program Committee:
  Andreas Abel        (LMU Munich)
  Peter Dybjer        (Chalmers University of Technology)
  Alberto Momigliano  (University of Edinburgh)
  Brigitte Pientka    (McGill University)
  Randy Pollack       (University of Edinburgh)
  Carsten Schuermann  (IT University of Copenhagen)
  Peter Sewell        (University of Cambridge)
  Aaron Stump         (Washington University)
  Christian Urban     (TU Munich)
* Three categories of papers are solicited:
  - Category A: Detailed and technical accounts of new research: up
    to fifteen pages including bibliography.
  - Category B: Shorter accounts of work in progress and proposed
    further directions, including discussion papers: up to eight
    pages including bibliography and appendices.
  - Category C: System descriptions presenting an implemented tool
    and its novel features: up to six pages. A demonstration is
    expected to accompany the presentation.
* Submission is electronic.  Authors are required to submit a paper
  title and a short abstract of about 100 words before submitting the
* Papers are to be submitted in postscript or PDF format and must
  conform to the ENTCS style preferably using LaTeX2e. For further
  information and submission instructions, see the LFMTP web page:
* The organizers:
  Andreas Abel                           Christian Urban
  Theoretical Computer Science           Institute for Computer Science
  Ludwig-Maximilians-University Munich   Technical University of Munich
  Email:         Email:

  Call for Papers
  22 June 2008
  Carnegie Mellon University
  Pittsburgh, Pennsylvania, USA
* PCC 2008 is a joint LICS and CSF affiliated workshop on Proof-Carrying
* Proof-carrying code is an important and distinctive approach to
  enhancing trust in programs. It provides a practical framework for
  independent assurance of program behaviour; especially where source
  code is not available, or the code author and user are unknown to
  each other.
* The workshop will address theoretical foundations of proof-carrying
  code as well as practical examples and work on alternative application
  domains. Here "proof" is construed broadly, to include not just
  mathematical derivations but any formal evidence that supports the
  static analysis of programs. That is, evidence about an intrinsic
  property of code and its behaviour that can be independently checked
  by any user, intermediary, or third party. These manifest guarantees
  mean that PCC raises trust in the code itself, distinct from and
  complementary to any existing trust in the creator of the code, the
  process used to produce it, or its distributor.
* Topics include:
  - PCC addressing properties of safety, security, and correctness
    such as:
          Memory safety, information flow, declassification, resource
          management, access control, protocol enforcement, functional
  - Examples of PCC in application domains, including but not
    limited to:
          Mobile code, mobile devices, operating systems, grid
          computing, peer-to-peer computing, active networks, embedded
          systems, cloud computing, databases, e-Science.
  - Probabilistically-checkable proofs, zero-knowledge proofs,
  - Trust and policy frameworks; supporting modular and extensible
    systems; compositionality in code and proofs.
  - Certifying compilation, proof-transforming compilation,
    certified verifiers.
  - Logics and notions of certificate specific to proof-carrying
* Programme Committee
  * David Aspinall, University of Edinburgh (co-chair)
  * Gilles Barthe, INRIA Sophia-Antipolis / IMDEA Software, Madrid
  * Nick Benton, Microsoft Research Cambridge
  * Adriana Compagnoni, Stevens Institute of Technology
  * Karl Crary, Carnegie Mellon University
  * Ewen Denney, NASA Ames
  * Hans-Wolfgang Loidl, LMU Munich
  * George Necula, UC Berkeley / Rinera Networks
  * Ian Stark, University of Edinburgh (co-chair)
  * Stephanie Weirich, University of Pennsylvania
* Important Dates
  Abstract submission:	18	April	2008
  Paper submission:	25	April	2008
  Author notification:	23	May	2008
  Final versions:	7	June	2008
  Workshop:		22	June	2008
* Papers should be in the form of a PDF file using the ENTCS style and
  must not exceed 15 pages. Submission is via the EasyChair system.
  Links: ENTCS style
         EasyChair submission page
* All submissions will be reviewed by the programme committee. There
  will be an informal proceedings distributed at the workshop, with
  final proceedings to appear as a volume of ENTCS.
* Organisers
  David Aspinall and Ian Stark
  Laboratory for Foundations of Computer Science
  School of Informatics
  The University of Edinburgh

  Saint-Malo, France, September 15--17, 2008
  (Co-Located with QEST'08 :
* Submission Deadline : **May 12th**, 2008
  Submission is now open
* Objectives and Scope of the Conference
  Timing aspects of  systems from a variety of  computer science domains
  have been treated independently by different communities.  Researchers
  interested in  semantics, verification and  performance analysis study
  models  such as  timed automata  and  timed Petri  nets.  The  digital
  design  community focuses  on propagation  and switching  delays while
  designers of  embedded controllers  have to take  account of  the time
  taken  by controllers to  compute their  responses after  sampling the
  Timing related  questions in these separate disciplines  do have their
  particularities. However, there is  a growing awareness that there are
  basic  problems that are  common to  all of  them. In  particular, all
  these  sub-disciplines  treat  systems  whose behaviour  depends  upon
  combinations of logical  and temporal constraints; namely, constraints
  on the temporal distances between occurrences of events.
  The  aim  of  FORMATS is  to  promote  the  study of  fundamental  and
  practical aspects of timed  systems, and to bring together researchers
  from  different  disciplines that  share  interests  in modelling  and
  analysis of timed systems. Typical topics include (but are not limited
  - Foundations  and  Semantics:  Theoretical foundations  of  timed
   systems and languages; comparison between different models (timed
   automata,  timed  Petri  nets,  hybrid  automata,  timed  process
   algebra, max-plus algebra,  probabilistic models).
  - Methods and Tools:  techniques, algorithms, data structures, and
   software tools for analyzing timed systems and resolving temporal
   constraints  (scheduling,  worst-case  execution  time  analysis,
   optimisation, model-checking, testing, constraint solving, etc).
   - Applications:   adaptation   and   specialization   of   timing
   technology  in  application  domains  in which  timing  plays  an
   important  role  (real-time   software,  hardware  circuits,  and
   problems of scheduling in manufacturing and telecommunication).
* Submission and Publication:
  The proceedings  of FORMATS'08  will be published  by Springer  in the
  Lecture Notes in Computer  Scienceseries. Papers must contain original
  contributions, be clearly  written, and include appropriate references
  to and comparison with  related work. Simultaneous submission to other
  conferences  with published  proceedings is  not  allowed. Submissions
  should  not exceed  15 pages,  and  should be  formatted according  to
  Springer  LNCS  guidelines.  If   necessary,  the  submission  may  be
  supplemented with a clearly marked appendix, which will be reviewed at
  the discretion of the program committee.
* Program Committee:
  - Eugène Asarin, LIAFA, Univ. Paris 7 and CNRS, France
  - Patricia Bouyer, CNRS, LSV, France
  - Ed Brinksma, ESI, Univ. of Twente & Eindhoven Univ. of Technology,
                        The Netherlands
  - Franck Cassez, CNRS/IRCCyN, Nantes, France
  - Flavio Corradini, Univ. Camerino, Italy
  - Deepak D'Souza, CSA, IISc, Bangalore, India
  - Martin Fränzle, Univ. of Oldenbourg, Germany
  - Goran Frehse, Univ. Grenoble 1, Verimag, France
  - Claude Jard, ENS Cachan/IRISA, Rennes, France
  - Joost-Pieter Katoen RWTH Aachen Univ., Germany
  - Bruce Krogh, CMU, USA
  - Salvatore La Torre, Univ. of Salerno, Italy
  - Insup Lee, Univ. of Pennsylvania, USA
  - Rupak Majumdar, UCLA, USA
  - Brian Nielsen, CISS & Aalborg Univ., Denmark
  - Joël Ouaknine, Oxford Univ., UK
  - Paritosh Pandya, TIFR, Bombay, India
  - Paul Pettersson, Mälardalen Univ., Sweden
  - Jean-François Raskin, ULB, Belgium
  - P.S. Thiagarajan, National Univ. of Singapore
  - Stavros Tripakis, Cadence Research Labs and Verimag/CNRS,
                Berkeley, USA
  - Frits Vaandrager, Radboud Univ. Nijmegen, The Netherlands
  - Farn Wang, National Taiwan Univ., Taiwan
  - Wang Yi, Uppsala Univ., Sweden
  - Tomohiro Yoneda, NII, Tokyo, Japan
* Chairs:
 - Franck Cassez (CNRS/IRCCyN, Nantes, France)
 - Claude Jard (ENS Cachan/IRISA, Rennes, France)
* Important Dates:
  -  Submission Deadline: May 12th, 2008
  -  Notification: June 23rd, 2008

  (FMCAD 2008)
  Call for Papers
  November 17-18, 2008
  Embassy Suites Portland--Downtown
  Portland, Oregon
* Important Dates (firm)
  Paper Submission Deadline:    May 12, 2008
  Author Feedback:              June 19-22, 2008
  Acceptance Notification:      July 3, 2008
  Final Version Due:            August 17, 2008 (To be confirmed)
  Early Registration Deadline:  October 14, 2008
  Hotel Registration Deadline:  October 17, 2008 (To be confirmed)
  FMCAD 2008 is the eighth in a series of conferences on the theory and
  application of formal methods in hardware and system design and
  verification. In 2005, the bi-annual FMCAD and sister conference
  CHARME decided to merge to form an annual conference with a unified
  community. The resulting unified FMCAD provides a leading
  international forum to researchers and practitioners in academia and
  industry for presenting and discussing groundbreaking methods,
  technologies, theoretical results, and tools for formally reasoning
  about computing systems, as well as open challenges therein.  Topics
  of interest for the technical program include, but are not limited to:
  - Foundations: advancing industrial-strength technologies in model
    checking, theorem proving, equivalence checking, abstraction and
    refinement techniques, property-preserving reduction techniques,
    compositional methods, decision procedures, SAT- and BDD-based
    methods, combining deductive methods with decision procedures, and
    probabilistic methods.
  - Verification applications: tools, industrial experience reports,
    and case studies.  We encourage the submission of materials
    relating to novel and challenging industrial-scale applications of
    formal methods, including problem domains where formal methods
    worked well or even fell short. We also encourage submissions
    relating to the development and execution of methodologies for
    formal and informal verification strategies.
  - Applications of formal methods in design: topics relating to the
    application and applicability of assertion-based verification,
    equivalence checking, transaction-level verification, semi-formal
    verification, runtime verification, simulation and testcase
    generation, coverage analysis, microcode verification, embedded
    systems, software verification, concurrent systems, timing
    verification, and formal approaches to performance and power.
  - Model-based approaches: modeling and specification languages,
    system-level design and verification, design derivation and
    transformation, and correct-by-construction methods.
  - Formal methods for the design and verification of emerging and
    novel technologies: nano, quantum, biological, video, gaming, and
    multimedia applications.
* Paper Submission
  Submissions must be made electronically in PDF format through the
  FMCAD'08 web site, The proceedings will be
  published by ACM and will be available online in the ACM Digital
  Library and the IEEE Xplore Digital Library. Two categories of papers
  can be submitted: regular papers (8 pages), containing original
  research that has not been previously published, nor concurrently
  submitted for publication; and short papers (4 pages), describing
  applications, case studies, industrial experience reports, emerging
  results, or implemented tools with novel features.
  Regular and short papers must use the IEEE Transactions format on
  letter-size paper with a 10-point font size (see
  We recommend that self-citations be written in the third person, though
  authors will be required to identify themselves on their submissions.
  Submissions must contain original research that has not been
  previously published, nor concurrently submitted for publication. Any
  partial overlap with any published or concurrently submitted paper
  must be clearly indicated. If experimental results are reported,
  authors are strongly encouraged to provide adequate access to their
  data so that results can be independently verified.
  A small number of accepted papers will be considered for a
  distinguished paper award.
* Program Committee
 - Mark Aagaard, University of Waterloo, Canada
 - Jason Baumgartner, IBM Corporation, USA
 - Valeria Bertacco, University of Michigan, USA
 - Armin Biere, Johannes Kepler University, Austria
 - Per Bjesse, Synopsys, USA
 - Roderick Bloem, TU Graz, Austria
 - Dominique Borrione, Grenoble University, France
 - Gianpiero Cabodi, Politecnico di Torino, Italy
 - Alessandro Cimatti (co-chair), FBK-irst, Trento, Italy
 - Koen Claessen, Chalmers University of Technology, Sweden
 - Ganesh Gopalakrishnan, University of Utah, USA
 - Aarti Gupta, NEC Laboratories America, USA
 - Alan J. Hu, University of British Columbia, Canada
 - Robert Jones (co-chair), Intel Corp., USA
 - Daniel Kroening, ETH Zurich, Switzerland
 - Andreas Kuehlmann, Cadence Laboratories, USA
 - Wolfgang Kunz, University of Kaiserslautern, Germany
 - Shuvendu Lahiri, Microsoft, USA
 - Jeremy Levitt, Mentor Graphics, USA
 - Panagiotis Manolios, Northeastern University, USA
 - Andy Martin, IBM Research Division, USA
 - Tom Melham, Oxford University, UK
 - Ken McMillan, Cadence Labs, USA
 - John O'Leary, Intel Corp., USA
 - Lee Pike, Galois Inc., USA
 - Rajeev Ranjan, Jasper Design Automation, USA
 - Sandip Ray, University of Texas at Austin, USA
 - Fei Xie Portland State U., USA
 - Alper Sen, Freescale Austin, USA
 - Natasha Sharygina, University of Lugano, Switzerland
 - Eli Singerman, Intel Corp., USA
 - Karen Yorav, IBM Haifa Research Laboratory, Israel

  Call for Papers
  August 19-21, 2008
  Washington DC, U.S.A.
* PerMIS'08 will be the eighth in the series that started
  in 2000, targeted at defining measures and methodologies of evaluating
  performance of intelligent systems. The workshop has proved to be an
  excellent forum for discussions and partnerships, dissemination of
  ideas, and future collaborations in an informal setting. Attendees
  usually include researchers, graduate students, practitioners from
  industry, academia, and government agencies.
* PerMIS'08 aims at identifying and quantifying contributions of
  functional intelligence towards achieving success. Our working
  definition of functional intelligence is the ability to act
  appropriately in an uncertain environment, where appropriate action is
  that which increases the probability of success, and success is
  the achievement of behavioral goals (J. Albus, 1991). In addition to
  the main theme, as in previous years, the workshop will focus on
  applications of performance measures to practical problems in
  commercial, industrial, homeland security, and military applications.
* Topic areas include, but are not limited to:
  - Defining and measuring aspects of a system:
        The level of autonomy
        Human-robot interaction
        Collaboration & Coordination
  - Evaluating components within intelligent systems:
        Sensing and perception
        Knowledge representation, world models, ontologies
        Planning and control
        Learning and adapting
  - Infrastructural support for performance evaluation:
        Testbeds and competitions for intercomparisons
        Instrumentation and other measurement tools
        Simulation and modeling support
  - Technology readiness measures for intelligent systems
  - Applied performance measures in various domains, e.g.,
        Intelligent transportation systems
        Emergency response robots (search and rescue, bomb disposal)
        Homeland security systems
        De-mining robots
        Defense robotics
        Hazardous environments (e.g., nuclear remediation)
        Industrial and manufacturing systems
        Space/Aerial  robotics
        Medical Robotics & assistive devices
* Submission Information
  Prospective authors are requested to submit a
  draft paper (max. 8 pages) or an extended abstract (1-2 pages) for
  review. Invited session proposals can also be submitted as draft
  papers but should contain 1) a session title and a brief statement of
  purpose, 2) name and affiliation of the organizer(s), and 3) a
  preliminary list of speakers. All submissions must be written in
  English, starting with a succinct statement of the problem, the
  results achieved, their significance, and a comparison with previous
  work. Papers are to be submitted at using the
  specified templates.
* Important Dates
  Submission of full papers       May 29, 2008
  Proposal for invited sessions   June 06, 2008
  Notification of acceptance      June 27, 2008
  Final papers due                July 25, 2008
* Program Committee
  S. Balakirsky NIST USA
  R. Bostelman NIST USA
  F. Bonsignorio Heron Robots Italy
  G. Berg-Cross EM & I USA
  J. Bornstein ARL USA
  P. Courtney PerkinElmer UK
  J. Evans USA
  D. Gage XPM Tech. USA
  J. Gunderson GammaTwo USA
  L. Gunderson GammaTwo USA
  S.K. Gupta UMD USA
  A. Jacoff NIST USA
  S. Julier Univ. College London UK
  M. Lewis UPitt USA
  T. Kalmar-Nagy Texas A& M USA
  A. del Pobil Univ. Jaume-I Spain
  S. Ramasamy UALR USA
  L. Reeker NIST USA
  C. Schlenoff NIST USA
  M. Shneier NIST USA
  E. Tunstel JHU-APL USA

 Call for Papers
 September 15/16, 2008, Munich, Germany
 Affiliated workshop of the 12th IEEE International EDOC Conference
 The capability of rapidly adapting systems and processes to an
 ever-changing environment to leverage existing resources has become a
 crucial factor of an organization's agility. The traditional approach
 to process management is only partially appropriate to this new
 context, and calls for the advent of new, dynamic business processes.
 Broad business policies or narrower constraints of technical nature
 make dynamic business process particularly suited to a declarative
 approach to their modelling and design.
 Topics of the workshop include but are not limited to:
 - Dynamic business process modelling
 - Implementation issues for dynamic processes
 - Tools for dynamic processes
 - Use cases of dynamic processes
 - Business and technical requirements for dynamic processes
 - Declarative model specification
 - Mathematical and logical foundations of declarative business
 - Formal models of declarative business processes
 - Monitoring of declarative business processes
 - Validation of declarative business processes
 - Tools for declarative business processes
 The papers accepted for the workshop will be published with their own
 ISBN by the IEEE in the IEEE Digital Library.
  - Paper submission:  June 13th, 2008
  - Paper notification:  July 18th, 2008
  - Camera ready:  July 28th, 2008
  - Workshop:  September 15th or 16th (to be confirmed)
 - Dragan Gasevic, Athabasca University and Simon Fraser University,
 - Tobias Graml, ETH Zürich, Switzerland
 - Sylvain Halle, Université du Québec à Montréal, Canada
* PROGRAM COMMITTEE (to be completed)
 - Colin Atkinson, Universität Mannheim, Germany
 - Claudio Bartolini, HP Labs Palo Alto, USA
 - Thomas Bauer, DaimlerChrysler Group Research and Advanced
   Engineering, Germany
 - Andrew Berry, Deontik, Australia
 - Kamal Bhattacharya, IBM Watson, USA
 - Domenico Bianculli, University of Lugano, Switzerland
 - Franck van Breugel, York University, Canada
 - Christoph Bussler, Cisco Systems, Inc, USA
 - Sanjay Chaudhary, Dhirubhai Ambani Institute of Information and
   Communication Technology, India
 - Marlon Dumas, University of Tartu, Estonia
 - Dragan Gasevic, Athabasca University, Canada
 - Xiang Fu, Georgia Southwestern State University, USA
 - Karthik Gomadam, Wright State University, USA
 - Guido Governatori, University of Queensland, Australia
 - Reiko Heckel, University of Leicester, UK
 - Jana Koehler, IBM Zürich, Switzerland
 - Zoran Milosevic, Deontik, Australia
 - Shin Nakajima, National Institute of Informatics, Japan
 - Leo Orbst, The MITRE Corporation, USA
 - Maja Pesic, Technical University of Eindhoven, The Netherlands
 - Manfred Reichert, University of Twente, The Netherlands
 - Stefanie Rinderle, Universität Ulm, Germany
 - Florian Rosenberg, Technical University of Vienna, Austria
 - Shazia Sadiq, The University of Queensland, Australia
 - Jennifer Sampson, National ICT Australia
 - Biplav Srivastava, IBM India Research Lab
* Detailed information can be found on the workshop webpage:

  Call for Workshop Proposals
  December 9-13, 2008
  Udine, Italy
* ICLP'08, the 24rd International Conference on Logic Programming, will
  be held in Udine (Italy), from December 9 to 13, 2008.
* Workshops co-located with international conferences are one of the
  best venue for the presentation and discussion of preliminary work or
  novel ideas, and new open problems to a wide and interested audience.
  Co-located workshops also provide an opportunity for
  presenting specialized topics and opportunities for intensive
  discussions and project collaboration. The topics of the workshops
  co-located with ICLP'08 can cover any areas related to logic
  (e.g., theory, implementation, environments, language issues,
  alternative paradigms, applications) including cross-disciplinary
  However, any workshop proposal will be considered.
* The format of the workshop will be decided by the workshop organizers,
  but ample time must be allowed for general discussion. Workshops can
  vary in length, but the optimal duration will be half a day or a
  full day.
* Workshop Proposal:
  Those interested in organizing a workshop at ICLP'08 are invited
  to submit a workshop proposal. Proposals should be in English and
  about two pages in length. They should contain:
  - The title of the workshop.
  - A brief technical description of the topics covered by the
  - A discussion of the timeliness and relevance of the workshop.
  - A list of some related workshops held in the last years
  - The (preliminary) required number of half-days allotted to the
    workshop and an estimate of the number of expected attendees.
  - The names, affiliation and contact details (email, web page, phone,
    fax) of the workshop organizer(s) together with a
    designated contact person.
  - The previous experiences of the workshop organizing committee in
    workshop/conference organization.
* Proposals are expected in ASCII or PDF format. All proposals should be
  submitted to the Workshop Chair (Tran Cao Son) by email
  ( by June 2nd, 2008.
* Workshop Organizers' Tasks:
  - Producing a "Call for Papers" for the workshop and posting it
    on the net and/or other means. Please provide a web page URL which
    can be linked into the ICLP'08 home page by July 15th, 2008.
  - Providing a brief description of the workshop for the conference
  - Reviewing/accepting submitted papers.
  - Scheduling workshop activities in collaboration with the local
    organizers and the workshop chair.
  - Sending workshop program and workshop proceedings in  pdf
    format to the workshop chair for printing (deadline to be defined)
  - The use of the Computing Research Repository (CoRR) for the
    workshop proceedings is strongly suggested
    [Guidelines for electronic publishing of proceedings])
* Location:
  All workshops will take place in the city of Udine at the site of the
  main conference. See the ICLP'08 web site for location details.
* Important Dates:
  June     2,    2008: Proposal submission deadline
  June     15,   2008: Notification
  July     15,   2008: Deadline for receipt of CFP and URL for workshop
                       web page
  November 1,    2008: Deadline for preliminary proceedings
  December 9-13, 2008: ICLP'08 workshops
* Workshop Chair:
  Tran Cao Son  [tson AT cs dot nmsu dot edu] (

  by Christel Baier and Joost-Pieter Katoen
  MIT Press 2008, 993 pages
  ISBN: 978-0-262-02649-9
* Principles of Model Checking offers a comprehensive introduction to
  model checking that is not only a text suitable for classroom use but
  also a valuable reference for researchers and practitioners in the
* The book begins with the basic principles for modeling concurrent
  and communicating systems, introduces different classes of properties
  (including safety and liveness), presents the notion of fairness, and
  provides automata-based algorithms for these properties. It introduces
  the temporal logics LTL and CTL, compares them, and covers algorithms
  for verifying these logics, discussing real-time systems as well as
  systems subject to random phenomena. Separate chapters treat such
  efficiency-improving techniques as abstraction and symbolic
  manipulation. The book includes an extensive set of examples (most of
  which run through several chapters) and a complete set of basic
  results accompanied by detailed proofs. Each chapter concludes with
  a summary, bibliographic notes, and an extensive list of exercises
  of both practical and theoretical nature.
* Complementary material such as slides and solutions to selected
  exercises will be made available to lecturers.
* Foreword by Kim G. Larsen; endorsements by Moshe Vardi and Gerard
* Further information can be found at:

* The Computing Laboratory has a vacancy for a postdoctoral research
  assistant in the area of Database Theory. The post is funded by the
  EPSRC Project "Schema Mappings and Services for Data Integration and
  Exchange" (PI Georg Gottlob).
* The contract will have a duration of approximately two years, and is
  available from April 2008. Salary will be on the University Grade 7,
  (£26,666 to £32,796 p.a.)
* Applicants should have, or expect shortly to obtain, a doctoral degree
  in computer science, mathematics, or related discipline, and should be
  skilled in theoretical computer science and mathematics. They should
  have relevant scientific publications, possess good scientific-writing
  skills and project management skills.
* The post will require occasional travel to conferences and
  co-operation with partners in the EU and in America.
* Application deadline: 15 April 2008.
* For more details, see

* The Information Systems Research Group is offering fully-funded PhD
  positions in Oxford University's Computing Laboratory in Information
  Systems. This position is not tied to a project, and any student with
  a strong background in theoretical computer science and an interest in
  information management can apply.
* Research topics available include
  - logic and complexity: (logic and automata on trees, tractability of
    graph and hypergraph algorithms),
  - database theory (tractability in query processing, foundational and
    systems issues in XML query processing, data cleaning, and data
    integration), and
  - database systems (querying of social networks, information extraction,
    stream processing).
* The studentships are fully funded *at EU fee levels* for three years
  from October 2008.  Each includes a stipend of £12,600 per year as well
  as provision for travel to conferences.  Students who are *not* from
  EU countries will need supplementary funding.
* Candidates must satisfy the usual requirements
  for doing a doctorate at Oxford.  For Further Information contact
  Michael Benedikt
  ( or
  Georg Gottlob (, who
  will be happy to discuss this position on an informal basis.
* The deadline for applications is April 30,
  2008. Interviews for qualified candidates will take place in May of
  2008. To apply you need to download the University's application form
  You will need to submit references, transcript, and a statement of
  research interests (in the slot marked ``research proposal') with
  your application.
  Submit the form to:
    Mrs Julie Sheppard
    Secretary for Graduate Studies,
    Oxford University Computing Laboratory
    Wolfson Building, Parks Road,
    Oxford, OX1 3QD, UK
  for e-mail queries:

Back to the LICS web page.