*** Apologies for multiple copies *** ************************ *** Final Call for POSTERS *** 3rd International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2010) Edinburgh, Scotland August 16th-19th, 2010 http://www.macs.hw.ac.uk/vstte10 POSTER SESSION The complementary themes of Theories, Tools and Experiments makes VSTTE an unique conference. Through the introduction of a POSTER session at VSTTE 2010, we are aiming to widen the body of researchers that are involved in the Verified Software Initiative (VSI) and its related Challenges (more details on VSTTE & VSI are provided below). Limited financial support will be available if necessary to enable attendance of both MSc and PhD students whose posters are accepted. Specifically, we aim to attract students who are already engaged in theories or tools or experiments relevant to verification; and give them an opportunity to meet other students and researchers engaged in complementary experiments or theories or tools. Note that the POSTER session is open to all researchers, not just students. With regards to submissions, we require the following: 1. 1-page abstract of your research 2. Poster OR a poster plan 3. For students, a supporting statement from your supervisor Submissions should be sent electronically to vstte10@macs.hw.ac.uk. The timetable for POSTER authors is as follows: JUNE 18: Submission of abstract & poster (plan) deadline JUNE 30: Notification of decision JULY 31: Camera-ready abstract deadline AUGUST 17: Poster session Note that a collection of abstracts for the accepted posters will be distributed at the conference. Poster authors will be expected to bring their poster with them to the conference. Details of the size of the final posters will be provided in due course. Financial support will be allocated on a case-by-case basis, and will support around 30 partial/fully funded places, including 10 SICSA PhD funded places. If you have any queries, please direct them to vstte10@macs.hw.ac.uk MORE DETAILS ON VSTTE 2010 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) WHAT IS THE HISTORY OF VSTTE? 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) 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. 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; 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) * Jane Hillston (University of Edinburgh) * Cliff Jones (University of Newcastle) * Gerwin Klein (National ICT Australia) * 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 (Universitat 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.