2011-11-28

[Caml-list] PADL 2012 Call for Participation

Call for Participation
======================

14th International Symposium on
Practical Aspects of Declarative Languages (PADL 2012)

http://research.microsoft.com/~crusso/padl12

Philadelphia, Pennsylvania, USA, January 23-24, 2012
Co-located with ACM POPL'12


You are cordially invited to PADL'12. PADL is a forum for researchers
and practitioners to present original work emphasizing novel
applications and implementation techniques for all forms of
declarative concepts, including functional, logic and
constraints. PADL'12 is sponsored by Association for Logic Programming
with cooperation of ACM SIGPLAN and support by Microsoft Research.


Registration
============
To register for PADL'12, please follow the instructions at:

https://regmaster3.com/2012conf/POPL12/register.php

The early registration deadline is December 24, 2011. The registration
fee will cover a copy of the symposium proceedings, refreshments, and
an informal dinner.

Hotel Information
=================

PADL will be co-located with POPL at the Sheraton Society Hill Hotel
in Philadelphia. Please visit POPL's web site to make reservations at
the special conference rate.

Program
=======

The symposium will include invited talks by Boon Thau Loo and Don
Stewart, and 19 technical papers selected from 41 submissions.

The preliminary program is as follows:

Invited Talk (9:00-10:00)

* Boon Thau Loo
Recent Advances in Declarative Networking

Break (10:00-10:30)
Session 1: Applications (10:30-12:00)

* Mayer Goldberg and Guy Wiener
A Declarative Approach for Software Modeling
* Sergio Antoy and Michael Hanus
Contracts and Specifications for Functional Logic Programming
* Pedro M. Martins, Julie A. McCann and Susan Eisenbach
The Environment as an Argument

Lunch (not provided) (12:00-13:30)
Session 2: Logic Programming (13:30-15:30)

* Yuliya Lierler, Shaden Smith, Mirek Truszczynski and Alex Westlund
Weighted-Sequence Problem: ASP vs CASP and Declarative vs Problem-Oriented Solving
* Marcello Balduccini and Yuliya Lierler
Practical and Methodological Aspects of the Use of Cutting-Edge ASP Tools
* Christian Theil Have and Henning Christiansen
Efficient tabling of structured data using indexing and program transformation
* Dario Campagna, Beata Sarna-Starosta and Tom Schrijvers
Optimizing Inequality Joins in Datalog with Approximated Constraint Propagation

Break (15:30-16:00)
Session 3: Parallelism and Concurrency (16:00-17:30)

* Elvira Albert, Puri Arenas and Miguel Gomez-Zamalloa
Symbolic Execution of Concurrent Objects in CLP
* Pablo Chico De Guzmán, Amadeo Casas, Manuel Carro and Manuel Hermenegildo
A Segment-Swapping Approach for Executing Trapped Computations
* Michael Lesniak
Palovca: Describing and Executing Graph Algorithms in Haskell

Informal PADL Dinner (Place: TBA)

Tuesday, January 24, 2012
Breakfast (8:00-9:00)
Invited Talk (9:00-10:00)

* Don Stewart
Make Things Now! Pragmatic Functional Programming in Haskell

Break (10:00-10:30)
Session 4: Domain Specific Languages I (10:30-12:00)

* Kenny Zhu, Kathleen Fisher and David Walker
LearnPADS++: Incremental Inference of Ad Hoc Data Formats
* Jeroen Bransen, Arie Middelkoop, Atze Dijkstra and S. Doaitse Swierstra
The Kennedy-Warren algorithm revisited: ordering Attribute Grammars
* Nicholas Coleman
Distributed Policy Specification and Interpretation with Classified Advertisements

Lunch (not provided) (12:00-13:30)
Session 5: Domain Specific Languages II (13:30-15:30)

* Andy Gill and Bowe Neuenschwander
Handshaking in Kansas Lava using Patch Logic
* Daniel Winograd-Cort, Hai Liu and Paul Hudak
Virtualizing Real-World Objects in FRP
* Edwin Brady and Kevin Hammond
Resource-safe Systems Programming with Embedded Domain Specific Languages
* David Broman and Henrik Nilsson
Node-Based Connection Semantics for Equation-Based Object-Oriented Modeling Languages

Break (15:30-16:00)
Session 6: Numerics (16:00-17:00)

* Paul Tarau
A Declarative Specification of Tree-based Symbolic Arithmetic Computations
* Vincent St-Amour, Sam Tobin-Hochstadt, Matthew Flatt and Matthias Felleisen
Typing the Numeric Tower


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

2011-11-03

[Caml-list] SAT 2012: Call for Papers

-------------------------------------------------------------------------
15th International Conference on
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
--- SAT 2012 ---

Trento, Italy, June 17-20th, 2012
http://sat2012.fbk.eu/
-------------------------------------------------------------------------

AIM and SCOPE
=============

The International Conference on Theory and Applications of
Satisfiability Testing (SAT) is the primary annual meeting for
researchers studying the propositional satisfiability
problem. Importantly, here SAT is interpreted in a rather broad sense:
besides plain propositional satisfiability, it includes the domains of
MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean
Formulae (QBF), Satisfiability Modulo Theories (SMT), Constraints
Programming (CSP) techniques for word-level problems and their
propositional encoding.

To this extent, many hard combinatorial problems can be encoded as SAT
instances, in the broad sense mentioned above, including problems that
arise in hardware and software verification, AI planning and
scheduling, OR resource allocation, etc. The theoretical and practical
advances in SAT research over the past twenty years have contributed
to making SAT technology an indispensable tool in these domains.

SAT 2012 will take place in Trento, Italy, a cosmopolitan city set in
a spectacular mountain scenery, and home to a world-class university
and research centres.

RELEVANT TOPICS
===============

The topics of the conference span practical and theoretical research
on SAT (in the broader sense above) and its applications, and include,
but are not limited to:

* Theoretical issues
- Combinatorial Theory of SAT
- Proof Systems and Proof Complexity in SAT
- Analysis of SAT Algorithms
* Solving:
- Improvements of current solving procedures
- Novel solving procedures, techniques and heuristics
- Incremental solving
* Beyond solving:
- Functionalities (e.g., proofs, unsat-cores, interpolants,...)
- Optimization
* Applications
- SAT techniques for other domains
- Novel Problem Encodings
- Novel Industrial Applications of SAT

A more detailed description can be found on the web site.

INVITED SPEAKERS
================

We are honored to announce the following invited speakers at SAT'12:

* Aaron Bradley, Boulder, USA.
"SAT-based Verification with IC3: Foundations and Demands"

* Donald Knuth, Stanford, USA.
"Satisfiability and The Art of Computer Programming"

The presence of both speakers has been confirmed, although the titles
of the talks may be provisional.

PAPER SUBMISSION
================

Papers must be edited in LATEX using the LNCS format and
be submitted electronically as PDF files via EasyChair.
We envisage three categories of submissions:

REGULAR PAPERS. Submissions, not exceeding fourteen (14) pages, should
contain original research, and sufficient detail to assess the
merits and relevance of the contribution. For papers reporting
experimental results, authors are strongly encouraged to make their
data available with their submission. Submissions reporting on case
studies in an industrial context are strongly invited, and should
describe details, weaknesses and strength in sufficient
depth. Simultaneous submission to other conferences with proceedings
or submission of material that has already been published elsewhere
is not allowed.

TOOL PRESENTATIONS. Submissions, not exceeding four (4) pages, should
describe the implemented tool and its novel features. A
demonstration is expected to accompany a tool presentation. Papers
describing tools that have already been presented in other
conferences before will be accepted only if significant and clear
enhancements to the tool are reported and implemented.

EXTENDED ABSTRACTS/POSTERS. Submissions, not exceeding two (2) pages,
briefly introducing work in progress, student work, or preliminary
results. These papers are expected to be presented as posters at the
conference.

Further information about paper submission, including a more detailed
description of the scope and specification of the three submission
categories, will be made available at SAT'12 web page. The review
process will be subject to a rebuttal phase.

IMPORTANT DATES:
================
Abstract Submission: 05/02/2012
Paper Submission: 12/02/2012
Rebuttal phase: 28-30/03/2012
Final Notification: 12/04/2012
Final Version Due: 04/05/2012
Conference: 17-20/06/2012

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

The proceedings of SAT'12 will be published by Springer-Verlag in the
LNCS series.

PROGRAM CHAIRS
==============

Alessandro Cimatti -- FBK-Irst, Trento, Italy
Roberto Sebastiani -- DISI, University of Trento, Italy

PROGRAM COMMITTEE
=================

Dimitris Achlioptas -- UC Santa Cruz, USA
Fahiem Bacchus -- University of Toronto, Canada
Paul Beame -- University of Washington, USA
Armin Biere -- Johannes Kepler University, Austria
Randal Bryant -- Carnegie Mellon University, USA
Uwe Bubeck -- University of Paderborn, Germany
Nadia Creignou -- LIF Marseille, France}
Leonardo DeMoura -- Microsoft Research, USA
John Franco -- University of Cincinnati, USA
Malay Ganai -- NEC, USA
Enrico Giunchiglia -- Università di Genova, Italy
Yussef Hamadi -- Microsoft Research, UK
Zyiad Hanna -- Jasper, USA
Holger Hoos -- University of British Columbia, Canada
Marijn Heule -- Johannes Kepler University, Austria
Kazuo Iwama -- Kyoto University, Japan
Oliver Kullmann -- University of Wales Swansea, UK
Daniel Le Berre -- Université d'Artois, France
Ines Lynce -- Instituto Superior Técnico, Portugal
Panagiotis Manolios -- Northeastern University, USA
Joao Marques-Silva -- University College Dublin, Ireland
David Mitchell -- Simon Fraser University, Canada
Alexander Nadel -- Intel, Israel
Jussi Rintanen -- The Austrailan National University, Australia
Lakhdar Sais -- Université d'Artois, France
Karem Sakallah -- University of Michigan, USA
Bart Selman -- Cornell University, USA
Laurent Simon -- Université Paris 11, France
Carsten Sinz -- Karlsruhe Institute of Technology, Germany
Niklas Sorensson -- Chalmers University, Sweden
Ofer Strichman -- Technion, Israel
Stefan Szeider -- Vienna University of Technology, Austria
Allen Van Gelder -- University of California, Santa Cruz, USA
Toby Walsh -- University of New South Wales, Australia
Xishun Zhao -- Sun Yat-Sen University, China

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

[Caml-list] Call for Papers and Workshop Proposals: DisCoTec 2012, Stockholm, Sweden (COORDINATION + DAIS + FMOODS/FORTE)

[We apologize for multiple copies]

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

Call for Papers

DisCoTec 2012

7th International Federated Conference on
Distributed Computing Techniques

http://discotec.ict.kth.se/

Stockholm, Sweden, June 13-16 2012

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

The DisCoTec series of federated conferences is one of the major
events sponsored by the International Federation for Information
processing (IFIP). The main conferences are:

* COORDINATION
* DAIS
* FMOODS & FORTE

All conferences share the same deadlines:

* Important Dates *

February 10, 2012 Abstract Submission
February 17, 2012 Paper Submission
March 26, 2012 Notification of Acceptance
April 9, 2012 Camera ready version
June 13-16 2012 Conference and Workshops

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

COORDINATION
14th International Conference on Coordination Models and Languages

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

* Scope *

As ICT technologies and software-intensive systems are increasingly
embedded into the fabric of everyday life, effective coordination
techniques are needed to enhance our ability to develop software that
is responsive to emerging societal demands and changing application
needs, exploits effectively recent advances in computing and
communication technology, and is capable of adaptive behaviour in the
short and in the long term. COORDINATION is the premier forum for
exposing innovating research results and relevant experience reports
on software technologies for collaboration and coordination in
concurrent, distributed, and socio-technical systems. Its distinctive
feature is the emphasis on high-level abstractions that capture
interaction patterns manifest at all levels of the software architecture
and extending into the realm of the end-user and social domain.


Coordination 2012 seeks high-quality contributions on the usage, study,
design and implementation of languages, models and techniques for
coordination in distributed, concurrent, pervasive, and multicore
software systems. The focus is on languages, formalisms, models,
middleware, patterns, and algorithms that conceptually support a proper
engineering of the interaction dimension. Research paper should
demonstrate an ability to increase modularity, adaptivity, simplify
reasoning, and ultimately enhance the software development process and
its integration into a socio-techical context. Both practical and
foundational perspectives are of interest.Given the increasing importance
of coordination models and technologies in almost every domain of our
existence, the organizers of Coordination 2012 are keen to provide a
forum for studies that address practical concerns and industrial grade
solutions, e.g., the introduction of concurrency and distribution
concepts to novel domains, comparative evaluations of programming models
on important problems, and the adoption of domain-specific languages.
Experience reports are thus welcome that describe lessons learned from
the application of proposed models and techniques to problems in the real
world.In addition, the conference this year will welcome short "Visions
in Progress" papers that tries to look far ahead into the future of ICT
and society to expose innovative - though preliminary - ideas on highly
innovative models, technologies, or applications, related to coordination
models/languages/technologies.

* Publication *

All Research and Experience Papers must report on original unpublished
work and cannot be under review for publication elsewhere. Innovation,
scientific and technical soundness, and the capability to prove the
advantages of the proposed techniques, other than their potential for
applicability, will be the key criteria for evaluating submissions.
Maximum length: 15 pages.

Visions in Progress papers can report on work that has already been
presented elsewhere, but the paper in itself must be a new synthesis and
must clearly outline the motivation for the vision and the path that can
eventually lead to its realization. Solid motivations, radical innovation,
capability to look far beyond the state of the art, and feasibility of
the proposed vision, will be the key criteria for evaluating submissions.
Maximum length: 5 pages.

All contributions should be submitted electronically as postscript or PDF,
using the Springer LNCS style, via EasyChair. Submissions exceeding the
state length will be rejected without reviewing.

Each paper will undergo a thorough evaluation and the conference
proceedings will be published by Springer-Verlag in the LNCS series.
Proceedings will be made available at the conference. Submission is a
firm commitment that at least one of the authors will attend the conference,
if the paper is accepted.


* Program Committee Co-Chairs *

Marjan Sirjani Reykjavik University, Iceland
Franco Zambonelli Universita degli Studi di Modena e Reggio Emilia, Italy

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

DAIS
12th IFIP International Conference on
Distributed Applications and Interoperable Systems

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

* Scope *

The DAIS conference series addresses all aspects of distributed
applications, including their architecture, design, implementation and
operation, the supporting middleware, appropriate software engineering
methodologies and tools, as well as experimental studies and practice reports.
DAIS'12 is the 12th event in a series of successful international
conferences started in 1997. It will provide a forum for researchers,
application and platform service vendors, and users, to discuss and learn
about new approaches, trends, concepts and experiences in the fields of
distributed computing.

* Publication *

DAIS'12 seeks:
- Full research papers in no more than 14 pages.
- Full experimental and evaluation studies, case studies, and practice
reports in no more than 14 pages.
- Work-in-progress papers, describing ongoing work and interim results,
in no more than 6 pages.

All papers must be original, unpublished, and not submitted for publication
elsewhere. Contributions should be submitted electronically as PDF, using
the SPRINGER LNCS style. Each paper will undergo a thorough process of
review and the conference proceedings will be published by Springer-Verlag
in the LNCS series. Proceedings will be made available at the conference.
Submission implies that at least one author will register and attend the
conference if the paper is accepted.

* Program Committee Co-Chairs *

Karl M. Goeschka Vienna University of Technology, Austria
Seif Haridi Swedish Institute of Computer Science, Sweden

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

FMOODS & FORTE
IFIP International Conference on
Formal Techniques for Distributed Systems
joint international conference
14th Formal Methods for Open Object-Based Distributed Systems
32nd Formal Techniques for Networked and Distributed Systems

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

* Scope *

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

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

The conference encourages 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. FMOODS & 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.

* Publication *

The FMOODS & FORTE 2012 conference calls for high quality papers presenting
research results and/or application reports related to the research areas
in conference scope.

Like in the past, the conference proceedings will be published by Springer
in the LNCS Series. Proceedings will be made available at the conference.

All papers must be original, unpublished, and not submitted for publication
elsewhere. Contributions should be submitted electronically in PDF via the
EasyChair system. Each paper will undergo a peer review of at least 3
anonymous reviewers. The papers must be prepared using the SPRINGER LNCS style.

Research papers, experience reports as well as tool or system description
papers are all encouraged. Papers must not exceed 15 pages in length,
including figures and references. For referees' convenience, any
additional material that may help assessing the merits of the submission
but not to be included in the final version, like some detailed proofs,
may be placed in a clearly marked appendix (not to be counted in the
page limit). Referees can ignore the appendix, and papers must be
understandable without them.

Submissions not adhering to the above specified constraints may be rejected
immediately, without review.

* Program Committee Co-Chairs *

Holger Giese Hasso Plattner Insitute, University of Potsdam, Germany
Grigore Rosu University of Illinois at Urbana-Champaign, USA

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

DisCoTec 2012 Call for Workshop Proposals

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

DisCoTec 2012 invites proposals for one day workshops to be part of the
joint event. DisCoTec 2012 hosts conferences in the area of coordination
languages, distributed systems and formal methods for distributed
systems, ranging from practice to theory. We invite workshops in these
areas to provide a forum for presentations of preliminary research
results and ongoing work as well as presentations of research work
to a focused audience. DisCoTec workshops provide a vivid and open
forum for discussions.

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

* Important Dates *

January 13, 2012 Workshop proposal deadline
January 20, 2012 Workshop proposal notification
June 13-16, 2012 Main Conference
June 16, 2012 Workshops

Submission and notification deadlines of the workshops are at the
discretion of the individual workshop organizers, however notification
must be no later than the early registration deadline for DisCoTec.

* Proposal Submission Guidelines *

Workshop proposals must be written in English, not exceed 5 pages with a
reasonable font and margin, and be submitted in PDF format via email to
Rui Oliveira (rco at di.uminho.pt).

Proposals should include the following information:

* The title, theme, and goals of the workshop.
* The targeted audience and the expected number of
participants. We prefer that workshops remain open to participation
from any members of the community, but by-invitation-only workshops
will also be considered. Please explicitly state your preference.
* The publicity strategy that will be used by the workshop organizers
to promote the workshop.
* The participant solicitation and selection process.
* Publication plan. Each workshop is responsible for managing its own
publication (e.g., pre- or post- proceedings), if any is desired.
* Approximate budget proposal (see section Budget below for details).
* A preliminary version of the call for papers. This CFP must include
important dates including submission, notification, and camera-ready
deadlines.
* The equipment and any other resource necessary for the organization
of the workshop.
* A brief description of the organizer's background, including relevant
past experience on organizing workshops and contact information.

* Review Process *

Workshop proposals will be reviewed by the following committee:

* Jim Dowling, KTH University, Stockholm (DiScoTec 2012 general chair)
* Rui Oliveira, Universidade do Minho, Portugal (workshops chair)


Acceptance is based on an evaluation of the workshop's potential for
generating useful results, the timeliness and expected interest in the
topic, the organizer's ability to lead a successful workshop, and
potential for attracting sufficient number of participants.

* Workshop Publicity *

Workshop publicity is responsibility of the organizers. In particular they
are responsible for the following items:

1. A workshop description (200 words) for inclusion on the DisCoTec site.
2. Hosting and maintaining of web pages either on the DisCoTec website or
linked from the DisCoTec site..
3. Workshop proceedings, if any. If there is enough interest, the
organizer of DisCoTec 2012 may contact the editor-in-chief of the
Electronic Proceedings in Theoretical Computer Science
(http://info.eptcs.org/) for having a common volume dedicated to the
workshops of DisCoTec 2012.
4. Publicising the event.

* Budget *

DisCoTec will provide registration and organizational support for the
workshops. Registration fees must be paid for all participants,
including organizers and invited guests.

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

* Contact Information *

Rui Oliveira, rco at di.uminho.pt

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

DisCoTec 2012 Organizing Committee

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

* General Chair *
Jim Dowling KTH, Stockholm

* Workshops Chair *
Rui Oliveira Universidade do Minho, Portugal

* Posters Chair *
Sarunas Girdzijauskas SICS, Sweden

* Publicity Chair *
Ivana Dusparic Trinity College Dublin, Ireland

* Industry Session Chair *
Gyorgy Dan KTH, Sweden

* Steering Committee *
Elie Najm (Chair) Telecom-ParisTech, France
Rocco De Nicola University of Florence, Italy
Kurt Geihs University of Kassel, Germany
Farhad Arbab (Coordination) CWI, Netherlands
Lea Kutvonen (DAIS) University of Helsinki, Finland
John Derrick (FMOODS-FORTE) University of Sheffield, UK
Frank de Boer CWI, Netherlands
Marjan Sirjani Reykjavik University, Iceland


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

2011-11-02

[Caml-list] VSTTE 2012 Verification Competition: last call for participation

VSTTE 2012 Verification Competition starts Tuesday 8 November 2011!
Follow the announcements at the competition Web page:

https://sites.google.com/site/vstte2012/compet

Join the discussion group or subscribe to our mailing list:

http://groups.google.com/group/vstte-2012-verification-competition

vstte-2012-verification-competition+subscribe@googlegroups.com


VSTTE 2012 Verification Competition
-----------------------------------

A software verification competition is organized on behalf of the
VSTTE 2012 conference (https://sites.google.com/site/vstte2012).
The purposes of this competition are: to help promote approaches and
tools, to provide new verification benchmarks, to stimulate further
development of verification techniques, and to have fun.

The contest takes place during 48 hours, on 8-10 November 2011, two
months prior to the conference. Problems will be put on the website of
the conference.  Solutions must be sent by email to the competition
organizers. Any programming language, specification language, and
verification tool is allowed.


Problems
--------
There will be several, independent problems.  Each problem is
presented as a sequential algorithm, using English or pseudocode, and
a list of properties to formally prove about it, also expressed in
plain English and standard mathematical notation. Participants have
liberty to implement the proposed algorithms in functional,
imperative, object-oriented, or any other programming style.


Evaluation
----------
Submissions are ranked according to the total sum of points they
score.  Each problem includes several sub-tasks, e.g. safety,
termination, behavioral correctness, etc., and each sub-task is given
a number of points.  While evaluating the submissions, judges take
into account the accuracy and thoroughness of solutions as well as
their terseness and elegance.  (Clarity is more important than brevity.)
A certain degree of subjectivity is inevitable and should be
considered as part of the game.


Participants
------------
Anybody interested can take part in the contest. Team work is allowed.
Only teams up to 4 members are eligible for the first prize.
Individual participants may belong to several teams.
However, the same solution cannot appear in different submissions.

The technical requirements are as follows:
- access to the web to download the problems (PDF file);
- access to the email to submit the solutions;
- any software used in the solutions should be freely available for
noncommercial use to the public. This does not exclude closed source
programs (such as Microsoft's Z3). Software must be usable on an x86
Linux or Windows machine. Participants are authorized to modify
their tools during the competition.


Submission
----------
A submission is a (possibly compressed) tarball that contains exactly
one directory (named by the team, for instance). This directory should
contain at least a text file named README, and one directory for each
problem solved. Thus it must look like:

team/ -+
      +- README
      +- problem1/
      +- problem2/
      +  ...
      +- problemN/
      +- other stuff...

The README file should contain the following information:
- contact information (email);
- detailed description of the submitted solutions: properties that
have been specified and/or proved, restrictions and/or
generalizations, anything that may facilitate the review;
- detailed instructions to replay the solutions, including the
software to use, URLs to get it from, compilation commands, etc.

Several solutions can be submitted for the same problem (for instance,
using different tools). They should be stored in separate subdirectories
of problemI/. During evaluation, only the best-faring solution will be
taken into account.


Organizers
----------
- Jean-Christophe Filliâtre (CNRS, France)
- Andrei Paskevich (Univ Paris Sud, France)
- Aaron Stump (University of Iowa, USA)


Schedule
--------
Tuesday   8 Nov 2011, 15:00 UTC - competition starts
Thursday 10 Nov 2011, 15:00 UTC - competition stops

Monday 12 Dec 2011 - the winner is notified
28-29 Jan 2012 - results are announced at VSTTE 2012


Prize
-----
The winner is awarded a talk slot at VSTTE 2012, to present any
research of his/her choice of interest for the VSTTE community. In
particular, a presentation of solutions to the competition problems
and/or of the techniques and system used would be appreciated.


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