[Om-announce] VSTTE 2010: Verified Software -- Final Call for Conference Papers

[Gudmund Grov]

(Apologies if you receive multiple copies of this announcement)

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

Third International Conference on Verified Software:
Theories, Tools, and Experiments

Call for Conference & Workshop Papers

*** CONFERENCE PAPER SUBMISSION DEADLINE:  March 29 ***

Edinburgh, Scotland

August 16th-19th, 2010

http://www.macs.hw.ac.uk/vstte10

SPONSORS
National Science Foundation (NSF)
Engineering and Physical Sciences Research Council (EPSRC)
Microsoft Research
Scottish Informatics & Computer Science Alliance (SICSA)
Altran Praxis
Software Systems Engineering Initiative (SSEI)
Formal Methods Europe (FME)

To become a sponsor see:
http://www.macs.hw.ac.uk/vstte10/Sponsors.html

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

The Third International Conference on Verified Software: Theories,
Tools, and Experiments follows a successful inaugural working
conference at Zurich (2005) and a successful conference in Toronto
(2008). This conference is part of the Verified Software Initiative
(VSI), a fifteen-year, cooperative, international project directed
at the scientific challenges of large-scale software verification.
VSI also includes UKCRC's Grand Challenge 6, i.e. Dependable Systems
Evolution. VSTTE is open to anyone who is interested in participating
actively in the VSI effort.

SCOPE
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.  Authors are encouraged to submit work in progress,
particularly if the work involves collaboration, theory unification,
and tool integration.  Topics of interest include

requirements modeling
specification languages
specification/verification case-studies
formal calculi
programming languages
language semantics
software design methods
software testing
automatic code generation
refinement methodologies
type systems
computer security
verification tools (static analysis, dynamic analysis, model
checking, theorem proving, satisfiability)
tool integration
benchmarks
challenge problems
integrated verification environments

We also encourage researchers to submit challenges in theory,
formalization, systems verification, code verification, and
applications. Contributions relating to existing challenges
will also be welcomed, i.e.

* POPLMark (http://tinyurl.com/poplmark)
* Tokeneer (http://www.adacore.com/home/products/sparkpro/tokeneer)
* POSIX file system (http://tinyurl.com/qyzqk9)
* medical devices (http://tinyurl.com/pnztqb)

VENUE
VSTTE 2010 is being hosted by Heriot-Watt University in Edinburgh.
The conference dates coincide with the 2010 Edinburgh International
Festival and the Edinburgh Festival Fringe -- collectively the
largest annual  arts festival on the planet! The technical programme
will take place in the Edinburgh Conference Centre (Riccarton campus),
where accommodation will be available at very competitive rates for
festival time. Social events will be arranged within the city centre,
making VSTTE an unique cultural and scholarly event for 2010!

INVITED SPEAKERS
* Tom Ball (Microsoft Research, Redmond)
* Gerwin Klein (National ICT Australia)
* Matthew Parkinson (University of Cambridge)

SUBMISSIONS
Submitted research papers and system descriptions must be original and
not submitted for publication elsewhere.  Research paper submissions are
limited to 15 proceedings pages in LNCS format and must include a
cogent and self-contained description of the ideas, methods and results,
together with a comparison to existing work. System descriptions
are also limited to 15 proceedings pages in LNCS format. 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

https://www.easychair.org/login.cgi?conf=vstte10.

Submissions that arrive late, are not in the proper format, or are too
long will not be considered.  The proceedings of VSTTE 2010 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.

WORKSHOPS
In addition to the main conference, VSTTE will host two workshops on August 19th:
* VS-Theory focuses on theoretical foundations of software verification. 
Topics range from the difficult and essential study of soundness of delicate 
proof methods, to the discovery of new specification techniques and proof 
methods, to dramatic simplification or unification of existing methods, to as 
yet unknown breakthroughs.
* VS-Tools & Experiments focuses on the development of verification tools and 
their experimental evaluation. Possible topics include interfaces between tools, 
tool integration platforms, and case studies. 

The workshops will provide a forum to present new, possibly unfinished work and will 
also give the opportunity to propose research challenges, which will help form a research 
agenda for the Verified Software Initiative. 

Papers must be written in English using Springer LNCS style. The page limit is 10 pages
for technical papers and 5 pages for proposals of verification challenges. The proceedings will be 
published as a technical report. 

IMPORTANT DATES
March 29 2010: Conference paper submission deadline
May 10 2010: Decisions on papers
May 21 2010: Workshop paper submission
June 1 2010: Final conference paper versions due
June 25 2010: Decisions on workshop papers
July 23 2010: Final workshop paper version
August 16-18 2010: Main conference
August 19 2010: Workshops

RESEARCH STUDENT SUPPORT
A limited number of grants, cover registration and travel, will be available to support PhD 
students wishing to attend VSTTE 2010. More details to follow via the website.

SUMMER SCHOOL
There will be a two-day summer-school preceding the main conference on the 14 and 
15 August. The summer school will give a broad overview of software verification 
techniques,  addressing both bottom-up and top-down approaches with a strong focus 
on the formal representation and reasoning themes. The school consists of eight 
introductory lectures, each concentrating on an unique aspect of one or both of the 
overall themes. The topics of the lectures include inductive theorem proving; SAT and 
SMT solving; proof planning and rippling; rely/guarantee conditions; separation 
logic; operating system verification; and formal analysis of security.

The school is intended for PhD students and researchers working within one or both of 
these themes, however familiarity with any of the techniques is not a prerequisite. 
All lectures are meant to be introductory.  For more information see:

http://dream.inf.ed.ac.uk/events/ssfrr-2010/

COMPETITION
A verification competition will be held at VSTTE 2010. The challenge is
to develop a machine-verified piece of software with respect to a given
specification. The competition will be conducted over a 2.5 hour period
on some evening of the conference. The problem will be presented with a
logical specification and test cases over .5 hours including time for
discussion with 2 hours to construct a solution. Each competing team
can feature up to three members. You can use any tool or combination of
tools as well as libraries, but you cannot modify these tools.  You can
reinterpret the specification to suit your tools and methods, but you
will be judged on the fidelity of your interpretation. The goal is to
produce an executable program and a replayable proof that the program
meets the specification.  It will be possible to code the solution using
integers and arrays. The solutions will be judged for soundness
(absence of bugs) and completeness (presence of proofs). The three best
solutions will be selected and the respective teams will be invited to
make presentations at the tools/experiments workshop. You must
register a copy of the  verification system with the judges prior to the
competition with instructions for replaying proofs and running the
programs.

CONFERENCE CHAIR
Andrew Ireland (Heriot-Watt University; A.Ireland at hw.ac.uk)

PROGRAM CHAIRS
Peter O'Hearn (Queen Mary, University of London; ohearn at dcs.qmul.ac.uk)
Gary T. Leavens (University of Central Florida; leavens at eecs.ucf.edu)
Sriram Rajamani (Microsoft Research; sriram at microsoft.com)

WORKSHOP GENERAL CHAIR
Peter Mueller (ETH Zurich; peter.mueller at inf.ethz.ch)

THEORY WORKSHOP CHAIRS
David Naumann (Stevens Institute of Technology; dnaumann at stevens.edu)
Hongseok Yang (Queen Mary, University of London;  hyang at dcs.qmul.ac.uk)

TOOLS & EXPERIMENTS WORKSHOP CHAIRS
Rajeev Joshi (NASA JPL; rajeev.joshi at jpl.nasa.gov)
Tiziana Margaria (Universitat Potsdam; margaria at cs.uni-potsdam.de)

PUBLICITY CHAIR
Gudmund Grov (Edinburgh University; ggrov at inf.ed.ac.uk)

LOCAL ARRANGEMENT CHAIR
Ewen Maclean (Heriot-Watt University; E.A.H.Maclean at hw.ac.uk)

CONFERENCE PROGRAM COMMITTEE
Ahmed Bouajjani
Leo Freitas
Philippa Gardner
John Hatcliff
Ranjit Jhala
Joseph Kiniry
Rustan Leino
Xavier Leroy
David Naumann
Matthew Parkinson
Wolfgang Paul
Shaz Qadeer
Andrey Rybalchenko
Augusto Sampaio
Zhong Shao
Aaron Stump
Serdar Tasiran
Willem Visser
Chin Wei-Ngan
Stephanie Weirich
Greta Yorsh

STEERING COMMITTEE
Tony Hoare
Jay Misra
Natarajan Shankar
Jim Woodcock


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.