Olivier Zendra | 23 Apr 15:37 2014

ICOOOLPS 2014 Call For Papers

                      CALL FOR PAPERS FOR THE

                       9th ICOOOLPS Workshop

     Implementation, Compilation, Optimization of OO Languages,
                        Programs and Systems

                  July 28th 2014, Uppsala, Sweden
                        Colocated with ECOOP


Important dates
Submission:   May 5th 2014 
Notification: May 26th 2014
Workshop:     July 28th 2014

Invited talk
Handcrafting VMs for dynamic languages: reality and dreams, 
Vyacheslav Egorov, Google
This is a story of what happens when the art of VM construction meets 
development constraints. This is a first-person narrative about my experience 
with the V8 and Dart virtual machines, fundamental engineering decisions, and 
their implications. I will try to show how production VMs are treading the thin 
line between "practical reality" and "dreams of academia". Finally I intend 
to share my own dreams on how ideas borrowed from academia could help to 
solve practical issues in VM-construction.
(Continue reading)

masoume tajvidi | 24 Apr 11:51 2014


My function for finding the max number of a list is as follows:
val Max_List = Define ( Max_List []= NONE)

 /\ ( Max_List (h::l) = let max= Max_List l in 

( if h > max then SOME h else if h = max then NONE 

(else( Max_List l)))

I do not know whats wrong with this? 
Can anybody help please?
when I use 0 instead of zero it works properly.

Thanks a lot

Start Your Social Network Today - Download eXo Platform
Build your Enterprise Intranet with eXo Platform Software
Java Based Open Source Intranet - Social, Extensible, Cloud Ready
Get Started Now And Turn Your Intranet Into A Collaboration Platform
hol-info mailing list
hol-info <at> lists.sourceforge.net
Carlo Alberto Furia | 24 Apr 13:05 2014

WING 2014: Invariant Generation

-----> DEADLINE EXTENDED: 1 May 2014

Call for Contributions

WING 2014: 5th International Workshop on Invariant Generation

23 July 2014. Vienna, Austria


** Important Dates: **

Submission deadline:  1 April 2014
Workshop:  23 July 2014

** About WING **

The ability to automatically extract and synthesize auxiliary properties
of programs has had a profound effect on program analysis,  testing, and
verification over the last several decades. A key impediment for program
verification is the overhead associated with providing, debugging, and
verifying auxiliary invariant annotations. Releasing the software
developer from this burden is crucial for ensuring the practical
relevance of program verification. In the context of testing, suitable
invariants have the potential of enabling high-coverage test-case
generation. Thus, invariant generation is a key ingredient in a broad
spectrum of tools that help to improve program reliability and
understanding. As the design and implementation of reliable software
remains an important issue, any progress in this area will have a
significant impact.

The increasing power of automated theorem proving and computer algebra
has opened new perspectives for computer-aided program verification; in
particular for the automatic generation of inductive assertions in order
to reason about loops and recursion. Especially promising breakthroughs
are invariant generation techniques by Groebner bases, quantifier
elimination, and algorithmic combinatorics, which can be used in
conjunction with model checking, theorem proving, static analysis, and
abstract interpretation. The aim of this workshop is to bring together
researchers from these diverse fields.

** Paper Submissions **

We encourage submissions on work in progress, new ideas, tools under
development, as well as work by PhD students, to be presented at WING
2014. Submissions should adhere to the EasyChair document class, and be
between 6 and 15 pages.

Submissions need not be original. Extended versions of submissions may
have been published previously, or submitted concurrently with or after
WING 2014 to another workshop, conference or a journal.

** Program Committee **

Stephan Falke (Karlsruhe Institute of Technology (KIT))
Carlo A. Furia (ETH Zurich)
Arie Gurfinkel (Software Engineering Institute, CMU)
Dilian Gurov (Royal Institute of Technology (KTH))
Reiner Hähnle (TU Darmstadt) -- chair
Andrew Ireland (Heriot-Watt University)
Bart Jacobs (Katholieke Universiteit Leuven, Belgium)
Einar Broch Johnsen (University of Oslo) -- chair
Laura Kovacs (Chalmers University of Technology)
Enric Rodríguez Carbonell (Technical University of Catalonia)
Philipp Ruemmer (Uppsala University, Department of IT)

Start Your Social Network Today - Download eXo Platform
Build your Enterprise Intranet with eXo Platform Software
Java Based Open Source Intranet - Social, Extensible, Cloud Ready
Get Started Now And Turn Your Intranet Into A Collaboration Platform
Serge Autexier | 22 Apr 09:24 2014

CfP: 8th Verification Workshop (VERIFY 2014), Focus Theme: Verification Beyond IT Systems, extended deadline *May 5th, 2014*

[Apologies for cross posting, Deadline extended to *May 5th, 2014*]

                            CALL FOR PAPERS

         8th International Verification Workshop (VERIFY'14)
              in connection with IJCAR 2014 at FLoC 2014
                  July 23-24, 2014, Vienna, Austria


The formal  verification of  critical information  systems has  a long
tradition  as one  of  the  main areas  of  application for  automated
theorem proving. Nevertheless, the area is of still growing importance
as the number of computers  affecting everyday life and the complexity
of  these systems  are  both  increasing. The  purpose  of the  VERIFY
workshop  series is  to  discuss problems  arising  during the  formal
modeling and  verification of  information systems and  to investigate
suitable solutions.  Possible perspectives include those  of automated
theorem proving, tool support, system engineering, and applications.

The VERIFY  workshop series aims  at bringing together people  who are
interested in the development of safety and security critical systems,
in formal  methods, in  the development  of automated  theorem proving
techniques,  and  in  the   development  of  tool  support.  Practical
experiences gained in  realistic verifications are of  interest to the
automated theorem proving community and new theorem proving techniques
should  be transferred  into practice.  The overall  objective of  the
VERIFY workshops is to identify  open problems and to discuss possible
solutions under the theme

What are the verification problems? What are the deduction techniques?

The 2014 edition of VERIFY aims for extending the verification methods
for processes implemented in hard-  and software to processes that may
well include computer-assistance, but have  a large part or a frequent
interaction  with non-computer-based  process  steps.  Hence the  2014
edition will run under the focus theme

                    Verification Beyond IT Systems

A  non-exclusive list of application areas  with these characteristics

       * Ambient assisted living
       * Intelligent home systems and processes
       * Business systems and processes
       * Production logistics systems and processes
       * Transportation logistics
       * Clinical processes
       * Social systems and processes (e.g., voting systems)

The scope of VERIFY includes topics such as

       * ATP techniques in verification
       * Case studies (specification & verification)
       * Combination of verification systems
       * Integration of ATPs and CASE-tools
       * Compositional & modular reasoning
       * Experience reports on using formal methods
       * Gaps between problems & techniques
       * Formal methods for fault tolerance
       * Information flow control security
       * Refinement & decomposition
       * Reliability of mobile computing
       * Reuse of specifications & proofs
       * Management of change
       * Safety-critical systems
       * Security models
       * Tool support for formal methods

Submissions are encouraged in one of the following two categories:

A. Regular  paper:  Submissions  in  this  category  should   describe
   previously unpublished  work (completed or in  progress), including
   descriptions of research, tools,  and applications.  Papers must be
   5-14  pages  long (in  EasyChair  style)  or  6-15 pages  long  (in
   Springer LNCS style).

B. Discussion  papers: Submissions  in this  category are  intended to
   initiate discussions and hence should address controversial issues,
   and may include  provocative statements. Papers must  be 3-14 pages
   long  (in EasyChair  style) or  3-15 pages  long (in  Springer LNCS

Important dates
   Abstract Submission Deadline:    May 5th, 2014 (extended)
   Paper Submission Deadline:       May 5th, 2014 (extended)
   Notification of acceptance:      May 20, 2014
   Final version due:               May 27, 2014
   Workshop date:                   July 23-24, 2014

Submission is via EasyChair:

Program Committee

 Serge Autexier (DFKI) - chair
 Bernhard Beckert (Karlsruhe Institute of Technology) - chair
 Wolfgang Ahrendt (Chalmers University of Technology)
 Juan Augusto (Middlesex University)
 Iliano Cervesato (Carnegie Mellon University)
 Jacques Fleuriot (University of Edinburgh)
 Marieke Huisman (University of Twente)
 Dieter Hutter (DFKI GmbH)
 Reiner Haehnle (Technical University of Darmstadt)
 Deepak Kapur (University of New Mexico)
 Gerwin Klein (NICTA and UNSW)
 Joe Leslie-Hurd (Intel Corporation)
 Fabio Martinelli (IIT-CNR)
 Catherine Meadows (NRL)
 Stephan Merz (INRIA Lorraine)
 Tobias Nipkow (TU Munich)
 Lawrence Paulson (University of Cambridge)
 Johann Schumann (SGT, Inc/NASA Ames)
 Kurt Stenzel (University of Augsburg)

Start Your Social Network Today - Download eXo Platform
Build your Enterprise Intranet with eXo Platform Software
Java Based Open Source Intranet - Social, Extensible, Cloud Ready
Get Started Now And Turn Your Intranet Into A Collaboration Platform
Ramana Kumar | 22 Apr 09:19 2014

HOL'14 Workshop (Deadline Extended)

                     CALL FOR ABSTRACTS

             2014 International Workshop on HOL4
               The HOL Theorem Proving System
                   hosted by ITP at FLoC
               July 13, 2014, Vienna, Austria



Abstract Submission     5th May 2014 (EXTENDED)
Author Notification     15th May   2014

HOL4 is the latest incarnation of the original theorem prover
for Higher-Order Logic, and is still a popular choice for
programming tactics and proof automation, and developing formal
theories. This year we invite everyone interested in the use and
development of HOL4 to participate in the reignition of a series
of workshops dedicated to improving both the tool itself and the
breadth of knowledge spread across its community of users.

The theme of the workshop is "hidden features": many useful
tools and methods for interacting with HOL4 and using it for
formal development work, some of which have been developed
relatively recently, are used regularly by some while remaining
unknown to others. Anyone who has used the system likely falls
into both categories for different features. We thus encourage
everyone to present the aspects of their idiomatic usage of HOL4
that they find particularly useful and think could be better

A parallel theme is "feature requests": newcomers and seasoned
theorem prover drivers alike often wish that some aspect of
their tools worked more smoothly or quickly, included more
automation, were more user-friendly, or even existed at all. We
therefore also solicit requests, plans, and design
considerations for improvements to HOL4 to be discussed and
possibly implemented at the workshop.

To register your interest in presenting hidden features and/or
feature requests at the workshop, please submit a short abstract
describing what you want to do and how long you would like to
have the floor (from 5 through 30 minutes). There will be
flexibility for impromptu talks and discussion on the day, but
we highly encourage early submissions to give priority to
better-prepared work.

Submissions is via EasyChair:
Start Your Social Network Today - Download eXo Platform
Build your Enterprise Intranet with eXo Platform Software
Java Based Open Source Intranet - Social, Extensible, Cloud Ready
Get Started Now And Turn Your Intranet Into A Collaboration Platform
hol-info mailing list
hol-info <at> lists.sourceforge.net
Mitra Purandare | 16 Apr 14:18 2014

Second Call for Papers: International Conference on Formal Methods in Computer-Aided Design (FMCAD) 2014



International Conference on
Formal Methods in Computer-Aided Design (FMCAD)

Lausanne, Switzerland, October 21-24, 2014

The conference includes the FMCAD student forum;
it is collocated with MEMOCODE, DIFTS, and the
Hardware Model Checking Competition 2014 FMCAD Edition.

FMCAD 2014 has technical co-sponsorship from IEEE's CEDA
(Council on Electronic Design Automation) and
in-cooperation status with
ACM SIGPLAN (Special Interest Group on Programming Languages) and
ACM SIGSOFT (Special Interest Group on Software Engineering).


Abstract Submission: Tuesday, May 6
Paper Submission: Friday, May 16
Author Response Period: June 23-27
Author Notification: July 25
Camera-Ready Version: August 15
Conference: October 21-24


FMCAD 2014 is the 14th in a series of conferences on the
theory and application of formal methods in computer-aided
design and verification of computer systems and related
topics. FMCAD provides a leading international forum to
researchers and practitioners in academia and industry for
presenting and discussing novel methods, technologies,
theoretical results, tools, and open challenges in formal

FMCAD employs a rigorous peer-review process and is devoted
to maximizing the dissemination of papers.  Accepted papers
are distributed through both ACM and IEEE digital
libraries. In addition, published articles are made
available freely on the conference page and the authors
retain the copyright. There are no publication fees. At
least one of the authors is required to register for the
conference and present the accepted paper.

FMCAD 2014 will be co-located with MEMOCODE, the ACM/IEEE
International Conference on Formal Methods and Models for
Codesign, in Lausanne, Switzerland.  MEMOCODE will take
place from October 19 to 20, followed by a joint
FMCAD/MEMOCODE tutorial day on October 21.  FMCAD will
continue from October 22 to 24, 2014.


FMCAD welcomes submission of papers reporting original
research on advances in all aspects of formal methods
technology and its application to computer-aided design.
Topics of interest include, but are not limited to, the

-- Model checking, theorem proving, equivalence checking,
  abstraction and reduction, compositional methods,
  decision procedures at the bit- and word-level,
  probabilistic methods, combinations of deductive methods
  and decision procedures.

-- Synthesis and compilation for computer system
  descriptions, modeling, specification, and implementation
  languages, formal semantics of languages and their
  subsets, model-based design, design derivation and
  transformation, correct-by-construction methods.

-- Application of formal and semi-formal methods to
  functional and non-functional specification and
  validation of hardware and software, including timing and
  power modeling, verification of computing systems on all
  levels of abstraction, system-level design and
  verification for embedded and cyberphysical systems,
  hardware-software co-design and verification,
  transaction-level verification.

-- Experience with the application of formal and semi-formal
  methods to industrial-scale designs. Tools that represent
  formal verification enablement, new features, or a
  substantial improvement in the automation of formal

-- Application of formal methods in areas beyond computer
  systems, including formal methods describing processes
  studied in other areas of science, engineering, and


Submissions must be made electronically in PDF format
through a link available on the FMCAD web site


Two categories of papers can be submitted: regular papers (8
pages) and short papers (4 pages) containing ideas and
results that can be described succinctly.  Both regular and
short papers must use the IEEE Transactions format on
letter-size paper with a 10-point font size.

Submissions must contain original research that has not been
previously published, nor concurrently submitted for
publication. Any partial overlap with published or
concurrently submitted papers 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. Recently awarded papers include:

* "An SMT Based Method for Optimizing Arithmetic
 Computations in Embedded Software Code", Hassan Eldib and
 Chao Wang (2013)

* "A quantifier-free SMT encoding of non-linear hybrid
 automata", Alessandro Cimatti, Sergio Mover and Stefano
 Tonetta (2012)

* "An Incremental Approach to Model Checking Progress Properties",
 Aaron Bradley, Fabio Somenzi, Zyad Hassan and Yan Zhang (2011)

* "Applying SMT in Symbolic Execution of Microcode", Anders
 Franzen, Alessandro Cimatti, Alexander Nadel, Roberto
 Sebastiani, and Jonathan Shalev (2010)


FMCAD 2014 will host a Student Forum that provides a
platform for graduate students at any career stage to
introduce their research to the wider Formal Methods
community, and solicit feedback. Submissions for the event
must be short reports describing research ideas or ongoing
work that the student is currently pursuing, and must be
within the scope of FMCAD.  Work, part of which has been
previously published, will be considered; the novel aspect
to be addressed in future work must be clearly described in
such cases.

The event will consist of short presentations by the student
authors of each accepted submission, and of a poster that
will be on display throughout the duration of the
conference.  Accepted submissions will be listed, with title
and author name, in the event description in the conference
proceedings.  The authors will also have the option to
upload their poster and presentation to the FMCAD web site.

Limited funds will be available for travel assistance for
students with accepted contributions.

More details are available at


Submission Deadline: Sunday, June 08
Acceptance notification: Sunday, Aug 03
Forum date: Monday, Oct 20


The following meetings will be co-located with this year's edition:

-- MEMOCODE 2014, the ACM/IEEE International Conference on
  Formal Methods and Models for Codesign
  ( http://www.memocode-conference.com )

-- DIFTS 2014, International Workshop on Design and
  Implementation of Formal Tools and Systems
  ( http://fmgroup.polito.it/cabodi/difts2014/ )

-- We are also proud to host this year's
  Hardware Model Checking Competition 2014 FMCAD Edition


Koen Claessen, Chalmers University of Technology
Viktor Kuncak, EPFL

Viktor Kuncak, EPFL

Barbara Jobstmann, EPFL, Jasper DA, and CNRS/Verimag

Ruzica Piskac, Yale University

Mitra Purandare, IBM Research Lab, Zurich


Jason Baumgartner, IBM
Dirk Beyer, University of Passau
Armin Biere, Johannes Kepler University
Per Bjesse, Synopsys
Nikolaj Bjorner, Microsoft Research
Roberto Bruttomesso, Atrenta
Gianpiero Cabodi, Politecnico di Torino
Hana Chockler, King's College
Alessandro Cimatti, FBK-irst
Koen Claessen (Chair), Chalmers University of Technology
Bruno Dutertre, SRI International
Ziyad Hanna, Jasper Design Automation
Keijo Heljanko, Aalto University
Alan Hu, University of British Columbia
Warren Hunt, University of Texas
Susmit Jha, Strategic CAD Lab, Intel
Daniel Kroening, University of Oxford
Viktor Kuncak (Chair), EPFL
Panagiotis Manolios, Northeastern University
Ken McMillan, Microsoft Research
Katell Morin-Allory, TIMA Laboratory, Grenoble
Lee Pike, Galois, Inc.
Ruzica Piskac, Yale University
Mitra Purandare, IBM Research Lab, Zurich
Sandip Ray, Intel Corporation
Philipp Ruemmer, Uppsala University
Andrey Rybalchenko, Microsoft Research Cambridge
Julien Schmaltz, TU Eindhoven
Natasha Sharygina, Universita' della Svizzera Italiana
Anna Slobodova, Centaur Technology
Niklas Sorensson, Chalmers University of Technology
Daryl Stewart, ARM
Cesare Tinelli, The University of Iowa
Martin Vechev, ETH Zurich
Thomas Wahl, Northeastern University
Georg Weissenbacher, Vienna University of Technology


Jason Baumgartner, IBM, USA
Armin Biere, Johannes Kepler University in Linz, Austria
Alan Hu, University of British Columbia, Canada
Warren Hunt, University of Texas at Austin, USA
Start Your Social Network Today - Download eXo Platform
Build your Enterprise Intranet with eXo Platform Software
Java Based Open Source Intranet - Social, Extensible, Cloud Ready
Get Started Now And Turn Your Intranet Into A Collaboration Platform
hol-info mailing list
hol-info <at> lists.sourceforge.net

[fm-announcements] April 22, Extended SPIN 2014 deadline

The paper submission deadline for SPIN 2014 has been extended to April 22, 11:59PM AOE.

21st International Symposium on Model Checking of Software - SPIN 2014
             San Jose, CA, USA, July 21-23, 2014
             Joint Sessions with ISSTA on July 23rd

The SPIN Symposium is a leading forum for practitioners and
researchers interested in software verification and engineering. There
are two tracks for paper submissions.

              *** Software Verification Track  ***

We solicit submissions on theoretical techniques, novel algorithms and
empirical evaluation for state-space exploration based techniques. We
welcome submissions describing the development and application of
state space exploration techniques in testing and verifying embedded
software, mobile platforms, security-critical software, enterprise and
web applications, and other interesting software platforms.

         *** New this year: Software Engineering Track  ***

New this year we solicit submissions on techniques and approaches that
extend or leverage existing state-space exploration based techniques
such as model checking and symbolic execution to assist in automating
software engineering tasks such as design, implementation, analysis,
testing, and maintenance of software systems.

            Submission Guidelines

SPIN 2014 invites high quality contributions describing significant,
original, and unpublished results for submission in two categories:

   (a) Research papers describing fully developed work and complete
   results (10 pages)
   (b) Short papers describing tools, experience reports, descriptions
   of new ideas, or work in progress with preliminary results (4


            Important Dates

 Paper Submission: April 22, 2014 (11:59 PM AOE)
 Author Notification: May 23, 2014
 Camera-Ready Paper: June 16, 2014

            Invited Speakers

Karen Gundy-Burlet, NASA Ames Research Center, USA
Henny Sipma, Kestrel Technology, USA
Cormac Flanagan, UC Santa Cruz, USA (Joint speaker with ISSTA)

              Program Chairs

Neha Rungta, NASA Ames Research Center, USA
Oksana Tkachuk, NASA Ames Research Center, USA

            Program Committee

Ezio Bartocci,TU Wien, Vienna University of Technology, Austria
Dirk Beyer, University of Passau, Germany
Alastair Donaldson, Imperial College London, UK
Alex Groce, Oregon State University, USA
Arie Gurfinkel, Software Engineering Institute, CMU, USA
Gerard Holzmann, NASA/JPL, USA
Franjo Ivancic, NEC Laboratories America, Inc., USA
Sarfraz Khurshid, The University of Texas at Austin, USA
Shuvendu Lahiri, Microsoft Research, USA
Stefan Leue, University of Konstanz, Germany
Eric Mercer, Brigham Young University, USA
David Parker, University of Birmingham, UK
Suzette Person, NASA Langley Research Center, USA
Zvonimir Rakamaric, University of Utah, USA
C. R. Ramakrishna, Stony Brook University, USA
Robby, Kansas State University, USA
Scott Stoller, Stony Brook University, USA
Murali Talupur, Intel, USA
Suresh Thummalapenta, IBM Research, India
Jaco Van De Pol, University of Twente, Netherlands
Willem Visser, Stellenbosch University, South Africa
Michael Whalen, University of Minnesota, USA
To opt-out from this mailing list, send an email to

fm-announcements-request <at> lists.nasa.gov

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner <at> lists.nasa.gov 
Start Your Social Network Today - Download eXo Platform
Build your Enterprise Intranet with eXo Platform Software
Java Based Open Source Intranet - Social, Extensible, Cloud Ready
Get Started Now And Turn Your Intranet Into A Collaboration Platform
hol-info mailing list
hol-info <at> lists.sourceforge.net
Franck Cassez | 16 Apr 11:18 2014

ATVA 2014: Last Call for Papers -- Sydney November 3-7

[We apologise for duplicates.]
                   ATVA 2014 Call for Papers

          12th International Symposium on Automated
           Technology for Verification and Analysis

                   Sydney, November 3-7, 2014


Abstract submission:  NEW 19 April 2014
Paper submission:     NEW 27 April 2014


The purpose of ATVA is to promote research on theoretical and practical
aspects of automated analysis, verification and synthesis by providing
an international forum for interaction among the researchers in academia
and industry.

Abstract submission:  NEW 19 April 2014
Paper submission:     NEW 27 April 2014

Notification of acceptance:       30 June 2014
Final copy for proceedings:       30 July 2014
Conference:                       3-7 November 2014

ATVA 2014 solicits high quality submissions in areas related to the theory and
practice of automated analysis and verification of hardware and software systems.
Topics of interest include, but are not limited to:
Formalisms for modeling hardware, software and embedded systems
. Specification and verification of finite-state, infinite-state
and parameterized system
. Program analysis and software verification
. Analysis and verification of hardware circuits, systems-on-chip
and embedded systems
. Analysis of real-time, hybrid, timed, priced/weighted and probabilistic systems
. Deductive, algorithmic, compositional, and abstraction/refinement techniques
for analysis and verification
. Analytical techniques for safety, security, and dependability
. Testing and runtime analysis based on verification technology
. Synthesis and Games
. Analysis and verification of parallel and concurrent hardware/software systems
. Verification in industrial practice
. Applications and case studies
Theory papers should preferably be motivated by practical problems, and
applications should be based on sound theory and should solve problems of
practical interest.

ATVA invites research contributions in two categories: Regular research
papers (with 15 pages page limit) and tool papers (with 4 pages page limit).
Contributions must be written in English and in LNCS format, and must
present original research which is unpublished and not submitted elsewhere
(conferences or journals). The proceedings of ATVA 2014 will be
be published by Springer as a volume in the series of Lecture Notes in
Computer Science (LNCS). A special journal issue is also being planned
for selected papers.

  Pr. Krishnendu Chatterjee, IST Austria, Austria
  Pr. Ahmed Bouajjani, Univ. Paris Diderot, France

General Chair:
   Dr. Ralf Huuck (NICTA and UNSW)

Program co-chairs:
   Dr. Franck Cassez (NICTA and UNSW)
   Pr. Jean-François Raskin (ULB)

Workshop Chair:
   Dr. Peter Höefner (NICTA and UNSW)

Program committee:
   Ahmed Bouajjani (LIAFA, University Paris Diderot, France)
   Supratik Chakraborty (IIT Bombay, India)
   Alessandro Cimatti (FBK-irst, Italy)
   Deepak D'Souza (Indian Institute of Science, Bangalore, India)
   Hung Dang Van (UET, Vietnam National University, Hanoi)
   Giorgio Delzanno (DIBRIS, Università di Genova)
   E. Allen Emerson (The University of Texas at Austin, USA)
   Pierre Ganty (IMDEA Software Institute, Spain)
   Patrice Godefroid (Microsoft Research, USA)
   Kim Guldstrand Larsen (Aalborg University, Denmark)
   Teruo Higashino (Osaka University, Japan)
   Alan Hu (University of British Columbia, Canada)
   Joost-Pieter Katoen (RWTH Aachen University, Germany)
   Moonzoo Kim (KAIST, Korea)
   Gerwin Klein (NICTA and UNSW, Australia)
   Orna Kupferman (Hebrew University, Israel)
   Marta Kwiatkowska (University of Oxford, UK)
   Insup Lee (University of Pennsylvania, USA)
   Oded Maler (CNRS-VERIMAG, France)
   Annabelle McIver (Macquarie University, Australia)
   Madhavan Mukund (Chennai Mathematical Institute, India)
   Mizuhito Ogawa (Japan Advanced Institute of Science and Technology, Japan)
   Sungwoo Park Pohang (University of Science and Technology, Korea)
   Doron Peled (Bar Ilan University, Israel)
   Andreas Podelski (University of Freiburg, Germany)
   Pierre-Alain Reynier (Aix-Marseille University, France)
   Jie-Hong Rolland-Jiang (National Taiwan University Taipei, Taiwan)
   Jing Sun (The University of Auckland, New Zealand)
   P.S. Thiagarajan (National University of Singapore, Singapore)
   Ron Van Der Meyden (UNSW, Australia)
   Rob Van Glabbeek (NICTA and UNSW, Australia)
   Farn Wang (National Taiwan University Taipei, Taiwan)
   Chao Wang (Virginia Tech., USA)
   Bow-Yaw Wang (Academia Sinica, Taipei, Taiwan)
   Karsten Wolf (Rostock University, Germany)
   Hsu-Chun (Yen National Taiwan University, Taiwan)
   Wang Yi (Uppsala University, Sweden)
   Wenhui Zhang (Institute of Software, Chinese Academy of Sciences, China)

Steering Committee:
    Professor E. Allen Emerson (University of Texas at Austin)
    Professor Teruo Higashino (Osaka University)
    Professor Insup Lee (University of Pennsylvania)
    Professor Doron A. Peled (Bar Ilan Universioty)
    Professor Farn Wang (National Taiwan University)
    Professor Hsu-Chun Yen (National Taiwan University)


The information in this e-mail may be confidential and subject to legal professional privilege and/or
copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Start Your Social Network Today - Download eXo Platform
Build your Enterprise Intranet with eXo Platform Software
Java Based Open Source Intranet - Social, Extensible, Cloud Ready
Get Started Now And Turn Your Intranet Into A Collaboration Platform
Andreas Lochbihler | 15 Apr 15:57 2014

Two PhD positions in Information Security at ETH Zurich, Switzerland

The Information Security group headed by Prof. David Basin at ETH
Zurich has two open PhD positions in two projects:

(1) Formalizing computational soundness for protocol implementations
(2) Testing access control systems

We are looking for enthusiastic outstanding researchers with a strong
background and interest in one or more of the following areas:

- formal methods or mathematical logic,
- information security or cryptography,
- (project 1) interactive theorem proving
   (project 2) software testing.

Candidates with a strong theoretical background in related areas are
also encouraged to apply. ETH Zurich regulations require PhD
candidates to hold a Masters or equivalent degree (e.g. Diplom). The
preferred starting date for both positions is as soon as possible, at
the latest by the end of 2014.

Description of the projects:

(1) Formalizing computational soundness for protocol implementations,
     funded by the Swiss National Science Foundation

The project aims at a better understanding of, and more confidence in,
the security guarantees offered by symbolic analysis methods for
security protocols, e.g. TLS and IPsec. To this end, symbolic and
computational models of security protocols and security properties
will be formalized in the proof assistant Isabelle/HOL and linked with
computational soundness results. For more information see:

(2) Testing access control systems

The project aims at developing algorithms and tools for generating
security tests from formal access control policies, and assessing
their effectiveness. The position is within the Zurich Information
Security and Privacy Center (ZISC) and the successful candidate will
work closely with our industrial partner.

Applications should include a curriculum vitae, a brief description of
research interests, transcripts of grades, letters of recommendation
from teachers or employers, an indication of the preferred project,
and, if possible, the Master's or Bachelor's thesis and publications.
We will consider applications until the position is filled. Please


Applications and informal inquiries should be sent to Andreas
Lochbihler and Mohammad Torabi Dashti at the following email address:

     infsec.positions <at> inf.ethz.ch

PhD students are paid employees of ETH. Salary and employment
conditions are attractive. Zurich is a diverse and multicultural city
that is consistently rated among the best cities in the world in which
to live. Further information is available from the following links:

Open Positions at Institute of Information Security:

Institute of Information Security:

ETH Zurich:

City of Zurich:

Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
Ramana Kumar | 15 Apr 08:30 2014

INT_OF_NUM conversion

I'm about to write a conversion to reduce terms of the form Num(&n) where n is a ground non-negative integer. But I would expect such a thing to already exist somewhere - does anyone know where?

I notice that EVAL does not reduce Num(&1) - is there something I can load that will make it do so?
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
hol-info mailing list
hol-info <at> lists.sourceforge.net
Wendelin Serwe | 14 Apr 11:47 2014

FMICS 2014: submission still open


FMICS 2014
19th International Workshop on
Formal Methods for Industrial Critical Systems

11-12 September 2014, Florence, Italy

In co-location with EPEW, FORMATS, QEST, and SAFECOMP


The aim of the FMICS workshop series is to provide a forum for researchers who 
are interested in the development and application of formal methods in 
industry. In particular, FMICS brings together scientists and engineers that 
are active in the area of formal methods and interested in exchanging their 
experiences in the industrial usage of these methods. The FMICS workshop 
series also strives to promote research and development for the improvement of 
formal methods and tools for industrial applications.

Important Dates

     Paper submission: April 18th
     Notification: June 10th
     Final version due: June 27th
     Workshop: September 11th-12th

Topics of interest include (but are not limited to):

     Design, specification, code generation and testing based on formal methods.
     Methods, techniques and tools to support automated analysis, 
certification, debugging, learning, optimization and transformation of 
complex, distributed, real-time systems and embedded systems.
     Verification and validation methods that address shortcomings of existing 
methods with respect to their industrial applicability (e.g., scalability and 
usability issues).
     Tools for the development of formal design descriptions.
     Case studies and experience reports on industrial applications of formal 
methods, focusing on lessons learned or identification of new research directions.
     Impact of the adoption of formal methods on the development process and 
associated costs.
     Application of formal methods in standardization and industrial forums.

Paper Submission

Submissions must describe authors' original research work and results. 
Submitted papers must not have previously appeared in a journal or conference 
with published proceedings and must not be concurrently submitted to any other 
peer-reviewed workshop, symposium, conference or archival journal. Any partial 
overlap with any such published or concurrently submitted paper must be 
clearly indicated.

Submissions should clearly demonstrate relevance to industrial application. 
Case study papers should identify lessons learned, validate theoretical 
results (such as scalability of methods), or provide specific motivation for 
further research and development.

Submissions should not exceed 15 pages formatted according to the LNCS style 
(Springer), and should be submitted as Portable Document Format (PDF) files 
using the EasyChair submission site.

All submissions will be reviewed by the program committee who will make a 
selection among the submissions based on the novelty, soundness and 
applicability of the presented ideas and results. The proceedings of the 
workshop will be published in the Springer series Lecture Notes in Computer 
Science (LNCS). An USB stick with an electronic version of the proceedings 
will be distributed among participants during the workshop.

Participants will give a presentation of their papers in twenty minutes, 
followed by a ten-minute round of questions and discussion on participants' work.

Following the tradition of the past editions, a special issue of the journal 
Science of Computer Programming will be devoted to FMICS 2014.
Selected participants will be invited to submit an extended version of their 
papers after the workshop. These extended versions will again be reviewed by a 
program committee, which will decide on their final publication on the special 

Programme Committee

PC Chairs

     Francesco Flammini (Ansaldo STS, Italy)
     Frédéric Lang (Inria & LIG, France)

Publicity Chair

     Wendelin Serwe (Inria & LIG, France)

PC Members

     Maria Alpuente (Universitat Politècnica de València, Spain)
     Alvaro Arenas (IE University, Spain)
     Jiri Barnat (Masaryk University, Czech Republic)
     Cinzia Bernardeschi (University of Pisa, Italy)
     Simona Bernardi (Centro Universitario de la Defensa, AGM, Zaragoza, Spain)
     Jean Paul Blanquart (Astrium Satellites, France)
     Eckard Böde (Offis, Germany)
     Rocco De Nicola (IMT Lucca, Italy)
     Michael Dierkes (Rockwell Collins, France)
     Susanna Donatelli (University of Torino, Italy)
     Cindy Eisner (IBM Research - Haifa, Israel)
     Alessandro Fantechi (Università di Firenze, Italy)
     Jérôme Feret (CNRS & ENS & Inria, France)
     Wan Fokkink (Vrije Universiteit Amsterdam and CWI, Netherlands)
     Andrew Gacek (Rockwell Collins, USA)
     Stefania Gnesi (ISTI-CNR, Italy)
     Matthias Güdemann (Systerel, France)
     Keijo Heljanko (Aalto University, Finland)
     Jan Jürjens (TU Dortmund & Fraunhofer ISST, Germany)
     Tiziana Margaria (University of Potsdam, Germany)
     Pedro Merino (University of Málaga, Spain)
     Benjamin Monate (TrustInSoft, France)
     Gethin Norman (University of Glasgow, UK)
     Dave Parker (University of Birmingham, UK)
     Charles Pecheur (Université catholique de Louvain, Belgium)
     Ralf Pinger (Siemens AG, Germany)
     Wendelin Serwe (Inria & LIG, France)
     Hans Svensson (Quviq, Sweden)
     Jaco van de Pol (University of Twente, Netherlands)
     Valeria Vittorini (University of Naples Federico II, Italy)
     Angela Vozella (CIRA, Italy)

Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!