Ramana Kumar | 3 May 09:54 2016
Picon
Picon

Re: What is the advantage of HOL4?

Some strengths of HOL4 (off the top of my head, so maybe not comprehensive):
  • It is based on simple type theory. See "The seven virtues of simple type theory".
  • It is implemented in Standard ML. This is a formally specified programming language with multiple implementations.
  • It exposes APIs that make it relatively easy to write theorem-proving automation. It is highly programmable.
  • It can export proofs in a standard format (OpenTheory). It also has an implementation-independent representation of saved theories.
  • It is a suite of tools following the Unix philosophy.
  • It has reasonably large libraries and various big and interesting examples, including CakeML.
  • It is being actively improved and developed, and is free software.
  • It has reasonably thorough documentation (not perfect, but pretty good).

On 3 May 2016 at 17:34, Ada <956066427 <at> qq.com> wrote:
    Hi,guys
    I am working with HOL4. Recently, I read some papers, knowing that there are some other theorem provers, like PVS,COQ. They are similar in many aspects. For
example, the logic used by them is Higher order logic. I am wondering What is the advantage of HOL4?
    Thanks!

------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Nils Muellner | 28 Apr 11:41 2016
Picon
Picon

CFP Dependable Software Engineering (SETTA)

[Please accept our apologies if you receive multiple copies of this Call for Papers (CFP)]

Symposium on Dependable Software Engineering: Theories, Tools and Applications

 

Nov. 9-11, 2016, Beijing, China

 

IMPORTANT DATES (AoE)

* Abstract Submission: May 12, 2016

* Full Paper Submission: May 19, 2016

* Notification to Authors: Jul. 15, 2016

* Camera-ready Paper: Aug. 6, 2016

 

http://lcs.ios.ac.cn/setta/

 

Background and Objectives

 

The aim of the symposium is to bring together international researchers and practitioners in the field of software technology. Its focus is on formal methods and advanced software technologies, especially for engineering complex, large-scale artifacts like cyber-physical systems, networks of things, enterprise systems, or cloud-based services. Contributions relating to formal methods or integrating them with software engineering, as well as papers advancing scalability or widening the scope of rigorous methods to new design goals are especially welcome.

 

Being hosted in China, the symposium will also provide a platform for building up research collaborations between the rapidly growing Chinese computer science community and its international counterpart. The symposium will support this process through dedicated events and therefore welcomes both young researchers considering international collaboration in formal methods and established researchers looking for international cooperation and willing to attract new colleagues to the domain.

 

Authors are invited to submit papers on original research, industrial applications, or position papers proposing challenges in fundamental research and technology. The latter two types of submissions are expected to contribute to the development of formal methods either by substantiating the advantages of integrating formal methods into the development cycle or through delineating need for research by demonstrating weaknesses of existing technologies, especially when addressing new application domains.

 

Submissions can take the form of either normal or short papers. Short papers can discuss ongoing research at an early stage, including PhD projects. Papers should be written in English. Regular Papers should not exceed 15 pages and Short Papers should not exceed 6 pages in LNCS format. The proceedings will be published as a volume in Springer's LNCS series. The authors of a selected subset of accepted papers will be invited to submit extended versions of their papers to appear in a special issue of the Formal Aspects of Computing journal.

 

------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Manuel Hermenegildo | 30 Apr 17:25 2016

LOPSTR 2016 Call for Papers


======================================================================
                   LOPSTR 2016: 1st Call for Papers
======================================================================

                   26th International Symposium on
           Logic-Based Program Synthesis and Transformation
                             LOPSTR 2016

               http://cliplab.org/Conferences/LOPSTR16/

                  Edinburgh, UK, September 6-8, 2016
               (co-located with PPDP 2016 and SAS 2016)

======================================================================
DEADLINES:
Abstract submission: June 7,  2016
Paper/Extended abstract submission: June 14, 2016
======================================================================

The aim of the LOPSTR series is to stimulate and promote international
research and collaboration on logic-based program development.  LOPSTR
is  open to  contributions in logic-based  program development in  any
language  paradigm.   LOPSTR  has a  reputation for  being  a  lively,
friendly forum for presenting and discussing work in progress.  Formal
proceedings are produced only after the symposium so that authors  can
incorporate this feedback in the published papers.

The 26th International Symposium  on Logic-based Program Synthesis and
Transformation  (LOPSTR  2016)  will  be held  at  the  University  of
Edinburgh,  Edinburgh,  UK;  previous  symposia were  held  in  Siena,
Canterbury,  Madrid,  Leuven,  Odense, Hagenberg,  Coimbra,  Valencia,
Lyngby,  Venice,  London,  Verona, Uppsala,  Madrid,  Paphos,  London,
Venice, Manchester, Leuven, Stockholm, Arnhem, Pisa, Louvain-la-Neuve,
and  Manchester.   LOPSTR  2016  will be  co-located  with  PPDP  2016
(International  Symposium on  Principles and  Practice of  Declarative
Programming) and SAS 2016 (Static Analysis Symposium).

Topics  of   interest  cover   all  aspects  of   logic-based  program
development, all stages of the software life cycle, and issues of both
programming-in-the-small   and  programming-in-the-large.   Both  full
papers and  extended abstracts describing applications  in these areas
are especially  welcome. Contributions are  welcome on all  aspects of
logic-based program development, including, but not limited to:

    * synthesis
    * transformation
    * specialization
    * composition
    * optimization
    * inversion
    * specification
    * analysis and verification
    * testing and certification
    * program and model manipulation
    * transformational techniques in SE
    * applications and tools

Survey papers that present some aspects of the above topics from a new
perspective,  and application  papers  that  describe experience  with
industrial applications are also welcome.

Papers  must  describe original  work,  be  written and  presented  in
English, and must not substantially overlap with papers that have been
published  or   that  are  simultaneously  submitted   to  a  journal,
conference, or  workshop with refereed proceedings.  Work that already
appeared in  unpublished or informally published  workshop proceedings
may be submitted (please contact the PC chair in case of questions).

Important Dates

 Abstract submission:                            June 7, 2016
 Paper/Extended abstract submission:             June 14, 2016
 Notification:                                   August 3, 2016
 Camera-ready (for electronic pre-proceedings):  August 19, 2016
 Symposium:                                      September 6-8, 2016

Submission Guidelines

Authors  should submit  an electronic  copy of  the paper  (written in
English) in  PDF, formatted in  the Lecture Notes in  Computer Science
style. Each submission must include on its first page the paper title;
authors and their affiliations;  contact author's email; abstract; and
three  to  four keywords  which  will  be used  to  assist  the PC  in
selecting appropriate reviewers  for the paper. Page  numbers (and, if
possible, line  numbers) should appear  on the manuscript to  help the
reviewers in writing their report.  Submissions cannot exceed 15 pages
including references but excluding well-marked appendices not intended
for publication.  Reviewers  are not required to  read the appendices,
and thus papers should be intelligible without them.  Papers should be
submitted via the Easychair submission  website for LOPSTR 2016: 
http://www.easychair.org/conferences/?conf=lopstr2016
(can be accessed also through the LOPSTR 2016 web site).

Proceedings

The formal  post-conference proceedings will be  published by Springer
in the Lecture  Notes in Computer Science series.  Full  papers can be
directly  accepted  for  publication  in the  formal  proceedings,  or
accepted  only for  presentation  at the  symposium  and inclusion  in
informal  proceedings. After  the symposium,  all authors  of extended
abstracts  and full  papers  accepted only  for  presentation will  be
invited to revise and/or extend their  submissions in the light of the
feedback  solicited at  the symposium.  Then, after  another round  of
reviewing, these  revised papers may  also be published in  the formal
proceedings.

Program Committee

     Slim Abdennadher, German University of Cairo, Egypt
     Maria Alpuente, Universitat Politecnica de Valencia, Spain
     Sergio Antoy, Portland State University, USA
     Michael Codish, Ben-Gurion University of the Negev, Israel
     Jerome Feret, CNRS/ENS/INRIA Paris, France.
     Fabio Fioravanti, University of Chieti - Pescara, Italy.
     Maurizio Gabbrielli, University of Bologna, Italy
     Maria Garcia de la Banda, Monash University, Australia
     Robert Glueck, University of Copenhagen, Denmark.
     Miguel Gomez-Zamalloa, Complutense University of Madrid, Spain
     Gopal Gupta, University of Texas at Dallas, USA 
     Patricia Hill, Univ. of Leeds, UK 
     Jacob Howe, City University London, UK
     Viktor Kuncak , EPFL Lausanne, Switzerland
     Michael Leuschel, University of Duesseldorf, Germany
     Heiko Mantel TU Darmstadt, Germany
     Jorge A. Navas, NASA, USA
     Naoki Nishida, Nagoya University, Japan 
     Catuscia Palamidessi,  INRIA Saclay and LIX, France
     C.R. Ramakrishnan, SUNY Stony Brook, USA
     Vitor Santos Costa, Universidade do Porto, Portugal
     Hirohisa Seki, Nagoya Institute of Technology, Japan
     Peter Schneider-Kamp, University of Southern Denmark, Denmark

Program Chairs

    Manuel Hermenegildo, IMDEA Software Institute and T.U. Madrid (UPM)
    Pedro Lopez-Garcia, IMDEA Software Institute and CSIC

Organizing Committee

    James Cheney (University of Edinburgh, Local Organizer)
    Moreno Falaschi (University of Siena, Italy)

-----------------------------------------------------------------------------

------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
Martin Leucker | 26 Apr 11:06 2016
Picon

ICTAC 2016 - Paper submission closes on 9th of May 2016!


**********************************************************************

Paper submissions are welcome until 9 May, 2016, also from those that
did not submit an abstract.

**********************************************************************
CALL FOR PAPERS -- ICTAC 2016
13th International Colloquium on Theoretical Aspects of Computing
24-31 October 2016, Taipei, Taiwan, ROC
http://cc.ee.ntu.edu.tw/~ictac2016

DEADLINE FOR ABSTRACT SUBMISSIONS: 23 APRIL, 2016
**********************************************************************

ICTAC 2016 will be held in the Department of Electrical Engineering,
National Taiwan University, Taipei, Taiwan, ROC, during the period 24-31
October, 2016.

Established in 2004, the ICTAC conference series aims at bringing
together practitioners and researchers from academia, industry and
government to present research and to exchange ideas and experience
addressing challenges in both theoretical aspects of computing and in
the exploitation of theory through methods and tools for system
development. ICTAC also aims to promote cooperation in research and
education between participants and their institutions, from developing
and industrial countries.

THEMES AND TOPICS OF PAPERS

Topics of interest include theories of computation and programming,
foundations of software engineering and formal techniques in software
design and verification, as well as tools that support formal techniques
for system modeling, design and verification.

The topical areas of the conference include, but are not limited to
* Automata theory and formal languages;
* Principles and semantics of programming languages;
* Theories of concurrency, mobility and reconfiguration;
* Logics and their applications;
* Software architectures and their models, refinement and verification;
* Relationship between software requirements, models and code;
* Program static and dynamic analysis and verification;
* Software specification, refinement, verification and testing;
* Model checking and theorem proving;
* Models of object and component systems;
* Coordination and feature interaction;
* Integration of theories, formal methods and tools for engineering
computing systems;
* Service-oriented architectures: models and development methods;
* Models of concurrency, security, and mobility;
* Theory of distributed, grid and cloud computing;
* Real-time, embedded, hybrid and cyber-physical systems;
* Type and category theory in computer science;
* Models for learning and education;
* Case studies, theories, tools and experiments of verified systems;
* Domain-specific modeling and technology: examples, frameworks and
experience.
* Challenges and foundations in the environmental modeling and
monitoring, healthcare, and disaster management.

INVITED SPEAKERS

* Hsu-Chun Yen, National Taiwan University (TW)
* Leonardo de Moura, Microsoft (US)
* Heike Wehrheim, Universität Paderborn (DE)

ASSOCIATED EVENT

* ICTAC Summer School on Formal Methods (29-31 October, 2016)

IMPORTANT DATES

* Abstract submission: 23 April, 2016
* Paper submission: 1 May, 2016
* Author notification: 20 June, 2016
* Camera ready: Monday, 15 July, 2015

PAPER CATEGORIES AND FORMAT

We call for submissions, related to the above areas and topics,
according to the following three categories:
* Regular papers, with original research contributions;
* Short papers, on recent work or proposals of emerging challenges;
* Tool papers, on tools that support formal techniques for software
modeling, system design and verification. Submissions should adhere to
the LNCS format (see http://www.springer.de/comp/lncs/authors.html for
details). Regular papers should not exceed 18 pages. Short and tool
papers should not exceed 10 pages.

Submissions to the colloquium must not have been published or be
concurrently considered for publication elsewhere. All submissions will
be judged on the basis of originality, contribution to the field,
technical and presentation quality, as well as their relevance to the
conference.

SUBMISSION LINK

www.easychair.org/conferences/?conf=ictac2016

PROCEEDINGS

As for the past editions, the plan is to publish the proceedings of
ICTAC 2016 with Springer in the series Lecture Notes in Computer Science
(LNCS).

SPECIAL ISSUE

Extended versions of selected papers from ICTAC 2015 will be invited to
a special issue in a journal that will be announced later.

GENERAL CHAIR

* Farn Wang, National Taiwan University (TW)

PROGRAMME COMMITTEE CHAIRS

* Augusto Sampaio, Universidade Federal de Pernambuco, Brazil
* Farn Wang, National Taiwan University, Taiwan

PROGRAMME COMMITTEE

* Bernhard Aichernig, TU Graz, Austria
* Farhad Arbab, CWI and Leiden University, Netherlands
* Mauricio Ayala-Rincón, Universidade de Brasilia, Brazil
* Mário Benevides, Universidade Federal do Rio de Janeiro, Brazil
* Ana Cavalcanti, University of York, UK
* Yu-Fang Chen, Academia Sinica, Taiwan
* Gabriel Ciobanu, Institute of Computer Science, Romania
* Hung Dang-Van, Vietnam National University, Vietnam
* Rocco DeNicola, Institute for Advanced Studies Lucca, Italy
* Razvan Diaconescu, IMAR, Romania
* Jin-Song Dong, National University of Singapore, Singapore
* José Fiadeiro, University of London, UK
* John Fitzgerald, Newcastle University, UK
* Marcelo Frias, Buenos Aires Institute of Technology, Argentina
* Martin Fränzle, Universität Oldenburg, Germany
* Lindsay Groves, Victoria University of Wellington, New Zeland
* Zhenjiang Hu, NII, Japan
* Jie-Hong Jiang, National Taiwan University, Taiwan
* Cliff Jones, Newcastle University, UK
* Luis Lamb, Universidade Federal do Rio Grande do Sul, Brazil
* Kim Larsen, Aalborg University, Denmark
* Martin Leucker, University of Lübeck, Germany
* Zhiming Liu, Southwest University in Chongqing, China
* Ana Melo, Universidade de São Paulo, Brazil
* Dominique Méry, Université de Lorraine, France
* Alexandre Mota, Universidade Federal de Pernambuco, Brazil
* Mohammad Mousavi, Halmstad University, Sweden
* Tobias Nipkow, TU München, Germany
* José Oliveira, Universidade do Minho, Portugal
* Catuscia Palamidessi, INRIA, France
* Paritosh Pandya, Tata Institute of Fundamental Research, India
* António Ravara, Universidade Nova de Lisboa, Portugal
* Camilo Rueda, Universidad Javeriana, Colombia
* Jacques Sakarovitch, CNRS / Telecom ParisTech, France
* Augusto Sampaio (PC co-chair), Universidade Federal de Pernambuco, Brazil
* Martin Schaef, SRI International, US
* Sven Schewe, University of Liverpool, UK
* Emil Sekerinski, McMaster University, Canada
* Hiroyuki Seki, Nagoya University, Japan
* Tetsuo Shibuya, University of Tokyo, Japan
* Andrzej Tarlecki, Warsaw University, Poland
* Kazunori Ueda, Waseda University, Japan
* Frank Valencia, Ecole Polytechnique, France
* Farn Wang (PC co-chair), National Taiwan University, Taiwan
* Jim Woodcock, University of York, UK
* Hsu-Chun Yen, National Taiwan University, Taiwan
* Shoji Yuen, Nagoya University, Japan
* Naijun Zhan, Chinese Academy of Sciences, China
* Lijun Zhang, Chinese Academy of Sciences, China
* Huibiao Zhu, East China Normal University, China

STERRING COMMITTEE

* Ana Cavalcanti, University of York, UK
* Martin Leucker, University of Luebeck, Germany
* Zhiming Liu,  Southwest University  in Chongqing, China
* Tobias Nipkow, Technical University Munich, Germany
* Augusto Sampaio, Federal University of Pernambuco, Brazil
* Natarajan Shankar, SRI International, US
------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Mayo, Jackson | 30 Apr 01:30 2016
Picon

CFA: HCCV 2016 - Workshop on High-Consequence Control Verification

CALL FOR ABSTRACTS

Workshop on High-Consequence Control Verification

http://www.sandia.gov/hccv/

July 18, 2016 - Toronto, Ontario, Canada

In conjunction with the 28th International Conference on Computer Aided
Verification (venue and registration information will be available at
http://i-cav.org/2016/).

Abstract submissions describing practical applications of high-consequence
control verification are especially encouraged.

DATES

Abstract submission (1 page maximum): May 18, 2016
Notification: May 25, 2016
Workshop: July 18, 2016

PRELIMINARY PROGRAM

Confirmed invited speaker:
Sanjit Seshia (University of California, Berkeley)

Additional contributors:
Karla Morris (Sandia/California) and Colin Snook (University of Southampton)
Philip Johnson-Freyd (University of Oregon)
Aadithya Karthik (Sandia/New Mexico)
Lee Pike (Galois, Inc.)
Toby Wilkinson and Michael Butler (University of Southampton)

SCOPE

The Workshop on High-Consequence Control Verification (HCCV) focuses on formal
methods concepts and techniques to ensure the highest levels of reliability,
safety, and security for digitally controlled devices, including the effects
of possibly extreme physical environments. The workshop targets applications
where the severe consequences of failure justify extraordinary investments not
appropriate for less critical devices -- including special methodologies at
the design stage to enable verifying stringent reliability, safety, and
security requirements in the resulting devices under both nominal and
out-of-nominal (fault) conditions. Such needs exist in domains including
defense, medical devices, and scientific instrumentation.

The willingness to make greater investments for small but high-consequence
devices can provide an opportunity to leverage emerging, more powerful formal
methods techniques that may currently be considered too costly for
"mainstream" industrial applications. Novel ideas for design and analysis
techniques that promote in-depth verifiability are of strong interest for
these high-consequence digital controllers. The HCCV workshop offers a new
forum for engagement among formal methods researchers, tool developers, and
practitioners.

Topics of interest include:

  * Theory and techniques for formally verified high-consequence digital
    design (via model checking and/or theorem proving), such as:
      - Abstraction/refinement
      - Correct-by-construction synthesis
      - Exhaustive or probabilistic analysis of fault consequences
      - Incorporation of analog physics

  * Applications to safety-critical digitally controlled devices in domains
    such as:
      - Defense
      - Medical
      - Supervisory control and data acquisition (SCADA)

Important notes:

  * Submissions should target requirements for high-consequence devices, *not*
    general-purpose software verification or cybersecurity.

  * Submissions should target mathematical analyzability of designs, *not
    merely* testing- and simulation-based verification or the use of standard
    electronic design automation (EDA) tools.

SUBMISSION

Abstracts of up to 1 page in PDF format should be submitted at
https://easychair.org/conferences/?conf=hccv2016 on or before May 18, 2016.
Each accepted abstract will be allotted a speaking slot. The collection of
accepted abstracts will be made available for download from the workshop
website.

ORGANIZERS

Jackson R. Mayo (co-chair)
Sandia National Laboratories
Livermore, California, United States
jmayo <at> sandia.gov

Michael J. Butler (co-chair)
University of Southampton, United Kingdom
mjb <at> ecs.soton.ac.uk

------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
Alexander Romanovsky | 30 Apr 12:48 2016
Picon
Picon

ISSRE 2016 - Call for Submissions

*********************************************************************
CALL FOR SUBMISSIONS

The 27th IEEE International Symposium on Software Reliability Engineering
(ISSRE 2016)
October 23rd - 27th, 2016 - Ottawa, Canada
http://issre.net/

*********************************************************************
SUMMARY OF IMPORTANT DATES
*********************************************************************
Research Paper Abstract Submission:	 		May 6th, 2016
Research Papers Submission: 				May 13th, 2016
Workshop Proposal Submission: 				April 22nd, 2016
Tutorial Proposal Submission: 				July 1st, 2016
Industry Paper Submission: 				July 29th, 2016
Doctoral Symposium Paper Submission: 			August 5th, 2016
Fast Abstract Paper Submission: 			August 5th, 2016

For further information on the call for submissions, please see
http://issre.net/call-for-papers

ISSRE is the premium conference that focuses on the theory and practice of
software systems reliability engineering. Over the past 20+ years we have
grown to be recognized as the voice of software reliability. From its
humble beginnings in 1990, it has become a conference that has a unique
element to it: a rare combination of strong research and industry
participation.
Unlike the conferences which are either centred academically or
industrially, we are a rich combination of both! In recent years, our data
tells us that we are almost evenly split. This is a huge accomplishment
for any conference. And, this was no accident. The core leadership of the
conference has targeted this goal and created programs that allow the top
tier of research and industry to interact on issues of current importance.
That we have actually approached this target over the past five to eight
years is of immense satisfaction to us. Our gratitude is to you, the
participant, for helping us create this unique community.

*********************************************************************
Topics of interests
*********************************************************************
ISSRE 2016 is focused on innovative techniques and tools for assessing,
predicting, and improving the reliability, safety, and security of
software products. ISSRE also emphasizes industrial relevance, rigorous
empirical studies and experience reports on existing software systems.
ISSRE covers a broad range of topics. The list below identifies several,
but certainly not all:

* Reliability, availability and safety of software systems
* Validation and Verification
* Faults, errors, failures, defects, bugs
* Software quality and productivity
* Software security
* Dependability, survivability, fault tolerance and resilience of software
systems
* Systems (hardware + software) reliability engineering
* Metrics and measurements, estimation, prediction of quality/reliability
* Services reliability engineering
* Open source software reliability engineering
* Web 2.0 reliability, availability and security issues
* Supporting tools and automation
* Industry best practices
* Software as a Service
* Virtualization and software reliability
* Reliability of mobile devices and applications
* Green and Sustainable Software engineering
* Reliability of Big Data and Internet of Things
* Empirical studies of any of the above topics
* Software Standards

*********************************************************************
Call for Research papers
*********************************************************************
The main research track at ISSRE 2016 is soliciting original, unpublished
research papers in three categories: (1) full research (regular) papers,
(2) practical experience reports, and (3) wild and provocative ideas (WAP)
papers. Papers will be assessed with criteria appropriate to each
category. ISSRE looks for works exploring new territory, continuing a
significant research, or reflecting on practical experience. While full
research manuscripts should explore a specific technology problem and
propose a complete solution to it, with extensive experimental results,
practical experience reports are expected to provide an in-depth
exposition of practitioner experiences and empirical studies. On the other
hand, WAP papers are expected to present either work currently in progress
or less developed but highly innovative ideas related to areas relevant to
ISSRE, aiming at inspiring discussion among conference attendees and
getting people thinking about open research challenges. Submissions will
be judged on originality, significance, correctness and impact. Authors
will have a chance to rebut the reviews within 800 words over the period
of July 10th to July 12th.
There will be a best paper award given to a paper in the main research
track. Full research papers and practical experience reports are eligible
for the award. Extended versions of selected papers will be invited for
potential publication in a special issue of the Journal of Systems and
Software (JSS - pending approval).

FORMATTING GUIDELINES
Papers must be written in English, and be formatted according to the IEEE
Computer Society Format Guidelines. Papers that exceed the page limits
specified below, or are outside the scope of the symposium, or do not
follow the formatting guidelines will be rejected without review.
Manuscript page lengths (all in double column, IEEE conference style format):

Research papers: 10 pages + 2 pages (for references and appendices)

Experience reports: 10 pages + 2 pages (for references and appendices)

WAP papers: 6 pages

*********************************************************************
ALL IMPORTANT DATES
*********************************************************************
Call for Research Papers
Abstract submission: 					May 6, 2016
Full paper submission: 					May 13, 2016
Rebuttal period: 					July 10-12, 2016
Notification: 						July 20, 2016
Camera ready paper: 					August 21, 2016

Call for Workshops Proposals
Proposal submission: 					April 22, 2016
Notification: 						May 8, 2016
Paper Submission: 					July 29, 2016
Paper Notification: 					Aug 19, 2016
Camera ready paper:					Aug 28, 2016

Call for Tutorials proposals
Proposal Submission: 					July 1, 2016
Notification: 						July 15, 2016

Call for Industry Papers
Short paper submission: 				July 29, 2016
Abstract/Presentation Submission: 			August 15, 2016
Notification short paper: 				August 19, 2016
Notification abstract/presentation: 			August 28, 2016
Camera ready (short paper only): 			Aug 28, 2016

Call for Doctoral Symposium Papers
Paper submission: 					August 5, 2016
Notification: 						August 19, 2016
Camera ready paper:					August 28, 2016

Call for Fast Abstract Papers
Paper Submission: 					August 5, 2016
Notification: 						August 19, 2016
Camera ready paper: 					August 28, 2016

*********************************************************************
Organization Committee
*********************************************************************
General Chair
Yvan Labiche, Carleton University, Canada

Program Committee Chairs
Alexander Romanovsky, Newcastle University, United Kingdom
Elena Troubitsyna, Åbo Akademi University, Finland

Finance Chair
Guy-Vincent Jourdan, University of Ottawa, Canada

Program Managers
Juan Carlos Ruiz, Universitat Politecnica de Valencia, Spain
Karthik Pattabiraman, University of British Columbia, Canada

Workshop Chair
Sudipto Ghosh, Colorado State University, USA

Industry Track Chairs
Sigrid Eldh, Ericsson, Sweden
Brian Robinson, ABB, USA

Tutorial Chair
Sunita Chulani, Cisco Systems, USA

Fast Abstract Chair
Jeremy Bradbury, University of Ontario Institute of Technology, Canada

Doctoral Symposium Chair
Tanja Vos, Universidad Politecnica de Valencia, Spain

Publication Chair
Hadi Hemmati, University of Manitoba, Canada

Publicity Chair
Damiano Torre, Carleton University, Canada

Local Arrangement Chair
Cheryl Schramm, Carleton University, Canada

Web Chair
Sunint Kaur Khalsa, Carleton University, Canada

*********************************************************************
Steering Committee: http://issre.net/steering-committee

Program Committee: http://issre.net/program-committee

*********************************************************************

------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
Geoff Sutcliffe | 29 Apr 21:11 2016
Picon

PAAR 2016 - Extended Deadline

LAST CALL FOR PAPERS AND DEADLINE EXTENSION

PAAR-2016 - 5th Workshop on Practical Aspects of Automated Reasoning
July 2nd, 2016.  Coimbra, Portugal

Abstract Deadline: May 2nd, 2016
Full Paper Deadline (extended): May 9th, 2016
http://cs.ru.nl/paar16/

General Information

  The 5th Workshop on Practical Aspects of Automated Reasoning will
  be held on July 2nd, 2016 in Coimbra, Portugal.  PAAR is associated
  with the 8th International Joint Conference on Automated Reasoning
  (IJCAR-2016).

Scope

  PAAR provides a forum for developers of automated reasoning
  tools to discuss and compare different implementation
  techniques, and for users to discuss and communicate their
  applications and requirements. The workshop will bring
  together different groups to concentrate on practical aspects
  of the implementation and application of automated reasoning
  tools. It will allow researchers to present their work in
  progress, and to discuss new implementation techniques and
  applications.

Topics include but are not limited to:
    o automated reasoning in propositional, first-order,
      higher-order and non-classical logics;
    o implementation of provers (SAT, SMT, resolution, tableau,
      instantiation-based, rewriting, logical frameworks, etc);
    o automated reasoning tools for all kinds of practical
      problems and applications;
    o pragmatics of automated reasoning within proof assistants;
    o practical experiences, usability aspects, feasibility
      studies;
    o evaluation of implementation techniques and automated
      reasoning tools;
    o performance aspects, benchmarking approaches;
    o non-standard approaches to automated reasoning,
      non-standard forms of automated reasoning, new
      applications;
    o implementation techniques, optimisation techniques,
      strategies and heuristics, fairness;
    o support tools for prover development;
    o system descriptions and demos. 

  We are particularly interested in contributions that help the
  community to understand how to build useful reasoning systems
  in practice, and how to apply existing systems to real
  problems.

Paper Submissions

  Researchers interested in participating are invited to submit either
  an extended abstract (up to 8 pages) or a regular paper (up to 15
  pages) via EasyChair at
  https://easychair.org/conferences/?conf=paar2016. Submissions will
  be refereed by the program committee, which will select a balanced
  program of high-quality contributions. Short submissions that could
  stimulate fruitful discussion at the workshop are particularly
  welcome.

  Submissions should be prepared in LaTeX using the EasyChair proceedings
  style. The package containing the class file and its user guide and
  some helper tools can be downloaded from
  http://www.easychair.org/publications/easychair.zip. PAAR proceedings
  will be published electronically in the EasyChair Proceedings in
  Computing (EPiC) series.

Important Dates

  Abstract submission deadline: May 2nd, 2016 (Anywhere on the planet)
  Paper submission deadline: May 9th, 2016 (Anywhere on the planet)
  Notification: May 30th, 2016
  Camera ready versions due: June 6th, 2016
  Workshop: July 2nd, 2016

Program Committee

  June Andronick, NICTA and University of New South Wales, Australia
  Peter Baumgartner, NICTA/Australian National University, Australia
  Christoph Benzmüller, Freie Universität Berlin, Germany
  Armin Bierre, Johannes Kepler University, Austria
  Nikolaj Bjorner, Microsoft Research, USA
  Simon Cruanes, Loria, INRIA, France
  Hans de Nivelle, University of Wroclaw, Poland
  Pascal Fontaine, Loria, INRIA, University of Lorraine, France (co-chair)
  Vijay Ganesh, University of Waterloo, Canada
  Alberto Griggio, FBK-IRST, Italy
  John Harrison, Intel, USA
  Marijn Heule, The University of Texas at Austin, USA
  Dejan Jovanović, SRI International, USA
  Yevgeny Kazakov, The University of Ulm, Germany
  Chantal Keller, LRI, Université Paris-Sud, France
  Boris Konev, The University of Liverpool, UK
  Konstantin Korovin, The University of Manchester, UK
  Laura Kovacs, Chalmers University, Sweden
  Jens Otten, University of Potsdam, Germany
  Nicolas Peltier, CNRS - LIG, France
  Ruzica Piskac, Yale University, USA
  Giles Reger, The University of Manchester, UK
  Andrew Reynolds, EPFL, Switzerland
  Philipp Ruemmer, Uppsala University, Sweden
  Ulrike Sattler, The University of Manchester, UK
  Renate A. Schmidt, The University of Manchester, UK
  Stephan Schulz, DHBW Stuttgart, Germany (co-chair)
  Geoff Sutcliffe, University of Miami, USA
  Josef Urban, Radboud University, Nijmegen, The Netherlands (co-chair)
  Uwe Waldmann, MPI Saarbrücken, Germany

------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Osman Hasan | 26 Apr 16:45 2016
Picon

CFP FTSCS 2016: FTSCS 2016 5th International Workshop on Formal Techniques for Safety-Critical Systems, Tokyo, November 14/15, 2016

---------------------------------------------------------------------
                       Call for Papers

                          FTSCS 2016

5th International Workshop on Formal Techniques for Safety-Critical Systems

                   Tokyo, November 14/15, 2016
              (satellite workshop of ICFEM 2016)

                    http://www.ftscs.org

---------------------------------------------------------------------

*** Science of Computer Programming special issue ***
*** Springer CCIS proceedings ***


Aims and Scope:

There is an increasing demand for using formal methods to validate and
verify safety-critical systems in fields such as power generation and
distribution, avionics, automotive systems, and medical systems. In
particular, newer standards, such as DO-178C (avionics), ISO 26262
(automotive systems), IEC 62304 (medical devices), and CENELEC EN
50128 (railway systems), emphasize the need for formal methods and
model-based development, thereby speeding up the adaptation of such
methods in industry.

The aim of this workshop is to bring together researchers and engineers
who are interested in the application of formal and semi-formal methods
to improve the quality of safety-critical computer systems. FTSCS
strives to promote research and development of formal methods and
tools for industrial applications, and is particularly interested in
industrial applications of formal methods. 

Specific topics include, but are not limited to:

* case studies and experience reports on the use of formal methods for
  analyzing safety-critical systems, including avionics, automotive,
  medical, railway, and other kinds of safety-critical and QoS-critical systems
* methods, techniques and tools to support automated analysis,
  certification, debugging, etc., of complex safety/QoS-critical systems
* analysis methods that address the limitations of formal methods in
  industry (usability, scalability, etc.)
* formal analysis support for modeling languages used in industry,
  such as AADL, Ptolemy, SysML, SCADE, Modelica, etc.
* code generation from validated models.

The workshop will provide a platform for discussions and the exchange of
innovative ideas, so submissions on work in progress are encouraged.


Submission:

We solicit submissions reporting on:

A- original research contributions (15 pages max, LNCS format);
B- applications and experiences (15 pages max, LNCS format);
C- surveys, comparisons, and state-of-the-art reports (15 pages max, LNCS);
D- tool papers (5 pages max, LNCS format);
E- position papers and work in progress (5 pages max, LNCS format)

related to the topics mentioned above.


All submissions must be original, unpublished, and not submitted
concurrently for publication elsewhere. Paper submission is done
The final version of the paper must be prepared in LaTeX, adhering to
the LNCS format available at


Publication:

All accepted papers will appear in the pre-proceedings of FTSCS 2016.
Accepted papers in the categories A-D above will appear in the
workshop proceedings that will be published as a volume in
Springer's CCIS series. 

The authors of a selected subset of accepted papers will be invited to
submit extended versions of their papers to appear in a special issue
of the Science of Computer Programming journal.


Important dates:

Submission deadline: September 4, 2016
Notification of acceptance: October 7, 2016
Workshop: November 14/15, 2016


Venue:

Tokyo, Japan


Program chairs:

Cyrille Artho        AIST, Japan
Peter Olveczky       University of Oslo, Norway


Program committee:

Etienne Andre        University Paris 13, France
Toshiaki Aoki        JAIST, Japan
Cyrille Artho        AIST, Japan
Kyungmin Bae         Pohang University of Science and Technology, Korea
Eun-Hye Choi         AIST, Japan
Alessandro Fantechi  University of Florence and ISTI-CNR, Pisa, Italy
Bernd Fischer        Stellenbosch University, South Africa
Osman Hasan          National University of Sciences & Technology, Pakistan
Klaus Havelund       NASA JPL, USA
Jerome Hugues        Institute for Space and Aeronautics Engineering, France
Marieke Huisman      University of Twente, The Netherlands
Ralf Huuck           Synopsys, Australia
Fuyuki Ishikawa      National Institute of Informatics, Japan
Takashi Kitamura     AIST, Japan
Alexander Knapp      Augsburg University, Germany
Thierry Lecomte      ClearSy System Engineering, France
Yang Liu             Nanyang Technological University, Singapore
Robi Malik           University of Waikato, New Zealand
Frederic Mallet      INRIA Sophia Antipolis, France
Roberto Nardone      University of Napoli "Federico II", Italy
Vivek Nigam          Federal University of Paraíba, Brazil
Thomas Noll          RWTH Aachen University, Germany
Kazuhiro Ogata       JAIST, Japan
Peter Olveczky       University of Oslo, Norway
Charles Pecheur      Universite catholique de Louvain, Belgium
Markus Roggenbach    Swansea University, UK
Ralf Sasse           ETH Zurich, Switzerland
Martina Seidl        Johannes Kepler University, Austria
Oleg Sokolsky        University of Pennsylvania, USA
Sofiene Tahar        Concordia University, Canada
Carolyn Talcott      SRI International, USA
Tatsuhiro Tsuchiya   Osaka University, Japan
Andras Voros         Budapest University of Technology and Economics, Hungary
Chen-Wei Wang        State University of New York (SUNY), Korea
Alan Wassyng         McMaster University, Canada
Michael Whalen       University of Minnesota, USA
Huibiao Zhu          East China Normal University, China


Contact:



--
Osman Hasan, Ph.D.
Head of Department (Research),
Location: A.307 Faculty Block
School of Electrical Engineering and Computer Science,
NUST, Sector H12, Islamabad, Pakistan.
Voice : +92.51.90852137
Web: ohasan.seecs.nust.edu.pk
------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Roberto Guanciale | 26 Apr 15:53 2016
Picon
Picon

PhD position in Formal Modelling and Verification for High Assurance

We are seeking candidates for a PhD position in the department of computer
science at KTH Royal Institute of Technology. The position is fully funded and
is part of a larger research project led by Professor Mads Dam.
Our research vision is to produce embedded software platforms that have
mathematically guaranteed security properties through the use of formal modelling and verification.

We are looking for highly-qualified students that can contribute to the work on formal modelling
of processor microarchitecture and on software verification. The student will be involved in
(i) modelling the effects of low-level system components using interactive theorem provers,
(ii) validating the formal models by checking their adherence with the real hardware,
and (iii) verifying the effectiveness of new and existing countermeasures for the security threats that
exploit the system components.

KTH Royal Institute of Technology in Stockholm is the largest and oldest technical university in Sweden.
No less than one-third of Sweden’s technical research and engineering education capacity at
university level is provided by KTH. 

The application deadline is 30 May 2016. The starting date is open for discussion.
Ideally we would like the successful candidate to start September 2016.

The full advertisement can be found at

https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:98977/where:4/

Roberto Guanciale

------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
Peter Schueller | 21 Apr 23:15 2016
Picon
Gravatar

Final CFP and Deadline Extension ICLP 2016, New York City: 32nd International Conference on Logic Programming, Oct 17-21


                 Final Call For Papers and Deadline Extension
              32nd International Conference on Logic Programming

                              New York City, USA
                             October 17-21, 2016

               http://software.imdea.org/Conferences/ICLP2016/

Conference Scope

Since  the first conference held in Marseilles in 1982, ICLP has been the pre-
mier international conference for presenting research  in  logic  programming.
Contributions  are sought in all areas of logic programming, including but not
restricted to:

 - Theory: Semantic Foundations, Formalisms, Nonmonotonic Reasoning, Knowledge
   Representation.

 - Implementation: Compilation, Virtual Machines, Parallelism, Constraint Han-
   dling Rules, Tabling.

 - Environments: Program Analysis, Transformation,  Validation,  Verification,
   Debugging, Profiling, Testing.

 - Language  Issues:  Concurrency,  Objects,  Coordination,  Mobility,  Higher
   Order, Types, Modes, Assertions, Programming Techniques.

 - Related Paradigms: Inductive and Co-inductive Logic Programming, Constraint
   Logic Programming, Answer-Set Programming, SAT-Checking.

 - Applications:  Databases,  Big Data, Data Integration and Federation, Soft-
   ware Engineering,  Natural  Language  Processing,  Web  and  Semantic  Web,
   Agents, Artificial Intelligence, Bioinformatics, and Education.

In  addition  to  the  presentations of accepted papers, the technical program
will include invited talks, advanced tutorials, the doctoral  consortium,  and
several workshops.

Important Dates

Paper registration (abstract):       29 April, 2016  (extended deadline, firm)
Submission deadline:                 6 May, 2016     (extended deadline)
Notification to authors:             17 June, 2016
Revision deadline (when needed):     8 July, 2016
Final notification:                  22 July, 2016
Camera-ready copy due:               5 Aug, 2016
Conference:                          17-21 Oct, 2016

Submission Details

Submissions  of  regular papers must be made in the condensed TPLP format (see
http://software.imdea.org/Conferences/ICLP2016/TPLP-ICLP-2016.tar)  via  Easy-
Chair  (see  http://www.easychair.org/conferences/?conf=iclp2016).   A regular
paper must not exceed 14 pages including the bibliography, but the  paper  may
be  supplemented  with  appendices for proofs and details of datasets which do
not count towards this limit and which will be available as appendices to  the
published paper. We accept three kinds of papers:

 - Technical  papers  for technically sound, innovative ideas that can advance
   the state of logic programming;

 - Application papers that impact interesting application domains;

 - System and tool papers which emphasize  novelty,  practicality,  usability,
   and availability of the systems and tools described.

Application, system, and tool papers need to be clearly marked in their title.
All submissions must be written in English and describe  original,  previously
unpublished research, and must not simultaneously be submitted for publication
elsewhere.  Papers of the highest quality will be selected to be published  in
the journal of Theory and Practice of Logic Programming (TPLP), Cambridge Uni-
versity Press (CUP). In order to ensure the  quality  of  the  final  version,
papers  may  be subject to more than one round of refereeing (within the deci-
sion period).

The program committee may recommend some papers to be published  as  technical
communications.  Technical  communications (TCs) will be published by Dagstuhl
Publishing   in   the    OpenAccess    Series    in    Informatics    (OASIcs)
(http://www.dagstuhl.de/publikationen/oasics/).   These  TC  papers should not
exceed 14 pages including bibliography.  Authors can  also  elect  to  convert
their  submissions  into extended abstracts, of 2 or 3 pages, for inclusion in
the TCs.  This should allow authors to submit a long version  elsewhere.   All
regular papers and regular TCs will be presented during the conference.

Doctoral  consortium position papers, of between 10 and 14 pages, will also be
published as TCs.

Authors of accepted papers will, by default, be automatically included in  the
list  of  ALP  members, who will receive quarterly updates from the Logic Pro-
gramming Newsletter at no cost.

Conference Organization

General Chairs:

Michael         Kifer           Stony Brook University, USA
Neng-Fa         Zhou            City University of New York, USA

Program Chairs:

Manuel          Carro           UPM and IMDEA Software Institute, Spain
Andy            King            University of Kent, UK

Workshop Chair:

Marcello        Balduccini      Drexel University, USA

Publicity Chair:

Peter           Schueller       Marmara University, Turkey

Doctoral Consortium Chairs:

Marina          De Vos          University of Bath, UK
Neda            Saeedloei       University of Minnesota Duluth, USA

Programming Contest Chair:

Paul            Fodor           Stony Brook University, USA

Web Presence:

Joaquin         Arias           IMDEA Software Institute, Spain

Program Committee:

Marcello        Balduccini      Drexel University, USA
Mutsunori       Banbara         Kobe University, Japan
Roman           Bartak          Charles University, Czech Republic
Pedro           Cabalar         University of Corunna, Spain
Mats            Carlsson        SICS, Sweden
Manuel          Carro           UPM and IMDEA Software Institute, Spain
Michael         Codish          Ben-Gurion University of the Negev, Israel
Marina          De Vos          University of Bath, UK
Agostino        Dovier          Universita degli Studi di Udine, Italy
Gregory         Duck            National University of Singapore, Singapore
Esra            Erdem           Sabanci University, Turkey
Wolfgang        Faber           University of Huddersfield, UK
Thom            Fruehwirth      University of Ulm, Germany
John            Gallagher       Roskilde University, Denmark, and
                                IMDEA Software Institute, Spain
Marco           Gavanelli       Universita degli Studi di Ferrara, Italy
Martin          Gebser          University of Potsdam, Germany
Michael         Hanus           CAU Kiel, Germany
Katsumi         Inoue           NII, Japan
Gerda           Janssens        KU Leuven - University of Leuven, Belgium
Andy            King            University of Kent, UK
Ekaterina       Komendantskaya  Heriot-Watt University, UK
Michael         Leuschel        University of Dusseldorf, Germany
Vladimir        Lifschitz       University of Texas, USA
Jose F.         Morales         IMDEA Software Institute, Spain
Enrico          Pontelli        New Mexico State University, USA
Jorg            Puhrer          Leipzig University, Germany
Ricardo         Rocha           University of Porto, Portugal
Zoltan          Somogyi         Independent Researcher, Australia
Harald          Sondergaard     University of Melbourne, Australia
Theresa         Swift           NOVALINKS, US, and UNL, Portugal
Francesca       Toni            Imperial College London, UK
Irina           Trubitsyna      University of Calabria, Italy
Mirek           Truszczynski    University of Kentucky, USA
Alicia          Villanueva      Universitat Politecnica de Valencia, Spain
Jan             Wielemaker      VU University Amsterdam, Netherlands
Stefan          Woltran         TU Wien, Austria
Fangkai         Yang            Schlumberger Inc., USA
Jia-Huai        You             University of Alberta, Canada

Workshops

The ICLP 2016 program will include several workshops.  They  are  perhaps  the
best  places  for  the  presentation of preliminary work, underdeveloped novel
ideas, and new open problems to a wide and interested audience with opportuni-
ties for intensive discussions and project collaboration.

Autumn School on Computational Logic

A  school on computational logic is planned.  More up to date information will
be available at the conference Web page.

Doctoral Consortium

The Twelfth Doctoral Consortium (DC) on Logic Programming  provides  research
students  with  the  opportunity  to present and discuss their research direc-
tions, and to obtain feedback from  both  peers  and  experts  in  the  field.
Accepted  participants  will  receive  partial financial support to attend the
event and the main conference. The best paper from the DC will  be  given  the
opportunity to present in a session of the main ICLP conference.

Conference Venue

The  venue  will  be  the  Sheraton LaGuardia East Hotel in Flushing, New York
City.  New York City is an international  tourist  destination,  receiving  56
million  tourists in 2014 alone. Several sources have ranked New York the most
photographed city in the world. Times square, known as the  city's  heart,  is
the  brightly  illuminated hub of the Broadway theatre district. The Statue of
Liberty greets new arrivals to the Americas by ship in the late 19th and early
20th century, and is a globally recognized symbol of the United States. Flush-
ing is associated by many with the  National  Tennis  Centre,  since  Flushing
Meadows  has  been  the home of the US Open Grand Slam tennis tournament every
year since 1978.

New York is the most populous city in the United States and one  of  the  most
populous  urban  agglomerations  in  the world. Situated in one of the world's
largest natural harbours, New York City consists of  five  boroughs,  each  of
which is a separate county of New York State. The conference hotel is situated
in the Queens borough, just a two-minute walk from  the  Flushing-Main  Street
rail station.  Direct train lines take you directly from there to Times Square
in just over 45 minutes, which is fast for New York City. The Museum of Modern
Art  can  be  reached in under 40 mins, Grand Central Terminal in 40 mins, the
Empire State Building under 50 mins, and The High Line Park in 50 minutes.

The hotel is also close to LaGuardia Airports and JFK.  LaGuardia  is  just  3
miles  away  and  the  hotel  offers a complementary shuttle service.  John F.
Kennedy International Airport (JFK) is 10 miles away and can be reached within
30  minutes  by  taxi.  The hotel is situated in a vibrant Asian district that
offers a variety of Eastern cuisine, as well as many stores and shops.

Sponsor

The conference is sponsored by the Association for Logic Programming (ALP).

Financial Assistance

The Association for Logic Programming has funds to assist  financially  disad-
vantaged  participants  and, especially, students to enable them to attend the
conference.  Inquiries should be made to the general chairs.

------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
Barbara Kordy | 22 Apr 11:50 2016
Picon

Ph.D. Position in Security Modeling at IRISA in Rennes, France

Looking for a Ph.D. thesis that combines computer security and mathematics?
IRISA, the computer science laboratory of Rennes in France, seeks to 
hire an
outstanding Ph.D. student to perform research in the field of formal 
modeling
and analysis of security. The position is within the project entitled
"Attack-Defense Trees for Computer Security: Formal Modeling of 
Preventive and
Reactive Countermeasures".

Description of work
---------------------
Attack-defense trees constitute a methodology to represent how an attacker
may compromise a system and how a defender can protect it against potential
attacks. The project's objective is to increase the expressive power of
attack-defense trees by integrating reactive countermeasures into the 
formalism.
The main tasks of the Ph.D. student will be to
- Develop mathematical foundations for attack-defense trees distinguishing
   between protective and reactive countermeasures;
- Propose quantitative evaluation techniques for attack-defense trees with
   protective and reactive countermeasures;
- Validate the extended model in real-life case studies performed in 
collaboration
   with industry;
- Co-supervise master students.

A detailed description of the thesis topic is available at
http://people.irisa.fr/Barbara.Kordy/vacancies.php

Candidate's profile
--------------------
The candidate is expected to have:
- A Master degree in computer science or mathematics;
- A proven interest in formal methods and formal modeling;
- Excellent written and oral English skills.

Background in computer security will be a plus. Knowledge of French is 
not required.

Work environment
-----------------
We offer a three year appointment funded by the French Ministry of Higher
Education and Research. The successful candidate will participate in the
activities of the Embedded Security and Cryptography (EMSEC) research team
(http://www.irisa.fr/emsec/) co-led by Prof. Dr. Gildas Avoine and Prof. 
Dr.
Pierre-Alain Fouque. The student will be supervised jointly by Dr. Barbara
Kordy (http://people.irisa.fr/Barbara.Kordy/) and Prof. Gildas Avoine
(http://www.avoine.net/).

IRISA (https://www.irisa.fr/en) is located in Rennes at the heart of the
beautiful Brittany region in the north-west of France. Rennes is situated
60km from the Atlantic Ocean, 60km from the UNESCO World Heritage Site of
Mont Saint-Michel, and 70km from the charming city of Saint Malo. Direct
high-speed rail service (TGV) connects Rennes with the center of Paris
within 2 hours and with the France's largest international airport
Paris Charles de Gaulle (CDG) within 3 hours.

Application
---------------
Applications should be written in English and include the following 
documents:
- Motivation letter clearly explaining the candidate's interest in the 
proposed
   topic and his/her fit to the position;
- Curriculum Vitae (including contact information, education and work 
experience,
   short description of the master thesis, list of publications, etc.);
- Transcript of grades from all university-level courses taken;
- Contact information for 2 referees.

Applications will be considered on a rolling basis until the position is 
filled.
Documents should be submitted by e-mail to Dr. Barbara Kordy 
(barbara.kordy <at> irisa.fr).

Contact information
-----------------------
For further inquiries please contact Dr. Barbara Kordy 
(barbara.kordy <at> irisa.fr)

For more information about this vacancy please check
http://people.irisa.fr/Barbara.Kordy/vacancies/PhD_16.pdf

------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z

Gmane