Wednesday, November 11, 2015

Machines virtuelles pour le B événementiel

http://www.researchgate.net/publication/228364789_Machines_virtuelles_pour_le_B_vnementiel

Jean-Raymond Abrial at ICTAC 2015

http://www.ictac2015.co/http://www.ictac2015.co/

One ot the invited speakers :

Jean-Raymond Abrial

Consultant (France)

Jean-Raymond Abrial
Jean-Raymond Abrial is a French computer scientist, widely known as the co-inventor of various formal approaches to software specification: Z, B and Event-B.
He is the author of the "B-book" (Cambridge University Press, 1996), which presents the B-Method. More recently, he published the book "Modeling in Event-B: System and Software Engineering" (Cambridge University Press 2010). He was Guest Professor at ETH Zurich from 2004 to 2007, where he led the team developing the Rodin Platform tool for Event-B (funded by the European Project "Rodin"). After that, he was a researcher, also at ETH Zurich, working on the European Project "Deploy" until May 2009.
Jean-Raymond Abrial has been invited to give courses on formal methods in various Chinese Universities (Peking University in Beijing, East China Normal University in Shanghai). Before Zurich, he was a consultant for more than 20 years working in close contact with several industrial companies and universities around the world.

Friday, September 18, 2015

ABZ 2016

http://www.cdcc.faw.jku.at/ABZ2016/call4papers/

The ABZ conference is dedicated to the cross-fertilization of six related state-based and machine-based formal methods, Abstract State Machines (ASM), Alloy, B, TLA, VDM and Z, that share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and software systems. It builds on the success of the first ABZ conference held in London in 2008, where the ASM, B and Z conference series merged into a single event, the second ABZ 2010 conference held in Orford (Canada), where the Alloy community joined the event, the ABZ 2012 held in Pisa (Italy), which saw the inclusion of the VDM community, and ABZ 2014 held in Toulouse (France), which brought the inclusion of the TLA community into the ABZ conference series. The ABZ 2016 conference will be held in Linz, Austria.
Contributions are solicited on all aspects of the theory and applications of ASMs, Alloy, B, TLA, VDM, Z approaches in software/hardware engineering, including the development of tools and industrial applications. The program spans from theoretical and methodological foundations to practical applications, emphasizing system engineering methods and tools that are distinguished by mathematical rigor and have proved to be industrially viable. The main goal of the conference is to contribute to the integration of accurate state- and machine-based system development methods, clarifying their commonalities and differences to better understand how to combine different approaches for accomplishing the various tasks in modeling, experimental validation, mathematical verification of reliable high-quality hardware/software systems.
Although organized to host several formal methods with ASM, Alloy, B, TLA, VDM and Z, in a single event, editorial control of the joint conference is vested in one integrated program committee, which will respectively determine its ASM, Alloy, B, TLA, VDM and Z content, to be presented in parallel conference tracks with a schedule to allow the participants to switch between the sessions.
As successfully practiced at ABZ 2014, the 5th edition of ABZ will include again special sessions dedicated to a shared real-life case study among all the methods addressed in ABZ 2016. The objective of this session is to enrich the set of case studies developed with ABZ methods with a practical and real-life case study. After the success of the “Landing Gear” case study at ABZ 2014 in the aeronautical context this time the organizers defined a real-life case study issued from the medical domain with challenging safety requirements. The ABZ 2016 case study emphasizes the control of a hemodialysis machine. See http://www.cdcc.faw.jku.at/ ABZ2016/HD-CaseStudy.pdf for a detailed description of this case study.

Submission of Papers

Proposals are invited for workshops and tutorials to take place before the main conference.
Four kinds of contributions are invited:
  • Research papers: full papers of not more than 14 pages in LNCS format, which have to be original, unpublished and not submitted elsewhere.
  • Short presentations of work in progress, and tool demonstrations. This is an excellent opportunity for Ph.D. students to present and validate their work in progress. An extended abstract of not more than 4 pages is expected and will be reviewed.
  • Answers to case study papers: full papers of not more than 14 pages in LNCS format reporting on the experiments conducted with any of the state based techniques in the scope of ABZ 2016.
  • Application in industry papers reporting on work or experiences on the application of state based formal methods in industry. An extended abstract of not more than 4 pages is expected and will be reviewed. It is also an interesting option for industrial practitioners who sometimes face too many constraints to prepare a full paper.
Contributions should be submitted electronically in PDF at the ABZ 2016 conference submission website (Easy Chair).
The papers must be prepared using the SPRINGER LNCS style. The answers to case study should be submitted electronically in PDF at the ABZ 2016 case study submission website (Easy Chair)".
All research and short accepted papers will be published in a volume of Springer's LNCS series. The answers to case study papers and the application in industry papers will be published in a volume of Springer's CCIS series. The two volumes will be distributed at the conference.

Journal Special Issues

It is planned that an improved version of a selected number of contributions will be published in a special issue of the journal Science of Computer Programming for the research papers and in a special issue of the Software Tools and Technology Transfer journal for the answers to case study papers (to be confirmed).

Workshop Proposals

Workshops and tutorials will be associated to the main event ABZ. Proposals are solicited in areas related to the conference topics. Workshop proposal should be sent to the workshop chairs.
The deadline for submissions is October 16, 2015. Notifications will be sent by November 6, 2015.

Tutorial Proposals

Tutorial proposal should be sent to the tutorial chairs.
The deadline for submissions is February 15, 2016. Notifications will be sent by March 14, 2016.

Important Dates

Research paper and answers to case study submission:January 15, 2016
Short paper submission:February 04, 2016
Workshop proposal submissions:October 16, 2015
Workshop proposal notifications:November 06, 2015
Tutorial proposal submissions:February 15, 2016
Acceptance notification:February 22, 2016
Tutorial proposal notifications:March 14, 2016
Final Version due:March 14, 2016
Main ABZ 2016 conference:May 23-27, 2016

Program Committee Chairs

  • Michael BUTLER, University of Southampton, Southampton, UK
  • Klaus-Dieter SCHEWE, Johannes-Kepler-Universität Linz and Software Competence Center Hagenberg, Linz/Hagenberg, Austria

Case Study Chairs

Tutorial Chairs

Workshop Chairs

Program Committee

Program committee will be announced at a later date.

Conference Organizers


For questions concerning ABZ 2016, contact Klaus-Dieter SCHEWE (Klaus-Dieter.Schewe@scch.at).

Wednesday, June 17, 2015

Conférence de J-R Abrial au Collège de France, avril 2015

 http://www.college-de-france.fr/site/gerard-berry/seminar-2015-04-01-17h30.htm

Spécification, construction et vérification de programmes : le parcours d'une pensée scientifique sur une trentaine d'années

Monday, March 2, 2015

2015 Refinement Workshop at FM 2015 in Oslo

Call for Papers: 2015 Refinement Workshop at FM 2015 in Oslo

22 June 2015, colocated with FM 2015 at Oslo

www.refinenet.org.uk/ref15/

Refinement is one of the cornerstones of a formal approach to software
engineering: the process of developing a more detailed design or
implementation from an abstract specification through a sequence of
mathematically-based steps that maintain correctness with respect to the
original specification.

The aim of this BCS FACS Refinement Workshop, is to bring together
people who are interested in the development of more concrete designs or
executable programs from abstract specifications using formal notations,
tool support for formal software development, and practical experience
with formal refinement methodologies.

The purpose of the workshop is to provide a forum for the exchange of
ideas, and discussion of common ground and key differences.

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

    Simulation techniques
    Foundations and semantics
    Case studies (specification and verification)
    Compositional and modular reasoning
    Object-orientation
    Time, Probability, Hybrid Systems
    Specification notations
    Programming models
    Verification and tool support

Proceedings

Submissions will be reviewed, workshop proceedings will be published,
likely in Electronic Proceedings in Theoretical Computer Science, like
the 2013 and 2011 editions.

It is anticipated that selected papers from this workshop will be published
in extended versions in a special edition of a major international journal,
in line with the special issues in FACJ and SCP that have appeared for
workshop editions since 2003.

Key Dates

    Abstract Submission: 21 March 2015
    Paper Submission: 28 March 2015
    Notification: 22 April 2015
    Workshop: 22 June 2015

Submissions

Submissions can be made via EasyChair:
https://easychair.org/conferences/?conf=ref2015.
There is no prescribed format for submissions but accepted papers will
need to use the EPTCS LaTeX macro package, see EPTCS info for authors:
http://info.eptcs.org/
Papers should be no more than 16 pages.

History of the workshop

This 17th Refinement Workshop continues a long tradition in refinement
workshops run under the auspices of the British Computer Society (BCS)
FACS special interest group. Running since 1988, previous refinement
workshops have been held at Cambridge, London, Bath etc.

In 1998 the BCS refinement workshop was combined with the Australasian
Refinement Workshop to form the International Refinement Workshop,
hosted alongside Formal Methods Pacific 1998 at The Australian National
University. In 2002, the Refinement Workshop was held as an FME workshop
in Copenhagen. This and seven subsequent editions (Surrey, Macau,
Oxford, Turku, Eindhoven, Limerick, Turku) have had proceedings in ENTCS
or EPTCS and a subsequent journal special issue or selected journal
papers (most in Formal Aspects of Computing, once in Science of Computer
Programming). For more details, see here.

The Workshop Webpage is available from www.refinenet.org.uk

Program committee

    Eerke Boiten, University of Kent, UK (co-chair)
    John Derrick, University of Sheffield, UK (co-chair)
    Steve Reeves, University of Waikato, NZ (co-chair)
    Richard Banach, University of Manchester, UK
    Luis Barbosa, University of Minho, PT
    Ana Cavalcanti, University of York, UK
    Brijesh Dongol, Brunel University, UK
    Steve Dunne, UK
    Lindsay Groves, Victoria University of Wellington, NZ
    Stefan Hallerstede, Aarhus University, DK
    Marcel Oliveira, Universidade Federal do Rio Grande do Norte, Brazil
    Gerhard Schellhorn, Augsburg University, Germany
    Steve Schneider , University of Surrey, UK
    Emil Sekerinski, McMaster University, Canada
    Graeme Smith, University of Queensland, Australia
    Helen Treharne, University of Surrey, UK
    Heike Wehrheim, University of Paderborn, Germany
_______________________________________________

ATVA 2015, 13th International Symposium on Automated Technology for Verification and Analysis

ATVA 2015, 13th International Symposium on Automated Technology for
Verification and Analysis
  October 12-15, 2015, Shanghai, China, http://atva2015.ios.ac.cn/


BACKGROUND
The purpose of ATVA is to promote research on theoretical and
practical aspects of automated analysis, verification and synthesis
by providing a forum for interaction between the regional and the
international research communities and industry in the field.


SCOPE
ATVA 2015 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 systems
* Program analysis and software verification
* Analysis and verification of hardware circuits, systems-on-chip and
embedded systems
* Analysis of real-time, hybrid, 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
* 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.


IMPORTANT DATES
April 22, 2015        Abstract submission deadline (AOE)
April 25, 2015        Paper submission deadline (AOE)
May 5, 2015        Submission of workshop proposals
Jun 8, 2015        Paper acceptance/rejection notification
Jun 10, 2015        Announcement of the accepted papers
July 5, 2015        Camera-ready copy deadline

GENERAL CHAIR
Jifeng He (East China Normal University, China)

PROGRAMME CHAIRS
Bernd Finkbeiner (Saarland University, Germany)
Geguang Pu (East China Normal University, China)
Lijun Zhang (Institute of Software, Chinese Academy of Sciences)

PUBLICITY CHAIRS
David N. Jansen (Radboud Universiteit, Netherlands)
Huibiao Zhu (East China Normal University, China)

PROGRAM COMMITTEE
Alessandro Abate (University of Oxford, UK)
Erika Ábrahám (RWTH Aachen University, Germany)
Michael Backes (Saarland University, Germany)
Christel Baier (Technical University of Dresden, Germany)
Ahmed Bouajjani (University Paris Diderot, FR)
Tevfik Bultan (University of California at Santa Barbara, USA)
Franck Cassez (NICTA, Australia)
Rance Cleaveland (University of Maryland, USA)
Hung Dang-Van (UET, Vietnam National University, Vietnam)
Bernd Finkbeiner (Saarland University, Germany)
Mark Greenstreet (University of British Columbia, Canada)
Holger Hermanns (Saarland University, Germany)
Pao-Ann Hsiung (National Chung Cheng University, Taiwan)
Alan Hu (University of British Columbia, Canada)
Michael Huth (Imperial College London, UK)
Jie-Hong Roland Jiang (National Taiwan University, Taiwan)
Orna Kupferman (Hebrew University, Israel)
Kim Guldstrand Larsen (Aalborg University, Denmark)
Xuandong Li (Nanjing University, China)
Annabelle McIver (Macquarie University, AU)
Ken McMillan (Microsoft, USA)
Madhavan Mukund (Chennai Mathematical Institute, India)
Flemming Nielson (Technical University of Denmark, Denmark)
Mizuhito Ogawa (Japan Advanced Institute of Science and Technology)
Catuscia Palamidessi (INRIA Saclay and LIX, FR)
Doron Peled (Bar Ilan University, Israel)
Geguang Pu (East China Normal University, China)
Jean-François Raskin (Université Libre de Bruxelles, Belgium)
Kristin Y. Rozier (NASA's Ames Research Center, USA)
Sven Schewe (Liverpool University, UK)
Scott Smolka (Stony Brook University, USA)
Farn Wang (National Taiwan University, Taiwan)
Bow-Yaw Wang (Academia Sinica, Taiwan)
Wang Yi (Uppsala University, Sweden)
Naijun Zhan (Institute of Software, Chinese Academy of Sciences)
Lijun Zhang (Institute of Software, Chinese Academy of Sciences)

STEERING COMMITTEE
E. Allen Emerson (University of Texas-Austin, USA)
Teruo Higashino (Osaka University, Japan)
Insup Lee (University of Pennsylvania, USA)
Doron Peled (Bar Ilan University, Israel)
Farn Wang (National Taiwan University, Taiwan)
Hsu-Chun Yen (National Taiwan University, Taiwan)


WORKSHOP CHAIR
Jun Sun (Singapore University of Technology and Design, SG)


KEYNOTES
Dino Distefano (Queen Mary, University of London, UK)
Joost-Pieter Katoen (RWTH Aachen University, Germany)
J Strother Moore (University of Texas-Austin, USA)


ATVA 2015  invites  submissions  for  workshop  proposals on
topics of interest to the ATVA series. The workshops will be
either half day or one full day. Depending on  the  number of
accepted workshops, the workshops will be scheduled either on
October 11, or  October 16, 2015.

All proposals should be sent by e-mail to the workshop
chair, Jun Sun, Singapore University of Technology and Design, SG,
e-mail: sunjun@sutd.edu.sg

DEADLINES FOR WORKSHOP PROPOSALS:

May 5, 2015: Submission of workshop proposals
May 30, 2015:   Notification of acceptance

35th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems

CALL FOR PAPERS

                        FORTE 2015
                A DisCoTec Member Conference

35th IFIP International Conference on Formal Techniques for
Distributed Objects, Components and Systems

http://discotec2015.inria.fr/
http://discotec2015.inria.fr/forte-2015-call-for-papers/

taking place on June 2-4, 2015 in Grenoble, France


Abstract Submission: February 15, 2015 (compulsory)
Paper Submission:    February 22, 2015
Author Notification: March 23, 2015
Camera Ready copy:   April 2, 2015
=============================================================

FORTE 2015 is a forum for fundamental research on theory, models, tools, and 
applications for distributed systems. The conference solicits original 
contributions that advance the science and technologies for distributed systems, 
with special interest in the areas of:

  * service-oriented, ubiquitous, pervasive, grid, cloud, and mobile computing
    systems;
  * object technology, modularity, component- and model-based design;
  * software reliability, availability, and safety;
  * security, privacy, and trust in distributed systems;
  * adaptive distributed systems, self-stabilization;
  * self-healing/organizing;
  * verification, validation, formal analysis, and testing of the above.

Contributions that combine theory and practice and that exploit formal methods 
and theoretical foundations to present novel solutions to problems arising from 
the development of distributed systems are encouraged. FORTE covers distributed 
computing models and formal specification, testing and verification methods. The 
application domains include all kinds of application-level distributed systems, 
telecommunication services, Internet, embedded and real-time systems, as well as 
networking and communication security and reliability.

=== Main topics of interest ===

Topics of interest include but are not limited to:

  * Languages and semantic foundations: new modeling and language concepts for
    distribution and concurrency, semantics for different types of languages,
    including programming languages, modeling languages, and domain-specific
    languages; real-time and probability aspects;
  * Formal methods and techniques: design, specification, analysis,
    verification, validation, testing and runtime verification of various types
    of distributed systems including communications and network protocols,
    service-oriented systems, adaptive distributed systems, cyber-physical
    systems and sensor networks;
  * Foundations of security: new principles for qualitative and quantitative
    security analysis of distributed systems, including formal models based on
    probabilistic concepts;
  * Applications of formal methods: applying formal methods and techniques for
    studying quality, reliability, availability, and safety of distributed
    systems;
  * Practical experience with formal methods: industrial applications, case
    studies and software tools for applying formal methods and description
    techniques to the development and analysis of real distributed systems.

=== Invited Speakers (DisCoTec) ===

  * Alois Ferscha (Johannes Kepler Universität, Linz, Austria)

  * Leslie Lamport (Microsoft Research, USA)

  * Willy Zwaenepoel (EPFL, Switzerland)


=== Submission and publication ===

Contributions must be written in English and report on original, unpublished 
work, not submitted for publication elsewhere (cf. IFIP’s codes of conduct). The 
submissions must be prepared using Springer’s LNCS style. Papers can be 
submitted electronically in pdf via the FORTE’15 interface of the EasyChair system.

We solicit four kinds of submissions:

  *  Full papers (up to 15 pages): Describing thorough and complete research
     results, tools or experience reports (if relevant, additional appendixes
     with proofs or other material meant for easing the reviewers' live are
     allowed)

  *  Short papers (up to 7 pages): Describing research results that are not
     fully developed, or manifestos, calls to action, personal views on FORTE
     related research, on the current state of the art, or on prospects for the
     years to come.

  *  Tool demonstration papers (up to 7 pages): focus on the usage aspects of
     tools. Theoretical foundations and experimental evaluation are not
     required, however, a motivation as to why the tool is interesting and
     significant should be provided. Papers may have an appendix of up to 5
     additional pages with details on the actual demonstration.

  *  Posters (up to 3 pages): Summarizing research projects worth being
     advertised and discussed in at the conference.

Each paper will undergo a peer review of at least 3 anonymous reviewers. The 
conference proceedings will be published by Springer in the LNCS Series. The 
best papers will be invited after the conference to contribute to a special 
issue of a top-level journal (TCS or FMSD).


=== Programme Chairs ===

    Susanne Graf (VERIMAG & CNRS, Grenoble, France)
    Mahesh Viswanathan (U. Illinois, USA)

=== Programme Committee ===

    Erika Abraham (RWTH Aachen, Germany)
    Luca Aceto (U. Reykjavik, Iceland)
    S Akshay (IIT Bombay, India)
    Paul Attie (American U. Beirut, Lebanon)
    Rohit Chadha (U. Missouri, USA)
    Rance Cleaveland (U. Maryland, USA)
    Frank de Boer (CWI, Amsterdam, Netherlands)
    Borzoo Bonakdarpour (Mc Master U., Ontario, Canada)
    Michele Boreale (U. Firenze, Italy)
    Stephanie Delaune (CNRS & ENS Cachan, France)
    Wan Fokkink (VU Amsterdam, Netherlands)
    Gregor Goessler (INRIA Grenoble, France)
    Gerard Holzmann (Jet Propulsion Laboratory, Pasadena, CA, USA)
    Alan Jeffrey (Alcatel-Lucent Bell Labs, USA)
    Petr Kuznetsov (Telecom ParisTech, France)
    Ivan Lanese (U. Bologna, Italy)
    Kim Larsen (U. Aalborg, Denmark)
    Antonia Lopes (U. Lisbon, Portugal)
    Stephan Merz (LORIA & INRIA Nancy, France)
    Catuscia Palamidessi (INRIA Saclay, France)
    Alan Schmitt (IRISA & INRIA Rennes, France)

=== Steering Committee: ===

    Erica Abraham (RWTH Aachen, Germany)
    Dirk Beyer (U. Passau, Germany)
    Michele Boreale (U. Firenze, Italy)
    Einar Broch Johnsen (U. Oslo, Norway)
    Frank de Boer (CWI, Amsterdam, Netherlands)
    Holger Giese (U. Potsdam, Germany)
    Catuscia Palamidessi (INRIA, Saclay, France)
    Grigore Rosu (U. Illinois, USA)
    Jean-Bernard Stefani (INRIA, Grenoble, France) (Chair)
    Heike Wehrheim (U. Paderborn, Germany)

Forum on specification & Design Languages

Forum on specification & Design Languages


 

CALL FOR PAPERS

September 14-16, 2015 | Barcelona, Spain




FDL is an international forum to exchange experiences and promote new trends
in the application of languages, their associated design methods and tools
for the design of electronic systems. FDL stimulates scientific and
controversial discussions within and in-between scientific topics as
described below. The program structure includes research working sessions,
embedded tutorials, panels, and technical discussions. The Forum includes
tutorials and fringe meetings, such as user group or standardization
meetings. "Wild and Crazy Ideas" are also welcome. 

Authors are invited to submit manuscripts on topics including, but not
limited to:

 

Formalisms & Languages

Requirements and Property specification (RSLs, PSLs, SVA, .),
Extra-functional specification (timing, power, temperature, aging, .),
Multi-domain parallel applications in dynamic real-time environments, Models
of computation, Automata (xFSM, .), Networks (Process Networks, Petri Nets,
Task Networks), Platform modelling and abstraction, Transaction level
modelling, Run-time system and middleware abstraction, Model and
component-based design (UML, SysML, MARTE, .), Advanced language extensions
for SLDLs (SystemC(-AMS), Modelica, VHDL-AMS, SystemVerilog Verilog-AMS,.)

 

Tools & Techniques

Formal property checking, Modeling and Simulation of functional and
extra-functional properties, Parallel simulation, High-level hardware and
software synthesis, Testbench automation and Coverage monitoring, Design
space exploration and virtual prototyping, Scheduling & real-time analysis

 

Design Flows & Methodologies

Horizontal and vertical virtual integration testing, Requirements
engineering and traceability, Mixed critical embedded applications on
multi-core multi-CPU SoCs, Power and performance, Safety and security,
Heterogeneous (mixed-signal/multiphysical) component integration,
Multi-objective optimization; Model-Driven Engineering


Important Deadlines:

Trending Topics

Besides the established topic areas listed above, we are also looking for
contributions in domains which have explicitly been advocated by the FDL
community for this year, namely:

Methodology: Formal Models / Formal Verification, System Engineering
(Specification, Requirements), Analog Mixed Signal and Multiphysical
Embedded Systems, Parallel Processing, Power and Performance Modelling,
Universal Verification Methodology, Device models for new technologies

Applications: Internet of Things (including M2M communication), Mixed
Criticality Embedded Systems, Verification of Autonomous Driving, Automatic
Driving and Driver Assistance


Proposals for Special Session:

Full Research Paper submission:

Other Contributions submission:

Notification of acceptance:

Camera ready papers:

March 22, 2015

May 4, 2015

June 10, 2015

July 4, 2015

August 12, 2015




 <http://www.ieee.org/index.html> 

 <http://ieee-ceda.org/> 


Call for Special Sessions

Professionals are invited to submit proposals for Special Sessions. Special
Session should focus on a Topic which is of particular interest to the FDL
audience. Papers of Special Sessions may be included in the proceedings/IEEE
Xplore. If you are interested in organizing a Special Session, please submit
a brief proposal (no more than two pages) which describes the topic, the
intended audience, as well as a list of possible speakers to
<mailto:fdl2015@ecsi.org> fdl2015@ecsi.org. The deadline for Special Session
proposals is March 22, 2015.

Submissions:

Authors should submit papers in double column, IEEE format as PDF through
the submission system:  <https://easychair.org/conferences/?conf=fdl2015>
https://easychair.org/conferences/?conf=fdl2015. Full Research Papers shall
not exceed 6-8 pages. Other Contributions like work in progress, wild &
crazy ideas, demo night abstracts, or user experiences shall not exceed 2-4
pages. Submitted papers should be anonymous, are required to describe
original unpublished work, and must not be under consideration for
publication elsewhere.

Publications:

The conference proceedings will be published in electronic form with an ISSN
and ISBN number and made available on the ECSI website and submitted for
inclusion in IEEE Xplore. In addition, an edited collection of extended
versions of selected best papers will be published as a book by Springer.


 


Contacts:

 <mailto:fdl@ecsi.org> fdl@ecsi.org |  <http://www.ecsi.org/fdl>
www.ecsi.org/fdl

General Chair: Julio Medina | Universidad de Cantabria, ES

Program Co-Chairs: Rolf Drechsler, Robert Wille | University of Bremen/DFKI,
DE

Local Co-Chair: Francisco J. Cazorla, Carles Hernandez | 

Barcelona Supercomputing Center, ES

The 9th International Symposium on Theoretical Aspects of Software Engineering , (TASE 2015)

TASE 2015 - CALL FOR PAPERS

******************************************************************
                The 9th International Symposium on
           Theoretical Aspects of Software Engineering
                           (TASE 2015)
                12-14 September 2015, Nanjing, China
                  http://tase2015.nuaa.edu.cn

        For more information email: tase2015@easychair.org
******************************************************************

--------
OVERVIEW
--------
The 9th Theoretical Aspects of Software Engineering Conference (TASE
2015) will be held in Nanjing, China in September, 2015.

Modern society is increasingly dependent on software systems that are
becoming larger and more complex. This poses new challenges to the
various aspects of software engineering, for instance, software
dependability in trusted computing, interaction with physical
components in cyber physical systems, distribution in cloud computing
applications, etc. Hence, new concepts and methodologies are required
to enhance the development of software engineering from theoretical
aspects. TASE 2015 aims to provide a forum for people from academia
and industry to communicate their latest results on theoretical
advances in software engineering.

TASE 2015 is the 9th in the TASE series. The past TASE symposiums were
successfully held in Shanghai ('07), Nanjing ('08), Tianjin ('09),
Taipei ('10), Xi'an ('11), Beijing ('12), Birmingham ('13),
Changsha('14).The proceedings of the TASE 2015 symposium are planned
to be published by the IEEE Computer Society Press. 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 Frontiers
of Computer Science journal.

------
TOPICS
------
The symposium is devoted to theoretical aspects of software
engineering. Topics of interest include, but are not limited to:

* Requirements Engineering
* Specification and Verification
* Program Analysis
* Software Testing
* Model-Driven Engineering
* Software Architectures and Design
* Aspect and Object Orientation
* Embedded and Real-Time Systems
* Software Processes and Workflows
* Component-Based Software Engineering
* Software Safety, Security and Reliability
* Reverse Engineering and Software Maintenance
* Service-Oriented and Cloud Computing
* Semantic Web and Web Services
* Type System and Theory
* Program Logics and Calculus
* Probability in Software Engineering

----------------
INVITED SPEAKERS
----------------
Marsha Chechik (University of Toronto, Canada)
Patrick Cousot (Ecole Normale Superieure, Paris, France)
Jin Song Dong  (National University of Singapore)


----------
SUBMISSION
----------
Submission should be done through the TASE 2015 submission page,
handled by the EasyChair conference system:

https://www.easychair.org/conferences/?conf=tase2015

As in previous years, the proceedings of the conference are planned to
be published by the IEEE Computer Society Press. Papers must be
written in English and not exceed 8 pages in Two-Column IEEE format.

---------------
IMPORTANT DATES
---------------
Abstract submission:  7  March 2015 (23h59 GMT)
Paper submission:    14  March 2015 (23h59 GMT)
Notification:        23  May   2015
Camera-ready:        13  June  2015
Conference:          12-14  September 2015

-------------
GENERAL CHAIR
-------------
Jifeng He          (East China Normal University, China)

-----------------
PROGRAM CO-CHAIRS
-----------------
Zhiqiu Huang       (Nanjing University of Aeronautics and Astronautics, China)
Jun Sun            (Singapore University of Technology and Design)

-----------------
STEERING COMMITTE
-----------------
Keijiro Araki      (Kyushu University, Japan)
Jifeng He          (East China Normal University, China)
Michael Hinchey    (Lero, Ireland)
Shengchao Qin      (Teesside University, UK)
Huibiao Zhu        (East China Normal University, China)

------------------
PROGRAM COMMITTIEE
------------------
Luciano Baresi     (Politecnico di Milano, Italy)
Earl Barr          (University College London, UK)
Nikolaj Bjorner    (Microsoft Research, USA)
Lubos Brim         (Masaryk University, Czech Republic)
Zining Cao         (Nanjing University of Aeronautics and Astronautics, China)
Taolue Chen        (Middlesex University, UK)
Zhenhua Duan       (Xidian University, China)
Wei Dong           (National University of Defense Technology, China)
Joaquim Gabarro    (Universitat Politecnica de Catalunya, Spain)
Jaco Geldenhuys    (University of Stellenbosch, South Africa)
Peter Habermehl    (Liafa, Paris 7, France)
Ian J. Hayes       (University of Queensland, Australia)
Dang Van Hung      (Vietnam National University, Vietnam)
Jason Lee          (University of Melbourne, Australia)
Karl Leung         (VTC, Hong Kong)
Bixin Li           (Southeast University, China)
Xiaoshan Li        (University of Macau, Macau)
Xuandong Li        (Nanjing University, China)
Zhoujun Li         (Beihang University, China)
Shaoying Liu       (Hosei University, Japan)
Martin Leucker     (University of L®πbeck, Germany)
Xiaoqing(Frank) Liu(Missouri University of Science and Technology, USA)
Antoine Min®¶       (Ecole Normale Sup®¶rieure Paris, France)
Fernando Orejas    (Universitat Politecnica de Catalunya, Spain)
Paritosh K. Pandya (Tata Institute of Fundamental Research, India)
Jun Pang           (University of Luxembourg)
Xin Peng           (Fudan University, China)
Geguang Pu         (East China Normal University, China)
Shengchao Qin      (Teesside University, UK)
Zongyan Qiu        (Peking University, China)
Cesar Sanchez      (IMDEA Software Institute, Spain)
Klaus Schneider    (University of Kaiserslautern, Germany)
Axel Simon         (Technical University of Munich, Germany)
Graeme Smith       (University of Queensland, Australia)
Colin Snook        (University of Southampton, UK)
Volker Stolz       (Bergen University College, Norway)
Kaile Su           (Griffith University, Australia)
Jing Sun           (University of Auckland, New Zealand)
Jean Pierre Talpin (INRIA, France)
Yih-Kuen Tsay      (National Taiwan University, Taiwan)
Viktor Vafeiadis   (MPI-SWS, Germany)
Margus Veanes      (Microsoft Research, USA)
Tomas Vojnar       (Brno University of Technology, Czech Republic)
Yi Wang            (Uppsala University, Sweden)
Hongji Yang        (Bath Spa University, UK)
Hongli Yang        (Beijing University of Technology, China)
Hongwei Xi         (Boston University, USA)
Yingfei Xiong      (Peking University, China)
Naijun Zhan        (Chinese Academy of Sciences, China)
Hao Zhong          (Shanghai Jiaotong University, China)
Huibiao Zhu        (East China Normal University, China)

----------------
ORGANIZING CHAIR
----------------
Ou Wei             (Nanjing University of Aeronautics and Astronautics, China)

----------------
PUBLICITY CHAIRS
----------------
Jun Hun            (Nanjing University of Aeronautics and Astronautics, China)
Jun Pang           (University of Luxembourg)
Yu Zhou            (Nanjing University of Aeronautics and Astronautics, China)

25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015

 25th International Symposium on
       Logic-Based Program Synthesis and Transformation
                         LOPSTR 2015

         Special Issue of Formal Aspects of Computing

            http://alpha.diism.unisi.it/lopstr15/

        University of Siena, Siena, IT, July 13-15, 2015
                (co-located with PPDP 2015)


DEADLINES
Abstract submission: April 6,  2015
Paper/Extended abstract submission: April 13, 2015

============================================================


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 25th International Symposium on Logic-based Program Synthesis  and
Transformation (LOPSTR 2015) will be held at the University of  Siena,
Siena,  Italy;   previous symposia were held in  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 2015 will be co-located with PPDP 2015 (International Symposium
on Principles and Practice of Declarative Programming).

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:                            April 6, 2015
 Paper/Extended abstract submission:             April 13, 2015
 Notification:                                   May 25, 2015
 Camera-ready (for electronic pre-proceedings):  June 15, 2015
 Symposium:                                      July 13-15, 2015


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
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 2015, which can be accessed through the website of LOPSTR 2015.


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.


Special journal issue

After the symposium, a selection of the best papers will be invited to
a  special  issue of  the  'Formal Aspects of Computing'  journal. The
submissions to the special issue must be substantial extensions of the
proceedings versions and will  undergo the usual journal reviewing
process.


Invited speakers

Patrick Cousot, New York University, USA (Jointly with PPDP)
Gilles Barthe, IMDEA Software Institute, Spain
Dale Miller, INRIA and LIX/Ecole Polytechnique, France


Program Committee

  Slim Abdennadher,  German University of Cairo, Egypt
  Maria Alpuente,  Universitat Politecnica de Valencia, Spain
  Demis Ballis,  University of Udine, Italy
  Olaf Chitil,  University of Kent, UK
  Michael Codish,  Ben-Gurion University, Israel
  Moreno Falaschi,  University of Siena, Italy (Program Chair)
  Jerome Feret,  INRIA and ENS, France
  Maurizio Gabbrielli,  University of Bologna, Italy
  Jurgen Giesl,  RWTH Aachen University, Germany
  Miguel Gomez-Zamalloa,  Complutense University of Madrid, Spain
  Arnaud Gotlieb,  SIMULA Research Laboratory, Norway
  Gopal Gupta,  University of Texas at Dallas, USA
  Manuel Hermenegildo,  IMDEA, Spain
  Viktor Kuncak,  EPFL Lausanne, Switzerland
  Luigi Liquori,  INRIA Sophia-Antipolis Mediterranee, France
  Alexei Lisitsa,  University of Liverpool, UK
  Narciso Marti-Oliet,  Universidad Complutense de Madrid, Spain
  Jorge Navas,  NASA, USA
  Kazuhiro Ogata,  JAIST, Japan
  Carlos Olarte, ECT, Univ. Federal do Rio Grande do Norte, Brasil
  Catuscia Palamidessi,  INRIA and Ecole Polytechnique, France
  Maurizio Proietti,  IASI-CNR, Italy
  Albert Rubio, Universitat Politecnica de Catalunya, Barcelona, Spain
  Wim Vanhoof,  University of Namur, Belgium


Program and Symposium Chair:

Moreno Falaschi, Dept. of Information Engineering and Mathematics,
Univ. of Siena, Italy
(moreno.falaschi@unisi.it)


Organizing Committee

Monica Bianchini, DIISM, Univ. of Siena, Italy
Sara Brunetti, DIISM, Univ. of Siena, Italy
Andrea Machetti, DIISM, Univ. of Siena, Italy
Simonetta Palmas, DIISM, Univ. of Siena, Italy
Maurizio Proietti,  IASI-CNR, Italy
Simone Rinaldi, DIISM, Univ. of Siena, Italy
Elisa Tiezzi, DIISM, Univ. of Siena, Italy
Sara Ugolini, Dip. Informatica, Univ. of Pisa

The 7th NASA Formal Methods Symposium

NFM 2015 CALL FOR PARTICIPATION The 7th NASA Formal Methods Symposium http://www.NASAFormalMethods.org/nfm2015 27 – 29 April 2015 Pasadena, California, USA THEME The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification. The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. The focus of the symposium is on formal methods, and aims to foster collaboration between NASA researchers and engineers and the wider aerospace and academic formal methods communities. TOPICS Topics of interest include, but are not limited to: Model checking Theorem proving SAT and SMT solving Symbolic execution Static analysis Runtime verification Systematic testing Program refinement Compositional verification Modeling and specification formalisms Model-based development Model-based testing Requirement engineering Formal approaches to fault tolerance Security and intrusion detection Applications of formal methods INVITED SPEAKERS Dino Distefano Software Engineer at Facebook, California, USA and Professor at Queen Mary University of London, UK. Viktor Kuncak Leads Lab for Automated Reasoning and Analysis at EPFL, Lausanne, Switzerland. Rob Manning Chief Engineer at NASA/JPL. LOCATION, COST, REGISTRATION AND HOTEL ROOM BOOKING The symposium will take place at the Hilton Hotel, Pasadena, California, USA, April 27-29, 2015. There will be no registration fee for participants. All interested individuals, including non-US citizens, are welcome to attend; however, all attendees must register (but please only register if you intend to attend). Registration form and hotel booking websites are reachable from the main website. A block of rooms at a low price are reserved with booking deadline of March 26. PC CHAIRS Klaus Havelund, NASA Jet Propulsion Laboratory, USA Gerard Holzmann, NASA Jet Propulsion Laboratory, USA Rajeev Joshi, NASA Jet Propulsion Laboratory, USA PUBLICITY SUPPORT Ylies Falcone, Université Joseph Fourier, France PROGRAMME COMMITTEE Erika Abraham, RWTH Aachen University, Germany Julia Badger, NASA Johnson Space Center, USA Christel Baier, Technische Universität Dresden, Germany Saddek Bensalem, VERIMAG/UJF, France Dirk Beyer, University of Passau, Germany Armin Biere, Johannes Kepler University, Austria Nikolaj Bjorner, Microsoft Research, USA Borzoo Bonakdarpour, McMaster University, Canada Alessandro Cimatti, Fondazione Bruno Kessler, Italy Leonardo de Moura, Microsoft Research, USA Ewen Denney, NASA Ames Research Center, USA Ben Di Vito, NASA Langley Research Center, USA Dawson Engler, Stanford University, USA Jean-Christophe Filliatre, Université Paris-Sud, France Dimitra Giannakopoulou, NASA Ames Research Center, USA Alwyn Goodloe, NASA Langley Research Center, USA Susanne Graf, VERIMAG, France Alex Groce, Oregon State University, USA Radu Grosu, Vienna University of Technology, Austria John Harrison, Intel Corporation, USA Mike Hinchey, University of Limerick/Lero, Ireland Bart Jacobs, University of Leuven, Belgium Sarfraz Khurshid, The University of Texas at Austin, USA Gerwin Klein, NICTA, Australia Daniel Kroening, Oxford University, UK Orna Kupferman, Hebrew University Jerusalem, Israel Kim Larsen, Aalborg University, Denmark Rustan Leino, Microsoft Research, USA Martin Leucker, University of Lubeck, Germany Rupak Majumdar, Max Planck Institute, Germany Pete Manolios, Northeastern University, USA Peter Mueller, ETH Zurich, Switzerland Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA Corina Pasareanu, NASA Ames Research Center, USA Doron Peled, Bar Ilan University, Israel Suzette Person, NASA Langley Research Center, USA Andreas Podelski, University of Freiburg, Germany Grigore Rosu, University of Illinois, USA Kristin Yvonne Rozier, NASA Ames Research Center, USA Natarajan Shankar, SRI International, USA Natasha Sharygina, University of Lugano, Switzerland Scott Smolka, Stony Brook University, USA Willem Visser, University of Stellenbosch, South Africa Mahesh Viswanathan, University of Illinois, USA Mike Whalen, University of Minnesota, USA Jim Woodcock, University of York, UK STEERING COMMITTEE Julia Badger, NASA Johnson Space Center Ewen Denney, NASA Ames Research Center Ben Di Vito, NASA Langley Research Center Klaus Havelund, NASA Jet Propulsion Laboratory Gerard Holzmann, NASA Jet Propulsion Laboratory Cesar Munoz, NASA Langley Research Center Corina Pasareanu, NASA Ames Research Center Suzette Person, NASA Langley Research Center Kristin Yvonne Rozier, NASA Ames Research Center

The 3rd IEEE International Workshop on Formal Methods Integration – FMi 2015

==================================================*

The 3rd IEEE International Workshop on Formal Methods Integration – FMi
2015

In conjunction with the 16th IEEE IRI 2015

http://www.ieee-iri.org

San Francisco, USA, August 13-15, 2015

*==================================================*



*Important dates          *

Abstract Submission deadline: April 7, 2015
Paper submission deadline: April 15, 2015
Paper notification: May 20, 2015
Camera-ready paper due: May 30, 2015

Registration due: May 30, 2015


*Scope and topics*

Formal methods seek to contribute to the engineering of dependable systems
by applying sound techniques based on computer science fundamentals.
Complex systems often involve different formalisms to deal with the
modeling of their different aspects, as each formalism is specific to only
some system aspects and none is perfectly supporting all aspect constructs
and their related semantics. Accordingly, different analysis techniques are
required to check the different system views and verify different kinds of
properties. Formalism integration is intended to support coherent
specification and analysis of different aspects of a system. The FMi workshop
aims at further research into hybrid approaches to formal modeling and
analysis. It seeks contributions from researchers and practitioners
interested in all aspects of integrating methods, either formal or
semi-formal, for system development, covering all engineering development
phases from user requirements through design and analysis techniques to
tools. The workshop also encourages new initiatives of building bridges
between informal, semi-formal, and formal notations. Authors are invited to
submit both research and tool papers.



Topics of interest include, but are not limited to:

-          scalable formal methods,

-          component-based specification and analysis,

-          integrated software/hardware specification and analysis,

-          hybrid and embedded systems modeling and analysis,

-          object and multi-agent systems modeling and analysis,

-          requirement specification and analysis,

-          software and hardware specification, verification, and
validation,

-          theorem proving and decision procedures,

-          formal aspects of software evolution and maintenance,

-          formal methods for re-engineering and reuse,

-          formal languages integration,

-          semi-formal (UML, SysML, …) and formal model integration,

-          informal and formal language integration,

-          integration of formal methods into software engineering practice,

-          integrated analysis techniques,

-          tools integration,

-          integration of formal methods in education,

-          integration of formal methods in health,

-          integration of formal methods in industry,

-          integration of formal methods in security.



*Paper submission      *

Submitted papers must be unpublished and not considered elsewhere for
publication. Submissions will undergo a rigorous review process handled by
the Technical Program Committee. Papers will be selected based on their
originality, significance, relevance, and clarity of presentation. Only
electronic submissions in PDF format through the EasyChair submission
site: *https://easychair.org/conferences/?conf=fmi2015
<https://easychair.org/conferences/?conf=fmi2015>* will be considered.
Papers must be in English, up to 8 pages in IEEE format, including
references and appendices. The IEEE LaTeX and Microsoft Word templates, as
well as formatting guidelines, can be found on the paper submission
instructions available at the main conference website.



*Paper publication        *

At least one of the authors must register and present the paper, if
accepted. Registered papers will be published as workshop papers in the
IEEE IRI conference proceedings published by IEEE Computer Society
Press. Presented
papers will be invited to be extended and considered for publication in a
special issue of Advances in Intelligent Systems and Computing, edited by
Springer.



*Workshop Chair*

Thouraya Bouabana Tebibel, LCSI Laboratory, Ecole Nationale Supérieure
d’Informatique – ESI, Alger, Algeria



*Program Committee*

Alessandro Abate, University of Oxford, UK

Erika Ábrahám, RWTH Aachen University, Germany

Wolfgang Ahrendt, Chalmers University of Technology, Sweden

Yamine Ait Ameur, University of Toulouse, France

Keijiro Araki, Kyushu University, Japan

Cyrille Artho,     AIST, Japan

Kyungmin Bae, Carnegie Mellon University, USA

Luis Barbosa, Universidade do Minho, Portugal

Kamel Barkaoui, CNAM, France

Marcello Bonsangue, Leiden University, The Netherlands

Phillip J Brooke, Teesside University, UK

Andrew Butterfield, Trinity College Dublin, Ireland

Radu Calinescu, University of York, UK

Allaoua Chaoui, University of Constantine, Algeria

Krishnendu Chatterjee, Institute of Science and Technology, Austria

Hung Dang-Van, UET, Vietnam National University, Vietnam

John Derrick, University of Sheffield, UK

Bernd Finkbeiner, Saarland University, Germany

Alex Groce, Oregon State University, USA

Reiner Hähnle, Technical University of Darmstadt, Germany

René Rydhof Hansen, Aalborg University, Denmark

Klaus Havelund, JPL, California Institute of Technology, USA

Rolf Hennicker, Ludwig-Maximilians University, Germany

Nadjet Kamel, University of Sétif, Algeria

Ferhat Khendek, Concordia University, Canada

Peter Gorm Larsen, Aarhus University, Denmark

Michele Loreti, University of Florence, Italy

José Merseguer, University of Zaragoza, Spain

Bruno Monsuez, Ensta, France

Wojciech Mostowski, University of Twente, The Netherlands

Alexandre Mota, Centre of Informatics, Brazil

John Mullins, École polytechnique de Montréal, Canada

Brina Nielsen, Aalborg University, Denmark

Gordon J. Pace, University of Malta, Malta

Luigia Petre, Åbo Akademi University, Finland

Alexandre Petrenko, Centre de Recherche Informatique de Montréal, Canada

Erik Poll, Radboud University Nijmegen, The Netherlands

Matteo Rossi, Politecnico di Milano, Italy

Kristin Yvonne Rozier, NASA Ames Research Center, USA

Stuart H. Rubin, SSC-Pacific, USA

Philipp Ruemmer, Uppsala University, Sweden

Djamel Eddine Saidouni, University of Constantine, Algeria

Augusto Sampaio, Federal University of Pernambuco, Brazil

Steve Schneider, University of Surrey, UK

Christophe Sibertin Blanc, University of Toulouse 1, France

Jiri Srba, Aalborg University, Denmark

Shuling Wang, Chinese Academy of Sciences, China

Gianluigi Zavattaro, University of Bologna, Italy



*Contact*

Thouraya Bouabana Tebibel at t_tebibel@esi.dz

The 2nd Formal Integrated Development Environment Workshop (F-IDE 2015)

​******************************************************************
                F-IDE 2015 - CALL FOR PAPERS
******************************************************************

       The 2nd Formal Integrated Development Environment Workshop
                           (F-IDE 2015)
                   22 June 2015, Oslo, Norway
            http://www.eecs.qmul.ac.uk/~masci/fide2015

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

--------
OVERVIEW
--------
The 2nd Formal Integrated Development Environment Workshop (F-IDE 2015) will be held
in Oslo, Norway, in June, 2015.

High levels of safety, security and also privacy standards require the use of formal
methods to specify and develop compliant software (sub)systems. Any standard comes
with an assessment process, which requires a complete documentation of the
application in order to ease the justification of design choices and the review of
code and proofs.

Ideally, an F-IDE dedicated to such developments should comply with several
requirements. The first one is to associate a logical theory with a programming
language, in a way that facilitates the tightly coupled handling of specification
properties and program constructs. The second one is to offer a language/environment
simple enough to be usable by most developers, even if they are not fully acquainted
with higher-order logics or set theory, in particular by making development of
proofs as easy as possible. The third one is to offer automated management of
application documentation. It may also be expected that developments done with such
an F-IDE are reusable and modular. Moreover, tools for testing and static analysis
may be embedded in this F-IDE, to help address most steps of the assessment
process.

------
TOPICS
------
The workshop is opened to contributions on all aspects of a system development
process, including specification, design, implementation, analysis and
documentation. It should allow the presentation of tools, methods, techniques and
experiments. Topics of interest include, but are not limited to, the following:

– F-IDE building: design and integration of languages, compilation
– How to make high-level logical and programming concepts palatable to industrial
developers
– Integration of Object-Oriented and modularity features
– Integration of static analyzers
– Integration of automatic proof tools, theorem provers and testing tools
– Documentation tools
– Impact of tools on certification
– Experience reports of developing F-IDE
– Experience reports of using F-IDE
– Experience reports of formal methods-based assessments of industrial applications

----------
SUBMISSION
----------
Papers must be written in English, not exceed 15 pages in LNCS format, not counting
references, and follow the FM 2015 Format and Submission Guidelines.

They can be:
- Research papers providing new concepts and results
- Position papers and research perspectives
- Experience reports
- Tool presentations

Papers can be submitted through Easychair:
https://easychair.org/conferences/?conf=fide2015


-----------
PROCEEDINGS
-----------
- Preliminary proceedings, including all the papers selected for the workshop, will
be available electronically at the workshop.
- Post proceedings are under consideration as Electronic Proceedings in Theoretical
Computer Science (ETPCS) proceedings.

---------------
IMPORTANT DATES
---------------
Abstract submission:  March 24, 2015 (23h59 GMT)
Paper submission:     March 31, 2015 (23h59 GMT)
Notification:         April 30, 2015
Camera-ready:         May 15, 2015
Workshop:             June 22, 2015

-----------------
PC CO-CHAIRS
-----------------
Catherine Dubois     ENSIIE, Cedric, catherine (dot) dubois (at) ensiie (dot) fr
Paolo Masci          Queen Mary University of London, paolo (dot) masci (at) eecs
(dot) qmul (dot) ac (dot) uk
Dominique Mery       Université de Lorraine, dominique (dot) mery (at) loria (dot) fr

-----------------
PC MEMBERS (to be completed)
-----------------
Bernhard Beckert     Karlsruhe Institute of Technology
Jose     Campos      Universidade do Minho
Paul     Curzon      Queen Mary University of London
Carlo Alberto Furia  ETH Zurich
Therese  Hardin      UPMC
Rustan   Leino       Microsoft Research
Michael  Leuschel    University of Dusseldorf
Claude   Marche      INRIA
Stefan   Mitsch      Carnegie Mellon University
Patrick  Oladimeji   Swansea University
Suzette  Person      NASA Langley Research Center
Francois Pessaux     ENSTA ParisTech
Marie-Laure Potet    Laboratoire Verimag
Steve    Reeves      Waikato University
John     Rushby      SRI International
Rene     Thiemann    University of Innsbruck
Boris    Yakobowski  CEA LIST

5th International ABZ 2014 Conference (ASM, Alloy, B, TLA, VDM, Z)

Call for Papers, Answers to the case study, Workshops, Tutorials

5th International ABZ 2014 Conference (ASM, Alloy, B, TLA, VDM, Z)
==========================================

May 23-27, 2016 -- Linz, Austria
http://www.cdcc.faw.jku.at/ABZ2016/

The ABZ conference is dedicated to the cross-fertilization of six 
related state-based and machine-based formal methods, Abstract State 
Machines (ASM), Alloy, B, TLA, VDM and Z, that share a common conceptual 
foundation and are widely used in both academia and industry for the 
design and analysis of hardware and software systems. It builds on the 
success of the first ABZ conference held in London in 2008, where the 
ASM, B and Z conference series merged into a single event, the second 
ABZ 2010 conference held in Orford (Canada), where the Alloy community 
joined the event, the ABZ 2012 held in Pisa (Italy), which saw the 
inclusion of the VDM community, and ABZ 2014 held in Toulouse (France), 
which brought the inclusion of the TLA community into the ABZ conference 
series. The ABZ 2016 conference will be held in Linz, Austria.

Contributions are solicited on all aspects of the theory and 
applications of ASMs, Alloy, B, TLA, VDM, Z approaches in 
software/hardware engineering, including the development of tools and 
industrial applications. The program spans from theoretical and 
methodological foundations to practical applications, emphasizing system 
engineering methods and tools that are distinguished by mathematical 
rigor and have proved to be industrially viable. The main goal of the 
conference is to contribute to the integration of accurate state- and 
machine-based system development methods, clarifying their commonalities 
and differences to better understand how to combine different approaches 
for accomplishing the various tasks in modeling, experimental 
validation, mathematical verification of reliable high-quality 
hardware/software systems.

Although organized to host several formal methods with ASM, Alloy, B, 
TLA, VDM and Z, in a single event, editorial control of the joint 
conference is vested in one integrated program committee, which will 
respectively determine its ASM, Alloy, B, TLA, VDM and Z content, to be 
presented in parallel conference tracks with a schedule to allow the 
participants to switch between the sessions.

As successfully practiced at ABZ 2014, the 5th edition of ABZ will again 
include special sessions dedicated to a shared real-life case study 
among all the methods addressed in ABZ 2016. The objective of this 
session is to enrich the set of case studies developed with ABZ methods 
with a practical and real-life case study. After the success of the 
"Landing Gear" case study at ABZ 2014 in the aeronautical context this 
time the organizers defined a real-life case study issued from the 
medical domain with challenging safety requirements. The ABZ 2016 case 
study concerns the control of a hemodialysis machine. See 
http://www.cdcc.faw.jku.at/ABZ2016/ for a detailed description of this 
case study.

Proposals are invited for workshops and tutorials to take place before 
the main conference.

Four kinds of contributions are invited:

-- Research papers: full papers of not more than 14 pages in LNCS 
format, which have to be original, unpublished and not submitted elsewhere.

-- Short presentations of work in progress, and tool demonstrations. 
This is an excellent opportunity for Ph.D. students to present and 
validate their work in progress. An extended abstract of not more than 4 
pages is expected and will be reviewed.

-- Answers to case study papers: full papers of not more than 14 pages 
in LNCS format reporting on the experiments conducted with any of the 
state based techniques in the scope of ABZ 2014.

-- Application in industry papers reporting on work or experiences on 
the application of state based formal methods in industry. An extended 
abstract of not more than 4 pages is expected and will be reviewed. It 
is also an interesting option for industrial practitioners who sometimes 
face too many constraints to prepare a full paper.

Submissions:
========

Research, short and industry papers must be prepared using the SPRINGER 
LNCS style and submitted electronically in PDF at the ABZ 2016 
conference submission website (Easy Chair).

Programm Committee Chairs:
Michael BUTLER, University of Southampton, Southampton, UK
Klaus-Dieter SCHEWE, Johannes-Kepler-University Linz and Software 
Competence Center Hagenberg, Linz/Hagenberg, Austria

Program Committee: tba

Answers to the case study must be prepared using the SPRINGER LNCS style 
and submitted electronically in PDF at the ABZ 2016 conference 
submission website (Easy Chair).

Case study Chairs:
Atif Mashkoor, Software Competence Center Hagenberg, Hagenberg, Austria 
(atif.mashkoor@scch.at)
Miklos Biro, Software Competence Center Hagenberg, Hagenberg, Austria 
(miklos.biro@scch.at)

The submission system for the conference can be accessed at 
https://easychair.org/conferences/?conf=abz2016

The deadline for submissions is January 15, 2016. Notifications will be 
sent by February 22, 2016.

Publication:
=======

All research and short accepted papers will be published in a volume of 
Springer's LNCS series. The answers to case study papers and the 
application in industry papers shall be published in a volume of 
Springer's CCIS series (tbc). The two volumes will be distributed at the 
conference.

Journal Special Issues: It is planned that an improved version of a 
selected number of contributions will be published in a special issue of 
the journal Science of Computer Programming for the research papers and 
in a special issue of the Software Tools and Technology Transfer journal 
for the answers to case study papers (to be confirmed).

Workshops and Tutorials:
================

Workshops and tutorials will be associated to the main event ABZ. 
Proposals are solicited in areas related to the conference topics. 
Workshop proposal should be sent to the workshop chairs:

     Yamine Ait-Ameur, Institut National Polytechnique de Toulouse, 
France (yamine@enseeiht.fr)
     Stephan Merz, INRIA Nancy, Nancy, France (stephan.merz@loria.fr)
     Alexander Raschke, University of Ulm, Ulm, Germany 
(alexander.raschke@uni-ulm.de)

The deadline for submissions is October 16, 2015. Notifications will be 
sent by November 6, 2015.

Tutorial proposal should be sent to the tutorial chairs (tbc):

     Vincenzo Gervasi, University of Pisa, Pisa, Italy (gervasi@di.unipi.it)
     Michael Leuschel, University of Duesseldorf, Duesseldorf, Germany  
(leuschel@cs.uni-duesseldorf.de)

The deadline for submissions is February 15, 2016. Notifications will be 
sent by March 14, 2016.

Important Dates:
==========

Workshop proposal submission: October 16, 2015
Workshop proposal notification: November 6, 2015

Research paper submission:  January 15, 2016
Answers to case study submission:  January 15, 2016
Short and industry paper submission: February 4, 2016
Acceptance notification: February 22, 2016
Final Version due: March 14, 2016

Tutorial proposal submissions: February 15, 2016
Tutorial proposal notifications: March 14, 2016

ABZ 2016 conference: May 23-27, 2016


For questions concerning ABZ 2016, contact Klaus-Dieter SCHEWE 
(klaus-dieter.schewe@scch.at).