[Caml-list] HLPP2013 Paris July2013: Third Call for Papers

CALL FOR PAPERS

International Symposium on High-level Parallel Programming and Applications

https://sites.google.com/site/hlpp2013

HLPP2013,  Paris 1-2 July 2013

Aims and scope: 

As processor and system manufacturers increase the amount of both inter-

and intra-chip parallelism it becomes crucial to provide the software

industry with high-level, clean and efficient tools for parallel

programming. Parallel and distributed programming methodologies are

currently dominated by low-level techniques such as send/receive message

passing, or equivalently unstructured shared memory

mechanisms. Higher-level, structured approaches offer many possible

advantages and have a key role to play in the scalable exploitation of

ubiquitous parallelism. 

Since 2001 <http://www.hlpp.eu> the HLPP series of meetings has been a

forum for researchers developing state-of-the-art concepts, tools and

applications for high-level parallel programming. The general emphasis

is on software quality, programming productivity and high-level

performance models. The 2013 symposium will be a self-contained event,

held in central Paris. 

Invited speaker: Leslie Valiant (Harvard University) inventor of the

BSP paradigm and 2010 Turing award.

Topics:  HLPP 2013 invites the submission of papers written in English

on all topics including (but not limited to) the following aspects

of multi-core, parallel, distributed, grid and cloud computing: 

    High-­level programming and performance models (BSP, CGM, LogP,

    MPM, etc.) and tools 

    Declarative parallel programming methodologies 

    Algorithmic skeletons and constructive methods 

    Declarative parallel programming languages and libraries: semantics

    and implementation 

    Verification of declarative parallel and distributed programs 

    Software synthesis, automatic code generation for parallel programming 

    Model-driven software engineering with parallel programs 

    High-level methods for heterogeneous/hierarchical platforms: GPGPU,

    FPGA etc.  

    High-level parallel methods for large structured and

    semi-structured datasets 

    Applications of parallel systems using high­level languages and tools 

    Teaching experience with high­level tools and methods   

Proceedings:  

Authors of accepted papers will be expected to register and to present

their paper at the symposium. 

All accepted papers will be eligible for publication in a special issue

of Springer's International Journal of Parallel Programming

<http://www.springer.com/computer/theoretical+computer+science/journal/10766> (IJPP). 

International programme committee: 

    Mostafa Bamha (Université d'Orléans, France)

    Pavan Balaji (Argonne National Laboratory, United States)

    Rob Bisseling (Utrecht University, Netherlands) 

    Murray Cole (University of Edimburgh, United Kingdom) 

    Kento Emoto (University of Tokyo, Japan)

    Frédéric Gava (Université Paris-Est, France)

    Alexandros Gerbessiotis (New Jersey Institute of Technology, United

    States)

    Andy Gill (University of Kansas, United States)

    Clemens Grelck (University of Amsterdam, Netherlands)

    Christoph Kessler (Linköping University, Sweden) 

    Herbert Kuchen (Universität Münster, Germany)

    Ramon Lawrence (University of British Columbia, Canada)

    Quentin Miller (Somerville College Oxford, United Kingdom)

    Susanna Pelagatti (University of Pisa, Italy)

    Alexander Tiskin (University of Warwick, United Kingdom)

Organizers and program co-chairs:  

    Gaétan Hains (Université Paris-Est, France) 

    Youry Khmelevsky (University of British Columbia, Canada) 

HLPP steering committee: 

    Clemens Grelck (University of Amsterdam, Netherlands)

    Gaétan Hains (Université Paris-Est, France)

    Kiminori Matsuzaki (Kochi University of Technology, Japan) 

    Frédéric Loulergue (Université d'Orléans, France) 

    Quentin Miller (Somerville College Oxford, United Kingdom)

    Alexander Tiskin (University of Warwick, United Kingdom)

Paper submission:   

Submitted papers must not have been published or simultaneously

submitted elsewhere.  Submission should include a cover page with

authors' names, affiliation addresses, fax numbers, phone numbers, and

email addresses.  Please, indicate clearly the corresponding author and

include up to 6 keywords from the above list of topics and an abstract

of no more than 450 words.  Submissions should cover approximately 15

pages and camera-ready versions will be 20 pages long.  Full manuscripts

should be prepared with the IJSS latex macro package

<http://www.springer.com/cda/content/document/cda_downloaddocument/LaTeX.zip?SGWID=0-0-45-468198-0> and

submitted via the IJPP online editorial system

<http://www.editorialmanager.com/ijpp/>.  Only source latex files will

be acepted by the system. Each paper will receive a minimum of three

reviews.  Papers will be selected based on their originality, relevance,

technical clarity and presentation.  Authors of accepted papers must

guarantee that their papers will be registered and presented at the

symposium.  Accepted papers will be made available at the time of the

meeting and published in the symposium proceedings. 

 

Important dates: 

HLPP2013

 

  Paper submissions      Sun.  17 February 2013 

  Notification to authors Sun.  17 March 2013 

  HLPP symposium  Mon.-Tue. 1-2 July 2012 

Venue:   Institut Henri Poincaré <http://www.ihp.fr/>, Paris. 

Registration:   Registration fees will be kept to a minimum. Details

will be shown here as early as possible. 

 Past HLPP events:          http://www.hlpp.eu 

 URL for this page:         https://sites.google.com/site/hlpp2013/ 

 

Contacts: Gaetan.Hains@u-pec.fr, Youry.Khmelevsky@ubc.ca

[Caml-list] RTA 2013: LAST CALL FOR PAPERS

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

RTA 2013: LAST CALL FOR PAPERS

24th International Conference on Rewriting Techniques and Applications

June 24 - 26, 2013

Eindhoven, The Netherlands

co-located with TLCA 2013 as part of RDP 2013

http://rta2013.few.vu.nl/

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

abstract submission February 1 2013
paper submission February 5 2013 (THIS IS A STRICT DEADLINE !)
rebuttal period March 18-21 2013
notification April 4 2013
final version April 26 2013

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

The 24th International Conference on Rewriting Techniques and Applications
(RTA 2013) is organized as part of the Federated Conference on Rewriting,
Deduction, and Programming (RDP 2013), together with the 11th International
Conference on Typed Lambda Calculi and Applications (TLCA 2013), and several
workshops. RDP 2013 will be held at the Eindhoven University of Technology
in the Netherlands.

*** INVITED SPEAKERS ***

- Simon Peyton-Jones (Microsoft Research, UK)
joint invited speaker for TLCA+RTA 2013
- Jarkko Kari (University of Turku, Finland) invited speaker for RTA 2013
- Mitsu Okada (Keio University, Japan) invited speaker for RTA 2013

*** TOPICS OF INTEREST ***

RTA is the major forum for the presentation of research on all aspects of
rewriting. Typical areas of interest include (but are not limited to):

Applications: case studies; analysis of cryptographic protocols; rule-based
(functional and logic) programming; symbolic and algebraic computation;
SMT solving; theorem proving; system synthesis and verification; proof
checking; reasoning about programming languages and logics; program
transformation; XML queries and transformations; systems biology;
homotopy theory; implicit computational complexity;

Foundations: equational logic; universal algebra; rewriting logic;
rewriting models of programs; matching and unification; narrowing;
completion techniques; strategies; rewriting calculi; constraint solving;
tree automata; termination; complexity; modularity;

Frameworks: string, term, and graph rewriting; lambda-calculus and
higher-order rewriting; constrained rewriting/deduction; categorical and
infinitary rewriting; stochastic rewriting; net rewriting; binding
techniques; Petri nets; higher-dimensional rewriting;

Implementation: implementation techniques; parallel execution; rewrite and
completion tools; certification of rewriting properties; abstract
machines; explicit substitutions; automated (non)termination and
confluence provers; automated complexity analysis.

*** PUBLICATION ***

The proceedings will be published by LIPIcs (Leibniz International
Proceedings in Informatics). LIPIcs is open access, meaning that
publications will be available online and free of charge, and authors
keep the copyright for their papers. LIPIcs publications are indexed
in DBLP. For more information about LIPIcs please consult:
<http://www.dagstuhl.de/en/publications/lipics>

Also, authors of selected papers will be invited to submit
an extension of their RTA 2013 paper to a special issue of
Logical Methods in Computer Science (LMCS)
<http://www.lmcs-online.org/index.php>.

*** SUBMISSION GUIDELINES ***

Submissions must be
- original and not submitted for publication elsewhere,
- written in English,
- a research paper, or a problem set, or a system description,
- in pdf prepared with pdflatex using the LIPIcs stylefile:
<http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz>,
- at most 10 pages for system description,
at most 15 pages for the other two types of submissions
- submitted electronically through the EasyChair system at:
<https://www.easychair.org/conferences/?conf=rta2013>.

The page limit and the deadline for submission are strict.

Additional material for instance proof details, may be given in an appendix
which is not subject to the page limit. However, submissions must be
self-contained within the respective page limit; reading the appendix should
not be necessary to assess the merits of a submission.

*** PROGRAMME COMMITTEE CHAIR ***

Femke van Raamsdonk (VU University Amsterdam, The Netherlands)

*** PROGRAMME COMMITTEE ***

Eduardo Bonelli National University of Quilmes, Argentina
Byron Cook Microsoft Research Cambridge, UK
Stephanie Delaune ENS Cachan, France
Gilles Dowek Inria Paris-Rocquencourt, France
Maribel Fernandez King's College London, UK
Nao Hirokawa JAIST Ishikawa, Japan
Delia Kesner University Paris-Diderot, France
Helene Kirchner Inria Paris-Rocquencourt, France
Barbara Koenig University Duisburg Essen, Germany
Temur Kutsia Johannes Kepler University Linz, Austria
Aart Middeldorp University of Innsbruck, Austria
Vincent van Oostrom Utrecht University, The Netherlands
Femke van Raamsdonk VU University Amsterdam, The Netherlands
Kristoffer Rose IBM Research New York, USA
Manfred Schmidt-Schauss Goethe University Frankfurt, Germany
Peter Selinger Dalhousie University, Canada
Paula Severi University of Leicester, UK
Aaron Stump The University of Iowa, USA
Tarmo Uustalu Institute of Cybernetics Tallinn, Estonia
Roel de Vrijer VU University Amsterdam, The Netherlands
Johannes Waldmann HTWK Leipzig, Germany
Hans Zantema Eindhoven University of Technology, The Netherlands

*** CONFERENCE CHAIR ***

Hans Zantema (Eindhoven University of Technology, The Netherlands)

*** STEERING COMMITTEE ***

Mauricio Ayala-Rincon Brasilia University, Brasilia
Frederic Blanqui INRIA Tsinghua University Beijing, China
Salvador Lucas Technical University of Valencia, Spain
Georg Moser (chair) University of Innsbruck, Austria
Masahiko Sakai Nagoya University, Japan
Sophie Tison University of Lille, France

*** FURTHER INFORMATION ***

Questions related to submission, reviewing, and programme should be sent to
the programme committee chair Femke van Raamsdonk, email femke at few.vu.nl.



Pr. Sophie Tison
LIFL - University of Lille- CNRS
www.lifl.fr/~tison
sophie.tison@lifl.fr






--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] VSTTE 2013 - Second call for papers

CALL FOR PAPERS
Fifth Working Conference on
Verified Software: Theories, Tools, and Experiments
(VSTTE 2013)
May 17--19, 2013, Atherton, California
[https://sites.google.com/site/vstte2013/]

The Fifth IFIP Working Conference on Verified Software: Theories,
Tools, and Experiments follows a successful inaugural working
conference at Zurich in 2005 followed by conferences in Toronto
(2008), Edinburgh (2010), and Philadelphia (2012). The goal of this
conference is to advance the state of the art in the science and
technology of software verification, through the interaction of theory
development, tool evolution, and experimental validation.

Scope: We welcome submissions describing significant advances in the
production of verified software, i.e., software that has been proved
to meet its functional specifications. We are especially interested
in submissions describing large-scale verification efforts that
involve collaboration, theory unification, tool integration, and
formalized domain knowledge. We welcome papers describing novel
experiments and case studies evaluating verification techniques and
technologies. Topics of interest include education, requirements
modeling, specification languages, specification/verification
case-studies, formal calculi, software design methods, automatic code
generation, refinement methodologies, compositional analysis,
verification tools (e.g., static analysis, dynamic analysis, model
checking, theorem proving, satisfiability), tool integration,
benchmarks, challenge problems, and integrated verification
environments.

Submission: We are accepting both long (limited to 20 pages) and short
(limited to 12 pages) paper submissions. Short submissions also cover
Verification Pearls describing an elegant proof or proof technique.
Submitted research papers and system descriptions must be original and
not submitted for publication elsewhere. Research paper submissions
must be in LNCS format and must include a cogent and self-contained
description of the ideas, methods, results, and comparison to existing
work. Submissions of theoretical, practical, and experimental
contributions are equally encouraged, including those that focus on
specific problems or problem domains.

Papers can be submitted at http://www.easychair.org/VSTTE13.
Submissions that arrive late, are not in the proper format, or are too
long will not be considered. The post-conference proceedings of VSTTE
2013 will be published by Springer-Verlag in the LNCS series. Authors
of accepted papers will be requested to sign a form transferring
copyright of their contribution to Springer-Verlag. The use of LaTeX
and the Springer llncs class files, obtainable from
http://www.springer.de/comp/lncs/authors.html, is strongly encouraged.

Important Dates:
Feb 22, 2013 (firm): Title/Abstract
Mar 1, 2013 (firm): Full paper submission
Mar 29, 2013: Decision
May 17--19, 2013: Conference
Jun 28, 2013 (firm): Camera-ready

School/Workshops: The conference will be colocated with the Third Summer School
on Formal Techniques, and is preceded by NFM 2013 at NASA Ames
and followed by ICSE 2013 at San Francisco.

Conference Chair: Natarajan Shankar, SRI International

Program Chairs: Ernie Cohen, Microsoft, Andrey Rybalchenko, TU Munich

Program Committee: Josh Berdine, Ahmed Bouajjani, Marsha Chechik,
Jean-Christophe Filliatre, Silvio Ghilardi, Aarti Gupta, Arie Gurfinkel,
Andrew Ireland, Ranjit Jhala, Cliff Jones, Rajeev Joshi, Gerwin Klein,
Daniel Kroening, Gary Leavens, Xavier Leroy, Zhiming Liu, Pete
Manolios, Tiziana Margaria, David Monniaux, Peter Mueller, David
Naumann, Aditya Nori , Peter O'Hearn, Matthew Parkinson, Wolfgang
Paul, Andreas Podelski, Zhang Shao, Willem Visser, Thomas Wies, Jim
Woodcock, Kwangkeun Yi, Pamela Zave, Lenore Zuck

Publicity Chair: Sam Owre, SRI International

Steering Committee: Tony Hoare, Andrew Ireland, Jay Misra, Natarajan
Shankar, Jim Woodcock

--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] ARiSVe 2013 Call for Papers

Call For Papers

1st International Workshop on Automated Reasoning in Software
Verification

http://arisve2013.lri.fr/

Monday, June 10, 2013
Lake Placid, NY, USA
Affiliated with CADE-24

Aims and Scope

The focus of the workshop is application of automated reasoning in the
context of software verification, and, more generally, automation in
software verification. Relevant topics include but are not limited to:

* specifics of verification-related automated reasoning tasks;
* efficient translation of high-level verification conditions to
logical languages of automated reasoning tools;
* handling of the prover's feedback: proofs, models, answer terms;
* logical theories of interest for program verification, decision
procedures, integration into existing ATP and SMT systems;
* combination of automated and user-assisted verification;
* tool presentations, tool comparisons, and benchmarks;
* experience reports on verification of complex algorithms and
real-life software with the use of automated reasoning tools.

Paper Submission and Proceedings

All submissions are reviewed by the programme committee. We expect
that one author of every accepted paper will present their work at the
workshop.

Submissions are limited to 6-12 pages in the LaTeX EasyChair format
easychair.cls (http://www.easychair.org/publications/easychair.zip).
Technical details may be included in an appendix to be
read at the reviewers' discretion. Tool presentation papers and
experience reports are welcome.

Papers should be submitted through EasyChair,
at http://www.easychair.org/conferences/?conf=arisve2013
Submissions must be in PDF format. Electronic version of proceedings
will be freely distributed from the workshop web site.

Important Dates

* Abstract submission deadline: March 8, 2013
* Submission deadline: March 15, 2013
* Notification: April 10, 2013
* Camera ready versions due: May 10, 2013
* Workshop: June 10, 2013

Invited Speaker

K. Rustan M. Leino (Microsoft Research)

Program Committee

* June Andronick (NICTA)
* Clark Barrett (New York University)
* Ernie Cohen (Microsoft Corp.)
* Loïc Correnson (CEA)
* Gidon Ernst (Ausburg University)
* Jean-Christophe Filliâtre (CNRS), co-chair
* Alwyn Goodloe (NASA)
* Matthias Horbach (Koblenz University)
* Vladimir Klebanov (Karlsruhe Institute of Technology)
* Konstantin Korovin (The University of Manchester)
* Rosemary Monahan (National University of Ireland)
* Andrei Paskevich (Université Paris-Sud), co-chair
* Silvio Ranise (Fondazione Bruno Kessler)


--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] SCP Special Issue on Invariant Generation - Final Call for Papers [1 month to go]

(Apologies if you receive multiple copies of this announcement)
------------------------------------------------------------
Science of Computer Programming
Special Issue on Invariant Generation
-- FINAL CALL FOR PAPERS [1 month to go] --
------------------------------------------------------------

This special issue is devoted to the 4th international Workshop on
Invariant Generation (WING 2012)

http://cs.nyu.edu/acsys/wing2012/

which was held on June 30 2012 in Manchester as a satellite event of
IJCAR 2012. The scope of the workshop is the automation of extracting
and synthesising auxiliary properties of programs, in particular
providing, debugging, and verifying auxiliary invariant annotations.
This should be seen in a broad sense and relevant topics include (but
are not limited to) the following:

* Program analysis and verification
* Inductive assertion generation
* Inductive proofs for reasoning about loops
* Applications to assertion generation using:
- abstract interpretation,
- static analysis,
- model checking,
- theorem proving,
- theory formation,
- algebraic techniques
* Tools for inductive assertion generation and verification
* Alternative techniques for reasoning about loops

Submission to this special issue is completely open. We expect
original articles (typically not more than 30 pages) that present
high-quality contributions and must not be simultaneously submitted
for publication elsewhere. Submission of extended versions of
previously published papers is possible as long as the extension is
significant, i.e., the submission can be considered a new paper, the
previous paper is referenced, and the new material is clearly marked.

Submissions must comply with SCP's author guidelines

http://www.elsevier.com/wps/find/journaldescription.cws_home/505623/authorinstructions

and be written in English. Submission is over the SCP website:

http://ees.elsevier.com/scico/default.asp

which you will have to register for if you do not have an account.
When submitting your paper please choose the article type "Special issue: WING 2012".


IMPORTANT DATES
---------------
* Submission of papers: February 11, 2013.
* Notification: April 26, 2013.

GUEST EDITORS
--------------
* Gudmund Grov (Heriot-Watt University, UK)
* Thomas Wies (New York University, USA)

CONTACT
--------------
Please send any queries you may have to:

wing2012@easychair.org


--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] SAT 2013 Revised Call for Papers

[ We apologize if you receive multiple copies of this call. ]

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

2nd Revised CALL FOR PAPERS

Sixteenth International Conference on
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
--- SAT 2013 ---

Helsinki, Finland, July 8-12, 2013
http://sat2013.cs.helsinki.fi/

Abstract submission deadline: February 1, 2013
Paper submission deadline: February 8, 2013

Announcements:
** SAT 2013 OPEN FOR SUBMISSIONS via EasyChair.
** INVITED SPEAKERS to include Edmund M. Clarke (CMU, USA).
** WORKSHOPS to include SMT, PoS, QBF, LaSh.

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

The International Conference on Theory and Applications of
Satisfiability Testing (SAT) is the primary annual meeting for
researchers studying the theory and applications of the propositional
satisfiability problem, broadly construed. Besides plain propositional
satisfiability, it includes Boolean optimization (including MaxSAT and
Pseudo-Boolean (PB) constraints), Quantified Boolean Formulas (QBF),
Satisfiability Modulo Theories (SMT), and Constraint Programming (CP)
for problems with clear connections to Boolean-level reasoning.

Many hard combinatorial problems can be encoded as SAT instances, in the
broad sense mentioned above, including problems in formal verification
(hardware and software), artificial intelligence, and operations research.
More recently, biology, cryptology, data mining, machine learning, and
mathematics have been added to the growing list.

The SAT conference aims to further advance the field by soliciting original
theoretical and practical contributions in these areas with a clear
connection to satisfiability.

SAT 2013 takes place in Helsinki, the capital of Finland. Helsinki is a
vibrant Scandinavian and international city with a lot to offer to visitors.
SAT 2013 takes place during the main summer season, allowing one to
experience the white nights during which the sun almost never sets.


IMPORTANT DATES
===============

(Follow http://sat2013.cs.helsinki.fi/ for updates.)

February 1, 2013: Abstract Submission
February 8, 2013: Paper Submission
March 18, 2013 (approx.): Response from Authors begins, lasts 72 hours
April 3, 2013: Acceptance Notifications
April 22, 2013: Final Camera-Ready Versions

July 8-12, 2013: Main conference and workshops

SCOPE
=====

SAT 2013 welcomes scientific contributions addressing different aspects of
the satisfiability problem. interpreted in a broad sense. Domains include
MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulae (QBF),
Satisfiability Modulo Theories (SMT), Constraint Satisfaction Problems (CSP).

Topics include (but are not restricted to)

Theoretical advances (including exact algorithms, proof complexity, and
other complexity issues);

Practical search algorithms;

Knowledge compilation;

Implementation-level details of SAT solving tools and SAT-based systems;

Problem encodings and reformulations;

Applications (including both novel applications domains and
improvements to existing approaches);

Case studies and reports on insightful findings based on rigorous
experimentation.

OUT OF SCOPE
============

Papers claiming to resolve a major long-standing open theoretical
question in mathematics or computer science (such as those for which a
Millennium Prize is offered, see http://www.claymath.org/millennium)
are outside the scope of the conference because there is insufficient
time in the schedule to referee such papers; instead, such papers
should be submitted to an appropriate technical journal.

SUBMISSIONS
===========

Submissions to SAT 2013 are solicited in three paper categories, describing
original contributions:

REGULAR PAPERS (9 to 15 pages, excluding references)
Regular papers should contain original research, with sufficient detail
to assess the merits and relevance of the contribution.
For papers reporting experimental results, authors are strongly encouraged
to make their data and implementations available with their submission.
Submissions reporting on case studies are also encouraged, and should
describe details, weaknesses, and strengths in sufficient depth.

SHORT PAPERS (up to 8 pages, excluding references)
The same evaluation criteria apply to short papers as to regular papers.
They will be reviewed to the same standards of quality as regular papers,
but will naturally contain less quantity of new material.
Short papers will have the same status as regular papers and be eligible
for the same awards (to be announced later).

TOOL PAPERS (up to 6 pages, excluding references)
A tool paper should describe the implemented tool and its novel features.
Here "tools" are interpreted in a broad sense, including descriptions of
implemented solvers, preprocessors, etc., as well as systems that exploit
SAT solvers or their extensions to solve interesting problem domains, etc.
A demonstration is expected to accompany a tool presentation, and the
software for the tool should be made publicly available.
Papers describing tools that have already been presented previously are
expected to contain significant and clear enhancements to the tool.
Evaluation criteria include (but are not limited to) accurate
documentation, usability, and potential for furthering the state of
the art, with availability of source code being a significant factor.

For all paper categories, the page limits stated above do not include
references, but do include all other material intended to appear in the
conference proceedings. Submissions should use the Springer LNCS style
(without space-squeezing modifications), and be written in English.

Submissions should not be under review elsewhere nor be submitted elsewhere
while under review for SAT 2013, and should not consist of previously
published material.

Submissions not consistent with the above guidelines may be returned
without review.

Besides the paper itself, authors may submit a supplement consisting
of one file in the format of a gzipped tarball (.tar.gz or .tgz) or
a gzipped file (.gz) or a zip archive (.zip). Authors are encouraged
to submit such a supplement when it will help reviewers to evaluate
the paper, and such a supplement will be treated with the same degree
of confidentiality as the paper itself. For example, the supplement might
contain detailed proofs, examples, software, detailed experimental data,
or other material related to the submission. Individual reviewers
may or may not consult the supplementary material; the paper should
be self-contained.

Links to information on the Springer LNCS style is available through
the SAT website at http://sat2013.cs.helsinki.fi/cfp.html .

All papers submissions are done exclusively via EasyChair at
http://www.easychair.org/conferences/?conf=sat2013 .

PROCEEDINGS
===========

All accepted papers will be published in the proceedings of the conference,
which will be published within the Springer LNCS series.

PROGRAM CHAIRS
==============
Matti Jarvisalo University of Helsinki, Finland
Allen Van Gelder University of California at Santa Cruz, USA

PROGRAM COMMITTEE
=================
Gilles Audemard
Fahiem Bacchus
Armin Biere
Maria Luisa Bonet
Lucas Bordeaux
Uwe Bubeck
Samuel Buss
Nadia Creignou
Leonardo de Moura
John Franco
Enrico Giunchiglia
Ziyad Hanna
Marijn Heule
Holger H. Hoos
Jinbo Huang
Tommi Junttila
Matti Jarvisalo
Arist Kojevnikov
Daniel Kroening
Oliver Kullmann
Daniel Le Berre
Florian Lonsing
Ines Lynce
Joao Marques-Silva
Alexander Nadel
Jakob Nordstrom
Albert Oliveras
Ramamohan Paturi
Jussi Rintanen
Olivier Roussel
Ashish Sabharwal
Lakhdar Sais
Roberto Sebastiani
Bart Selman
Peter Stuckey
Stefan Szeider
Naoyuki Tamura
Allen Van Gelder
Toby Walsh

--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] SFM-13:DS school in Bertinoro - first call for participation

***********************************************************
* *
* SFM-13:DS *
* *
* 13th International School on *
* Formal Methods for the Design of *
* Computer, Communication and Software Systems: *
* Dynamical Systems *
* *
* Bertinoro (Italy), 17-22 June 2013 *
* *
* http://www.sti.uniurb.it/events/sfm13ds/ *
* *
***********************************************************
* CALL FOR PARTICIPATION *
* (deadline: 21 March 2013) *
***********************************************************


GENERAL INFORMATION ABOUT SFM
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Formal methods are emerging in computer science as a prominent
approach to the rigorous design of computer, communication and
software systems.

The aim of the SFM series is to offer a good spectrum of
current research in foundations as well as applications of
formal methods, which can be of interest for graduate students
and young researchers who intend to approach the field.

This year SFM is an offspring of the workshops QAPL and MLQA
and is devoted to dynamical systems. It covers topics such as
chaotic dynamics, information theory, systems biology, hybrid systems,
quantum computing, and automata-based models and model checking.


COURSES AND LECTURERS
^^^^^^^^^^^^^^^^^^^^^

The school features the following lectures:

"Introduction to Dynamical Systems"
Herbert Wiklicky (Imperial College London, UK)

"Introduction to Chaotic Dynamics and Fractals"
Abbas Edalat (Imperial College London, UK)

"Information-Theoretic Security Analysis"
Boris Koepf (IMDEA Software, ES)

"Quantum Information Theory"
Renato Renner (ETH Zurich, CH)

"Quantitative Automata-Based Models and Model Checking"
Joost-Pieter Katoen (RWTH Aachen, DE)

"Fluid Analysis of Markov Models"
Jeremy Bradley (Imperial College London, UK)

"Discrete and Hybrid Methods in Systems Biology"
Oded Maler (VERIMAG, FR)

"ODE Analysis of Biological Systems"
Ion Petre (Abo Akademi, FI)

"Model Checking of Biological Models"
Lubos Brim (Masaryk Univ., CZ)

"Fluid Model Checking"
Luca Bortolussi (Univ. Trieste, IT)

"Checking Stability of Hybrid Systems"
Andreas Podelski (Univ. Freiburg, DE)

"Topological Quantum Computing"
Jiannis Pachos (Univ. Leeds, UK)

All participants will receive a copy of a tutorial book published by
Springer as a volume in the Lecture Notes in Computer Science series.


LOCATION
^^^^^^^^

SFM-13:DS will be held in the medieval hilltop town of Bertinoro.

This town is in Emilia Romagna, about 70 km south-east of Bologna,
at an elevation of about 230 m. It can be reached in a couple of
hours from the international airport "G. Marconi" of Bologna by
shuttle (from the airport to the railway station) + train (from
Bologna to Forli`) + bus/taxi (from the railway station to Bertinoro).
The closest airport is the "L. Ridolfi" airport of Forli`, which is
13 km away.

Bertinoro is close to many splendid locations such as Urbino,
Gradara, San Leo, and the Republic of San Marino, as well as some
less well-known locations like the thermal springs of Fratta Terme.

Bertinoro can also be a base for visiting some of the better-known
Italian locations such as Bologna, Rimini, Ravenna, Ferrara, Venezia,
Padova, Verona, Firenze, Pisa, and Siena.

Bertinoro itself is picturesque, with its narrow streets and
walkways winding around the central peak. The school will be held
at the Centro Residenziale Universitario (CRU), an ex-episcopal
fortress that has been converted by the University of Bologna into
a modern conference center with computing facilities and Internet
access. From the fortress, it is possible to enjoy a beautiful vista
stretching from the Apennines to the Adriatic coast and the Alps
over the Po Valley.


ORGANIZATION
^^^^^^^^^^^^

Scientific directors:
* Marco Bernardo (University of Urbino, IT)
* Erik de Vink (Eindhoven University of Technology, NL)
* Alessandra Di Pierro (University of Verona, IT)
* Herbert Wiklicky (Imperial College London, UK)

Secretary:
* Monica Michelacci (CRU Bertinoro, IT)


APPLICATION
^^^^^^^^^^^

Prospective participants should send by 21 March 2013
the application form, available on the school website,
to the two e-mail addresses below:

Marco Bernardo
marco.bernardo AT uniurb.it

Monica Michelacci
mmichelacci AT ceub.it

The registration fee is 600 euros and includes the school material.

The accommodation fee is 350 euros and covers the period June 16-23
(7 nights), double room (to share with another participant),
half board (breakfast and lunch, dinner of June 16 included,
lunch of June 23 excluded).

The reduced accommodation fee for the participants who do not
need a room is 100 euros and covers the period June 17-22
(6 lunches).

A very limited number of grants is available to cover part
of the registration fee (no grant can be requested to cover
the accommodation fee or the travel expenses).

Notification of accepted/rejected applications and grant requests
will be communicated by March 31.

Registration to the school is due by April 20.

No refund is possible for cancellation after May 15.


--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] CiE13 call for papers and special awards

************************************************************************
CALL FOR PAPERS AND SPECIAL AWARDS:

                  CiE 2013: The Nature of Computation

                    Logic, Algorithms, Applications

                             Milan, Italy

                          July  1 - 5, 2013

                    http://cie2013.disco.unimib.it

IMPORTANT DATES:

Submission Deadline for LNCS:                   20 January 2013
Notification of authors:                        4 March 2013
Deadline for final revisions:                   1 April 2013


CiE 2013 is the ninth conference organised by CiE (Computability in
Europe), a European association of mathematicians, logicians, computer
scientists, philosophers, physicists and others interested in new
developments in computability and their underlying significance for the
real world. Previous meetings have taken place in Amsterdam (2005),
Swansea (2006), Siena (2007), Athens (2008), Heidelberg (2009), Ponte
Dalgada (2010), Sofia (2011) and Cambridge (2012).

The Nature of Computation is meant to emphasize the special focus of
CIE13 on the unexpected and strong changes that studies on Nature have
brought in several areas of mathematics, physics, and computer science.
Starting from Alan Turing, research on Nature with a computational
perspective has produced novel contributions, giving rise even to new
disciplines.

AWARDS:

Springer-Verlag has graciously funded two awards that will be given
during the CiE 2013 Conference.

Best student paper

This prize will be awarded for the best student paper presented at CiE
2013, as judged by the Program Committee. A prize of 500 Euros will be
given to the author(s) of the best student-authored paper (or split
between more than one paper if there is a tie). In order to be
considered, a paper has to be submitted in the category 'Regular paper
(eligible for best student paper award)' on EasyChair.
Papers are eligible if all of its authors are full-time students at the
time of submission.

Best paper on Natural Computing

The prize consists of the four volumes of the Handbook of Natural
Computing (see http://cie2013.disco.unimib.it/awards/).
This prize will be awarded to the best paper on Natural Computing
presented at CiE 2013, as judged by the Program Committee. A paper is
eligible if its main topic falls within the scope of Natural Computing,
roughly defined as the set of fields studied in the above handbook. The
Program Committee is the only judge of the relevance of a paper within
the Natural Computing scope. The authors of a paper eligible for the
award must indicate this in the submission notes.

INVITED SPEAKERS

Ulle Endriss (University of Amsterdam)
Lance Fortnow (Georgia Institute of Technology)
Anna Karlin (University of Washington)
Bernard Moret (Ecole Polytechnique Fédérale de Lausanne)
Mariya Soskova (Sofia University)
Endre Szemerédi (Hungarian Academy of Sciences, Rutgers University)

TUTORIAL SPEAKERS
Gilles Brassard (Université de Montréal)
Grzegorz Rozenberg (Leiden Institute of Advanced Computer Science and
University of Colorado at Boulder)

SPECIAL SESSIONS on

Algorithmic Randomness
         organizers: Mathieu Hoyrup, Andre Nies
Data Streams and Compression
         organizers: Paolo Ferragina, Andrew McGregor
Computational Complexity in the Continuous World
         organizers: Akitoshi Kawamura, Robert Rettinger
Computational Molecular Biology
         organizers: Alessandra Carbone, Jens Stoye
Computation in Nature
         organizers: Mark Delay, Natasha Jonoska
History of Computation
         organizers: Gerard Alberts, Liesbeth De Mol

PROGRAM COMMITTEE:

* Gerard Alberts (Amsterdam)
* Luís Antunes (Porto)
* Arnold Beckmann (Swansea)
* Laurent Bienvenu (Paris)
* Paola Bonizzoni (Milan, co-chair)
* Vasco Brattka (Munich and Cape Town, co-chair)
* Cameron Buckner (Houston TX)
* Bruno Codenotti (Pisa)
* Stephen Cook (Toronto ON)
* Barry Cooper (Leeds)
* Ann Copestake (Cambridge)
* Erzsébet Csuhaj-Varjú (Budapest)
* Anuj Dawar (Cambridge)
* Gianluca Della Vedova (Milan)
* Liesbeth De Mol (Gent)
* Jérôme Durand-Lose (Orléans)
* Viv Kendon (Leeds)
* Bjørn Kjos-Hanssen (Honolulu, HI)
* Antonina Kolokolova (St. John's NF)
* Benedikt Löwe (Amsterdam)
* Giancarlo Mauri (Milan)
* Rolf Niedermeier (Berlin)
* Geoffrey Pullum (Edinburgh)
* Nicole Schweikardt (Frankfurt)
* Sonja Smets (Amsterdam)
* Susan Stepney (York)
* S. P. Suresh (Chennai)
* Peter van Emde Boas (Amsterdam)


The PROGRAMME COMMITTEE cordially invites all researchers (European and
non-European) in computability related areas to submit their papers (in
PDF format, max 10 pages using the LNCS style) for presentation at CiE
2013. The submission sitehttps://www.easychair.org/conferences/?conf=cie2013
is open. We particularly invite papers that build bridges between
different parts of the research community.

The CONFERENCE PROCEEDINGS will be published by LNCS, Springer Verlag.

Contact: Paola Bonizzoni - bonizzoni at disco.unimib.it
Website: http://cie2013.disco.unimib.it
************************************************************************

--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs