*** Apologies for multiple copies ***
************************
*** 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(a)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(a)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(a)hw.ac.uk)
PROGRAM CHAIRS
Peter O'Hearn (Queen Mary, University of London; ohearn(a)dcs.qmul.ac.uk)
Gary T. Leavens (University of Central Florida; leavens(a)eecs.ucf.edu)
Sriram Rajamani (Microsoft Research; sriram(a)microsoft.com)
WORKSHOP GENERAL CHAIR
Peter Mueller (ETH Zurich; peter.mueller(a)inf.ethz.ch)
THEORY WORKSHOP CHAIRS
David Naumann (Stevens Institute of Technology; dnaumann(a)stevens.edu)
Hongseok Yang (Queen Mary, University of London; hyang(a)dcs.qmul.ac.uk)
TOOLS & EXPERIMENTS WORKSHOP CHAIRS
Rajeev Joshi (NASA JPL; rajeev.joshi(a)jpl.nasa.gov)
Tiziana Margaria (Universitat Potsdam; margaria(a)cs.uni-potsdam.de)
PUBLICITY CHAIR
Gudmund Grov (Edinburgh University; ggrov(a)inf.ed.ac.uk)
LOCAL ARRANGEMENT CHAIR
Ewen Maclean (Heriot-Watt University; E.A.H.Maclean(a)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.
Haskell 2010
ACM SIGPLAN Haskell Symposium 2010
Baltimore MD, United States
30th September, 2010
FINAL CALL FOR PAPERS
http://www.haskell.org/haskell-symposium/2010/
The ACM SIGPLAN Haskell Symposium 2010 will be co-located with the
2010 International Conference on Functional Programming (ICFP), in
Baltimore, Maryland.
The purpose of the Haskell Symposium is to discuss experiences with
Haskell and future developments for the language. The scope of the
symposium includes all aspects of the design, semantics, theory,
application, implementation, and teaching of Haskell.
Topics of interest include, but are not limited to:
* Language Design, with a focus on possible extensions and
modifications of Haskell as well as critical discussions of the
status quo;
* Theory, such as formal treatments of the semantics of the present
language or future extensions, type systems, and foundations
for program analysis and transformation;
* Implementations, including program analysis and transformation,
static and dynamic compilation for sequential, parallel, and
distributed architectures, memory management as well as foreign
function and component interfaces;
* Tools, in the form of profilers, tracers, debuggers,
pre-processors, and suchlike;
* Functional Pearls, being elegant, instructive examples of using
Haskell;
* Applications, Practice, and Experience, using Haskell for
scientific and symbolic computing, database, multimedia and Web
applications, and so forth, as well as general experience with
Haskell in education and industry.
Papers in the latter two categories need not necessarily report
original research results; they may instead, for example, report
practical experience that will be useful to others, reusable
programming idioms, or elegant new ways of approaching a
problem. (More advice appears on the symposium webpage.)
The key criterion for such a paper is that it makes a
contribution from which other Haskellers can benefit. It is not
enough simply to describe a program!
Before 2008, the Haskell Symposium was known as the Haskell
Workshop. The name change reflects both the steady increase of
influence of the Haskell Workshop on the wider community, as well as
the increasing number of high quality submissions. The selection
process is highly competitive. After eleven Haskell Workshops
between 1995 and 2007, the first Haskell Symposium was held in
Victoria in 2008, and the second in Edinburgh in 2009.
Submission Details
* Submission Deadline: Monday, 14th June 2010, 15:00 UTC
* Author Notification: Monday, 12th July 2010
* Final Papers Due : Monday, 2nd August 2010
Submitted papers should be in portable document format (PDF),
formatted using the ACM SIGPLAN style guidelines
(http://www.acm.org/sigs/sigplan/authorInformation.htm) The text
should be in a 9pt font in two columns; the length is restricted to
12 pages, except for "Applications, Practice, and Experience"
papers, which are restricted to 6 pages. Each submission must
adhere to SIGPLAN's republication policy, as explained on the web.
Violation risks summary rejection of the offending submission.
Accepted papers will be published by the ACM and will appear in the
ACM Digital Library.
In addition, we solicit proposals for system demonstrations, based
on running (perhaps prototype) software rather than necessarily on
novel research results. Proposals are limited to 2-page abstracts,
in the same ACM format as papers, and should explain why a
demonstration would be of interest to the Haskell community. They
will be assessed for relevance by the PC; accepted proposals will
be published on the Symposium website, but not formally published
in the proceedings.
Links
* http://www.haskell.org/haskell-symposium,
the permanent homepage of the Haskell Symposium.
* http://www.haskell.org/haskell-symposium/2010,
the 2010 Haskell Symposium web page.
* http://www.icfpconference.org/icfp2010,
the ICFP 2010 web page.
Programme Committee
* Jeremy Gibbons, University of Oxford (chair)
* James Cheney, University of Edinburgh
* Duncan Coutts, Well-Typed LLP
* Sharon Curtis, Oxford Brookes University
* Fritz Henglein, Kobenhavns Universitet
* Tom Schrijvers, Katholieke Universiteit Leuven
* Chung-chieh Shan, Rutgers - The State University of New Jersey
* Martin Sulzmann, Informatik Consulting Systems AG
* Wouter Swierstra, Vector Fabrics
* Peter Thiemann, Universitaet Freiburg
* Andrew Tolmach, Portland State University
* Malcolm Wallace, University of York
This year's ICFP Programming Contest will begin on June 18th (12:00
Noon GMT) and will run till June 21st (12:00 Noon GMT). As in the
previous editions, this is your chance to show that your favorite
programming language is better than all others! The problem statement
and further information will become available at:
http://icfpcontest.org/2010/
Feel free to contact ifcpcont at imn dot htwk-leipzig dot de for
further questions. Good luck!
Wouter
Hello Haskellers,
I'd like to announce the first release of hbeanstalk, a new library
for interfacing with the Beanstalk message/work queue service.
Beanstalk is a simple, fast workqueue service written in C
http://kr.github.com/beanstalkd/ , which is often used to facilitate
moving time-consuming tasks off a web application server, reducing
latency for users.
hbeanstalk is a library that allows Haskell programs to either produce
jobs, or consume them. It's a perfect way to have Haskell do your
heavy lifting. The entire Beanstalk protocol is implemented, so you
can also use hbeanstalk to inspect jobs and gather statistics.
A large number of other languages have clients as well, so using
Beanstalk can be a convenient way to cross language barriers.
http://wiki.github.com/kr/beanstalkd/client-libraries
Check it out on Hackage:
http://hackage.haskell.org/package/hbeanstalk
Or at GitHub:
http://github.com/scsibug/hbeanstalk/
Enjoy,
Greg Heartsfield
