ForMASECC 2012 - Workshop on Formal Methods and Automated Software Engineering for Cloud Computing
Affiliated to the 12th International Conference on Algorithms and Architectures for Parallel Processing
Fukuoka, Japan, September 04-07, 2012
Objectives & Scope

With the development of mobile and internet applications, cloud computing becomes more and more important. More and more of our data are in the cloud. It is thus very important to have reliable, safe and secure cloud environments.

Verified programs could take several forms. One could use a methodology based on the specification of software and refinement down to an implementation, such as the B method. One could also use methods based on Hoare logic and associated tools. Another possibility is to take advantage of the fact that the logic of some interactive provers (such as Coq or Isabelle) contain a functional programming language. One writes the program to verify as a functional program, and proves that the function meets its specification.

Software composition in Cloud computing could be based on web services. The verification of the composition of such web services is thus of interest for Cloud computing.

The goal of the ForMASECC workshop is to provids a forum for discussion and research about formal verification and automated software engineering for all aspects of Cloud computing.

We welcome submission of original, unpublished papers in English on topics including (but not limited to) the following aspects:

- Programming models for Cloud computing:
* Formal semantics of these programming models
* Program logics for these programming models
* Type systems
* Application of formal tools
- Constructive methods for Cloud computing applications:
* Theory of constructive algorithmics for Cloud computing
* Tools for the derivation of Cloud computing applications
- Verification of the middleware:
* Formal models of the implementation of Map Reduce and related software
* Verification of Map Reduce implementations (and related software)
* Extended support for fault tolerance in Map Reduce
- Verification of hypervisors
- Formal aspects of software composition in Cloud computing:
* Specification of Web Services
* Composition of Web Services
* Exception handling

Submission

Regular Research Papers. Prospective authors are invited to submit full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. Papers will go through a rigorous reviewing process. Each paper will be reviewed by at least three referees. The papers are limited to 10 pages in the Springer LNCS format, including all figures, tables and references.

Work-in-Progress Papers. Prospective authors are invited to submit short abstracts in English presenting original research. Each paper will be reviewed by two referees. The papers are limited to 4 pages in the Springer LNCS format, including all figures, tables and references.

Website for Submission: https://www.easychair.org/conferences/?conf=formasecc2012
Publication

The author registration date and the final manuscript due date are strict. Accepted papers will be published in same proceedings (EI indexed) of the 12th International Conference on on Algorithms and Architectures for Parallel Processing ( ICA3PP 2012) published by Springer LNCS Series. At least one of the authors of each accepted paper must register as a full participant of the symposium to have the paper published in the proceedings.
Important Dates

Regular Research Paper Submission: May 7, 2012
Work-in-Progress Paper Submission: May 21, 2012
Notification of Acceptance: June 15, 2012
Camera-Ready Paper: June 28, 2012

Program Committee

Marco Aldinucci (University of Torino, Italy)
Frédéric Gava (University Paris East - Créteil, France)
Nikolai Kosmatov (CEA, France)
Kiminori Matsuzaki (Kochi University of Technology, Japan)
Frédéric Loulergue, Chair (University of Orleans, France)
Julien Tesson (Kochi University of Technology, Japan)
Emilio Tuosto (University of Leicester, UK)

Contact

formasecc2012@easychair.org