(Apologies if you receive multiple copies of this announcement) ***************************************************************** Third International Conference on Verified Software: Theories, Tools, and Experiments Call for Conference & Workshop Papers 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 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; BiGraphs and formal analysis of security. The following will present at the summer school: * Robert Atkey (University of Strathclyde) & Ewen Maclean (Heriot-Watt University) * Alan Bundy & Lucas Dixon (University of Edinburgh) * Cliff Jones (University of Newcastle) * Gerwin Klein (National ICT Australia) * Robin Milner (University of Cambridge/Edinburgh) * J Strother Moore (University of Texas at Austin) * Natarajan Shankar (SRI) * Graham Steel (INRIA) 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@hw.ac.uk) PROGRAM CHAIRS Peter O'Hearn (Queen Mary, University of London; ohearn@dcs.qmul.ac.uk) Gary T. Leavens (University of Central Florida; leavens@eecs.ucf.edu) Sriram Rajamani (Microsoft Research; sriram@microsoft.com) WORKSHOP GENERAL CHAIR Peter Mueller (ETH Zurich; peter.mueller@inf.ethz.ch) THEORY WORKSHOP CHAIRS David Naumann (Stevens Institute of Technology; dnaumann@stevens.edu) Hongseok Yang (Queen Mary, University of London; hyang@dcs.qmul.ac.uk) TOOLS & EXPERIMENTS WORKSHOP CHAIRS Rajeev Joshi (NASA JPL; rajeev.joshi@jpl.nasa.gov) Tiziana Margaria (Universität Potsdam; margaria@cs.uni-potsdam.de) PUBLICITY CHAIR Gudmund Grov (Edinburgh University; ggrov@inf.ed.ac.uk) LOCAL ARRANGEMENT CHAIR Ewen Maclean (Heriot-Watt University; E.A.H.Maclean@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.