Geoff Sutcliffe | 2 Jul 16:35 2015

LPAR-20 Workshops - Calls for Papers

LPAR-20 call for workshop papers:
- Workshop on the Implementation of Logics(IWIL-2015)
- Models for Formal Analysis of Real Systems (MARS 2015)
- First International Workshop on Focusing (WoF'15)

                 Call for papers

    LPAR'20 Workshop on the Implementation of Logics

        SUBMISSION DEADLINE: 5 October 2015

General Information
The 11th International Workshop on the Implementation of Logics will be held in
November 2015 in conjunction with the 20th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning in Suva, Fiji

We are looking for contributions describing implementation techniques for and
implementations of automated reasoning programs, theorem provers for various
logics, logic programming systems, and related technologies. Topics of interest
include, but are not limited to:

  - Propositional logic and decision procedures, including SMT
(Continue reading)

Isabela Drămnesc | 3 Jul 18:26 2015

CFP PAS 2015

             PAS 2015 - Fourth International Seminar on
Program Verification, Automated Debugging and Symbolic Computation
                Beijing, China, October 21-23, 2015

Important Dates
  - Submission of abstracts                         August 15, 2015
  - Submission of papers/extended abstracts:        August 20, 2015
  - Notification of acceptance or rejection:     September 20, 2015
  - Final version due:                             October 10, 2015
  - Seminar taking place:                       October 21-23, 2015


PAS 2015 will provide a forum for researchers and software developers
actively involved or interested in developing, using, and applying
methods and software tools of symbolic computation for program
verification and automated debugging to exchange ideas and views, to
review the state of the art and discuss prospects, to present research
results and experiments,  and to build up contacts for future
cooperation. The scientific program of the seminar will feature
invited talks and contributed presentations.

Specific topics for PAS 2015 include (but are not limited to):

  - Theories and methodologies for program verification and testing
  - Model checking, fault locating and program repairing
  - Symbolic computation and automated reasoning for program verification
  - Termination, correctness and complexity analysis of programs
  - Automated program synthesis and transformation
  - Logic and semantics for automated and algorithmic debugging
(Continue reading)

Radomirovic Sasa | 26 Jun 12:28 2015

3 PhD positions in Information Security at ETH Zurich

The Institute of Information Security headed by Prof. David Basin at
ETH Zurich has three open positions for PhD students on research
projects in the following areas:

- Formal Verification of Secure Networking Systems
- Anonymity of Statistical Data
- Secure Human-Server Interaction

We are looking for enthusiastic outstanding Computer Science or
Mathematics students with a strong background in at least two of the
following topics

- formal methods or mathematical logic,
- probability theory and statistics, and
- information security.

Additionally, experience in the following specialized areas would be

- formal software development by refinement,
- experience with an interactive theorem prover, or
- security protocols.

ETH Zurich regulations require PhD students to hold a Masters or
equivalent degree (e.g., Diplom). All candidates matching the profile
above are encouraged to apply as soon as possible. We will process
applications until all positions are filled. Successful candidates are
expected to start soon after acceptance, but the starting date is

Applications should include:

- a curriculum vitae,
- a brief description of research interests,
- transcripts of grades,
- letters of recommendation from teachers or employers, and,
- if possible, the Master's or Bachelor's thesis and publications.

Applications and inquiries should be sent to Sasa Radomirovic at the
following email address.

  infsec.positions <at>

PhD students are paid employees of ETH Zurich. Salary and employment
conditions are attractive. Zurich is a diverse and multicultural city
which is consistently rated among the best cities in the world in
which to live.

Published end of June, 2015
Monitor 25 network devices or servers for free with OpManager!
OpManager is web-based network management software that monitors 
network devices and physical & virtual servers, alerts via email & sms 
for fault. Monitor 25 devices for free with no restriction. Download now;119417398;o
hol-info mailing list
hol-info <at>
Jasmin Blanchette | 28 Jun 23:26 2015

Open software engineer position at Inria Nancy

We are looking for a software engineer to fill a two-year full-time position at Inria Nancy - Grand-Est, to
work on a successor to Nitpick: a stand-alone higher-order model finder, written in OCaml. The tool will
target the hundreds of users of Isabelle/HOL, HOL4, HOL Light, and similar systems, to help them debug
their specifications. This model finder will be based on an SMT solver. Solid bases in functional
programming and experience with logic are prerequisites.

This position can be interesting for an outgoing Ph.D. student or a strong programmer with a master's
degree. Neither knowledge of French nor European citizenship are required. The monthly salary bracket
is about 2600 to 3200 EUR gross for Ph.D. holders (otherwise: 2100 to 2600 EUR). See

for more details or contact me directly.



Monitor 25 network devices or servers for free with OpManager!
OpManager is web-based network management software that monitors 
network devices and physical & virtual servers, alerts via email & sms 
for fault. Monitor 25 devices for free with no restriction. Download now;119417398;o

Summer School VTSA: 24-28 August 2015, Koblenz

Summer School on Verification Technology, Systems, and Applications
                           August 24-28, 2015,
            University Koblenz-Landau, Koblenz, Germany

The summer school Verification Technology, Systems, and Applications
(VTSA 2015) will be organized from August 24-28, 2015 at the
University Koblenz-Landau, Koblenz, Germany.
This is the eighth edition of a yearly school organized by Inria Nancy,
Max-Planck-Institut  für Informatik Saarbrücken, Université de Liège,
Université du Luxembourg  and this year also Universität Koblenz-Landau.

The following lecturers have agreed to give courses at VTSA 2015:

- Bernhard Beckert:
   Deductive Verification of Object-Oriented Software
- Stephanie Delaune:
   Verification of Security Protocols: from Confidentiality to Privacy
- Alberto Griggio:
   Exploiting SMT for Verification of Infinite-State Systems
- Tobias Schubert:
   SAT-based Approaches for Test and Verification of Integrated Circuits
- Mihaela Sighireanu:
   Modelling, Specification and Formal Analysis of Complex Software Systems

Participation to the school is free to anybody holding at least a bachelor
degree or equivalent; it includes the lectures, daily coffee and lunch
breaks, and a school dinner. Attendance is limited to 40 participants.
Please apply electronically by sending an email to
Eugen Denerz ( including

- a one-page CV,
- an application letter explaining the participant's interest in the
   school and any experience in the area, and
- a copy of the participant's bachelor certificate
  (or equivalent or a more significant certificate)

The deadline for application is July 17, 2015.
Notification of acceptance will be given by July 24, 2015.

Full details are available at

Monitor 25 network devices or servers for free with OpManager!
OpManager is web-based network management software that monitors 
network devices and physical & virtual servers, alerts via email & sms 
for fault. Monitor 25 devices for free with no restriction. Download now;119417398;o
hol-info mailing list
hol-info <at>
Marcel Kyas | 24 Jun 13:49 2015

Second Call for Workshop Proposals: 12th International Conference on integrated Formal Methods


12th International Conference on integrated Formal Methods, iFM 2016

June 1-5, 2016 - Reykjavík, Iceland



Prospective workshop organizers are invited to submit proposals for
workshops to be affiliated to iFM 2016, on topics related to the
conferences main subjects.

About iFM

iFM 2016 is concerned with how the application of formal methods may
involve modelling different aspects of a system which are best
expressed using different formalisms. Correspondingly, different
analysis techniques may be used to examine different system views,
different kinds of properties, or simply in order to cope with the
sheer complexity of the system. The iFM conference series seeks to
further research into hybrid approaches to formal modelling and
analysis; i.e., the combination of (formal and semi-formal) methods
for system development, regarding modelling and analysis, and covering
all aspects from language design through verification and analysis
techniques to tools and their integration into software engineering

One day workshops will be held in conjunction with the main events.
Prospective workshop organizers are requested to follow the guidelines
below and are encouraged to contact the workshop chairs if any
questions arise.

The purpose of the workshops is to provide participants with a
friendly, interactive atmosphere for presenting novel ideas and
discussing their application.

The workshops take place on June 4-5, 2016.

Important Dates
Submission of workshop proposals: by July 20, 2015
Notification: by August 3, 2015
Workshops: June 4-5, 2016

Submission via e-mail
Marcel Kyas <marcel <at>> - Workshop chair

Proposal and Submission Guidelines

Workshop proposals must be written in English, not exceed 5 pages with
a reasonable font and margins, and be submitted in PDF format via
email to Marcel Kyas (marcel <at>

Proposals should include:

* The name and the preferred date of the proposed workshop
* A short description of the workshop.
* If applicable, a description of past versions of the workshop,
  including dates, organizers, submission and acceptance counts, and
* The publicity strategy that will be used by the workshop organizers 
  to promote the workshop.
* The participant solicitation and selection process.
* The target audience and expected number of participants.
* Approximate budget proposal (see section Budget below for details).
* The equipment and any other resource necessary for the organization 
  of the workshop.
* The name and short CV of the organizer(s).
* The publication plan (only invited speakers, no published
  proceedings, pre-/post-proceedings published with EPTCS/ENTCS/...).

Organizers Responsibilities

The scientific responsibility of organizing a workshop goes to the
workshop organizers. In particular, they are responsible for the
following items:

* A workshop description (200 words) for inclusion n the iFM site.
* Hosting and maintaining web pages to be linked from the iFM
  site. Workshop organizers can integrate their pages into the main
  iFM pages.
* Workshop proceedings, if any. If there is sufficient interest, the 
  organizer of iFM 2016 may contact the editor-in-chief of the
  Electronic Proceedings in Theoretical Computer Science
  ( for having a common volume dedicated to the
  workshops of iFM 2016.
* Workshop publicity (possibly including call for papers, submission
  and review process).
* Scheduling workshop activities in collaboration with the iFM
  workshop chair.


The iFM organization will provide registration and organizational
support for the workshops (including link from the conferences web
sites, set-up of meeting space, on-line and on-site
registration). Registration fees must be paid for all participants,
including organizers and invited guests.

To cover lunches, coffee breaks and basic organizational expenses, all
workshops will be required to charge a minimum participation fee (the
precise amount is still to be determined). Each workshop may increase
this fee to cover additional expenses such as publication charges,
student scholarships, costs for invited speakers, etc. All fees will
be collected by the iFM organizers as part of the registration, then
additional funds will be redistributed to the individual workshop

Evaluation Process

The proposals will be evaluated by the iFM organizing committee on the
basis of their assessed benefit for prospective participants of iFM
2016. Prospective organizers may wish to consult the web pages of
previous satellite events as examples:

* iFM 2014:
* iFM 2013:
* iFM 2012:
* iFM 2010:
* iFM 2009:


iFM 2016 will take place at the Campus of Reykjavík University,
Iceland. The campus at Reykjavík University is set in one of the most
beautiful areas next to Iceland's only geothermal beach. The building
has well equipped classrooms.

Further Information and Enquiries
Please contact the workshop chair Marcel Kyas <marcel <at>>
Monitor 25 network devices or servers for free with OpManager!
OpManager is web-based network management software that monitors 
network devices and physical & virtual servers, alerts via email & sms 
for fault. Monitor 25 devices for free with no restriction. Download now;119417398;o
hol-info mailing list
hol-info <at>
Ramana Kumar | 25 Jun 08:01 2015

HOL workshop, August 2-3

Dear all,

I warmly invite you to participate in the upcoming HOL workshop, co-located with CADE. It promises to be an exciting opportunity to learn about, discuss, and work on the HOL theorem prover and the CakeML verified programming language, and to shape future developments and integrations with other theorem proving tools.

Everyone is welcome!

A draft program can be found on the workshop website:

Registration is via the CADE website:

I look forward to seeing you there.
Monitor 25 network devices or servers for free with OpManager!
OpManager is web-based network management software that monitors 
network devices and physical & virtual servers, alerts via email & sms 
for fault. Monitor 25 devices for free with no restriction. Download now;119417398;o
hol-info mailing list
hol-info <at>
Roberto Guanciale | 24 Jun 12:04 2015

PhD position in trustworthy embedded platforms, KTH - School of Computer Science and Communication, Stockholm, Sweden

(Apologies for cross-posting)

The theory group at KTH, School of Computer Science and Communication, invites applications for a PhD
position in trustworthy embedded platforms.

The recruitment is part of the creation of the new cross-departmental Center for Resilient Critical
Infrastructures, CERCES, which is concerned with the security and resilience of industrial control and
information systems. The center will focus on control systems, communication networks, wireless
communication, and embedded software verification. In this call, we are looking for highly-qualified
students that can contribute to the work on embedded software verification.

The student will join the Prosper team, a team of researchers led by Professor Mads Dam, with collaborators
at the Swedish Institute of Computer Science. For examples on ongoing projects, go to
and The present project focuses on the development of embedded software platforms,
kernels, hypervisors, drivers, and applications with very high demands on security, safety, and
trustworthiness, with particular focus on the critical infrastructure domain. We meet these demands
through formal modelling and verification, by building models of processors, systems, and devices, by
building theories and tools for low level verification, and by implementing and verifying critical
software components.

Application deadline: 10 July 2015

For details on the position, required qualifications, and application procedure, see

Contact persons for further information:

Mads Dam <mfd <at>>,
Roberto Guanciale <robertog <at>>,

Monitor 25 network devices or servers for free with OpManager!
OpManager is web-based network management software that monitors 
network devices and physical & virtual servers, alerts via email & sms 
for fault. Monitor 25 devices for free with no restriction. Download now;119417398;o
Georg Weissenbacher | 23 Jun 00:24 2015

FMCAD student forum: deadline extension (July 9)

The deadline for the FMCAD student forum has been
extended. The new deadline is July 09, 2015!!

            FMCAD 2015 STUDENT FORUM

FMCAD 2015, the fifteenth conference on the theory and
applications of formal methods in hardware and system
verification, will host the

               3rd FMCAD Student Forum
               (September 28-30, 2015)

providing a platform for graduate students at any career
stage to introduce their research to the wider Formal Methods


Submission Deadline: July 09, 2015
Acceptance notification: July 19, 2015
Forum date: September 28-30, 2015

Details are provided on

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.  All
submissions will be reviewed by a select group of program committee

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.
The best contribution (determined by the committee based
on the quality of the submission and the presentation)
will be given public recognition and a certificate at the event.

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

We kindly ask faculty members to help us advertise the event
by displaying the posters available from the web-page in
their departments.

If you have questions, please contact the forum chair
Georg Weissenbacher (Vienna University of Technology, Austria).

For more details visit

Monitor 25 network devices or servers for free with OpManager!
OpManager is web-based network management software that monitors 
network devices and physical & virtual servers, alerts via email & sms 
for fault. Monitor 25 devices for free with no restriction. Download now;119417398;o
rim.abid | 19 Jun 12:55 2015

Software Verification and Testing Track, ACM SAC 2016 (Pisa, Italy) - First CFP

31st Annual ACM Symposium on Applied Computing
Software Verification and Testing Track
April 3 - 8, 2016, Pisa, Italy

More information: and

Important dates

* September 11, 2015: Paper submission
* November 13, 2015: Paper notification
* December 11, 2015: Camera-Ready Copies

ACM Symposium on Applied Computing

The ACM Symposium on Applied Computing (SAC) has gathered scientists
from different areas of computing over the thirty years. The forum
represents an opportunity to interact with different communities
sharing an interest in applied computing.

SAC 2016 is sponsored by the ACM Special Interest Group on Applied
Computing (SIGAPP), and will be hosted by the University of Pisa and
Scuola Superiore Sant'Anna University, Italy

Software Verification and Testing Track

We invite authors to submit new results in formal verification and
testing, as well as development of technologies to improve the
usability of formal methods in software engineering. Also welcome are
detailed descriptions of applications of mechanical verification to
large scale software. Possible topics include, but are not limited to:

- model checking
- theorem proving
- correct by construction development
- model-based testing
- verification-based testing
- symbolic execution
- static and run-time analysis
- abstract interpretation
- analysis methods for dependable systems
- software certification and proof carrying code
- fault diagnosis and debugging
- verification of large scale software systems
- real world applications and case studies applying software  verification

Submissions Guidelines

Paper submissions must be original, unpublished work. Submissions
should be in electronic format, via the START site:

Author(s) name(s) and address(es) must not appear in the body of the
paper, and self-reference should be avoided and made in the third
person. Submitted paper will undergo a blind review process. Authors
of accepted papers should submit an editorial revision of their papers
that fits within six two-column pages (an extra two pages, to a total
of eight pages, may be available at a charge). Please comply to this
page limitation already at submission time. Accepted papers will be
published in the ACM SAC 2016 proceedings.

Paper registration is required, allowing the inclusion of papers,
posters, or SRC abstracts in the conference proceedings. An author or
a proxy attending SAC MUST present the work. This is a requirement for
the presented work to be included in the ACM/IEEE digital
library. No-show of registered papers, posters, and SRC abstracts will
result in excluding them from the ACM/IEEE digital library.

Student Research Competition

As before, SAC 2016 organises a Student Research Competition (SRC)
Program to provide graduate students the opportunity to meet and
exchange ideas with researchers and practitioners in their areas of
interest. Guidelines and information about the SRC program can be
found at Submission to
the SRC program should be in electronic form via the following website

Program Committee 

Rui Abreu, University of Porto, Portugal 
Cristiano Braga, Universidade Federal Fluminense, Brazil
Radu Calinescu, University of York, UK 
Ana Cavalli, National Institute of Telecommunications, France 
Byoungju Choi, Ewha Womans University, Republic of Korea 
Maximiliano Cristiá, Universidad Nacional de Rosario, Argentina 
Khaled El-Fakih, American University of Sharjah, UAE 
Ylies Falcone, University of Grenoble Alpes, France 
Maria del mar Gallardo, University of Malaga, Spain 
Arie Gurfinkel, Carnegie Mellon University, USA
Tingting Han, University of London, UK 
Klaus Havelund, Nasa Jet Propulsion Laboratory, USA
Ralf Huuck, UNSW, Australia
Nikolai Kosmatov, CEA, France 
Stefan Leue, University of Konstanz, Germany 
Luis Llana, Universidad Complutense de Madrid, Spain 
Jasen Markovski, R&D group, GN Resound Benelux, The Netherlands 
Mohammad Mousavi, Halmstad University, Sweden 
Madhavan Mukund, Chennai Mathematical Institute, India
Shin Nakajima, National Institute of Informatics, Tokyo, Japan 
Brian Nielsen, Aalborg University, Denmark 
Peter Olveczky, University of Oslo, Norway 
Jun Pang, University of Luxembourg, Luxembourg 
Adenilso Simao, ICMC/USP, Brazil
Marjan Sirjani, Reykjavik University, Iceland 
Marielle Stoelinga, University of Twente, The Netherlands 
Jun Sun, Singapore University of Technology and Design
Tanja Vos, Valencia University, Spain 
Carsten Weise, Imbus AG, Germany 
Anton Wijs, Eindhoven University of Technology, The Netherlands 
Nina Yevtushenko, Tomsk State University, Russia
Cemal Yilmaz, Sabanci University, Turkey 
Fatiha Zaidi, Univ. Paris-Sud, France 
Gianluigi Zavattaro, University of Bologna, Italy 
Lijun Zhang, Chinese Academy of Sciences, China

Program Committee Chairs

Mercedes G. Merayo, Universidad Complutense de Madrid, Spain
Gwen Salaün, University of Grenoble Alpes, France

hol-info mailing list
hol-info <at>
Rob van Glabbeek | 19 Jun 08:47 2015

Call for Papers: Models for Formal Analysis of Real Systems (MARS'15)

First Call for Papers:

                             Workshop on
              Models for Formal Analysis of Real Systems
                             (MARS 2015)

                       Affiliated With LPAR 20

                     November 23, 2015 Suva, Fiji

Aim: Logics and techniques for automated reasoning have often been
developed with formal analysis and formal verification in mind. To
show applicability, toy examples or tiny case studies are typically
presented in research papers. Since the theory needs to be developed
first, this approach is reasonable.
  However, to show that a developed approach actually scales to real
systems, large case studies are essential. The development of formal
models of real systems usually requires a perfect understanding of
informal descriptions of the system-sometimes found in RFCs or other
standard documents-which are usually just written in English. Based on
the type of system, an adequate specification formalism needs to be
chosen, and the informal specification translated into it. Abstraction
from unimportant details then yields an accurate, formal model of the
real system.
  The process of developing a detailed and accurate model usually takes
a large amount of time, often months or years; without even starting a
formal analysis. When publishing the results on a formal analysis in a
scientific paper, details of the model have to be skipped due to lack
of space, and often the lessons learnt from modelling are not
discussed since they are not the main focus of the paper.
  The workshop aims at discussing exactly these unmentioned lessons.
Examples are:

  * Which formalism is chosen, and why?
  * Which abstractions have to be made and why?
  * How are important characteristics of the system modelled?
  * Were there any complications while modelling the system?
  * Which measures were taken to guarantee the accuracy of the model?

The workshop emphasises modelling over verification. In particular, we
invite papers that present full Models of Real Systems, which may lay
the basis for future formal analysis. The workshop will bring together
researchers from different communities that all aim at verifying real
systems and are developing formal models for such systems. Areas where
large models often occur are within networks, (trustworthy) systems
and software verification (from byte code up to programming- and
specification languages). An aim of the workshop is to present
different modelling approaches and discuss pros and cons for each of them.


Submissions must be unpublished and not be submitted for publication elsewhere.
Contributions are limited to 8 pages EPTCS style (
(not counting the appendix), but shorter extended abstracts are welcome.
Appendices (of arbitrary length) can be used to present all details of
a formalised model; the appendices will be part of the proceedings.
Submissions must be in English and submitted in PDF format via EasyChair (TBC).

All submissions will be peer reviewed by at least three referees based
on their novelty, relevance and technical merit. The proceedings will be 
published as part of the open access series Electronic Proceedings 
in Theoretical Computer Science (EPTCS).


 * Submission of abstracts: Monday 24 August 2015
 * Submission: Monday 31 August 2015
 * Notification: Friday 9 October 2015
 * Final version: Monday 2 November 2015
 * Workshop: Monday 23 November 2015


Rance Cleaveland        (University of Maryland, USA)
Hubert Garavel          (INRIA, France)
Rob van Glabbeek  (co-chair) (NICTA, Sydney, Australia)
Jan Friso Groote  (co-chair) (Eindhoven University of Technology, The Netherlands)
He Jifeng               (Easy China Normal University, China)
Holger Hermanns         (Saarland University, Germany)
Peter Hoefner     (co-chair) (NICTA, Sydney, Australia)
Gerald Holzmann 	(NASA/JPL, USA)
Magnus Myreen 		(Chalmers University, Sweden)
Viet Yen Nguyen 	(Fraunhofer IESE, Germany)
Bill Roscoe 		(University of Oxford, UK)
Pamela Zave             (AT&T Laboratories, USA)


Rob van Glabbeek  (NICTA, Sydney, Australia)
Jan Friso Groote  (Eindhoven University of Technology, The Netherlands)
Peter Hoefner      (NICTA, Sydney, Australia)


   mars15 <at>