[isabelle] Final Call for Participation: VSTTE'08

[paige at cs.york.ac.uk]

FINAL CALL FOR PARTICIPATION
Second Working Conference on
Verified Software: Theories, Tools, and Experiments (VSTTE 2008)
Oct 6--9, 2008, Toronto, Canada

http://qpq.csl.sri.com/vsr/vstte-08

Program Chairs:
   Jim Woodcock, University of York
   jim at cs.york.ac.uk

   Natarajan Shankar, SRI International
   shankar at csl.sri.com

Conference Chair:

   Eric Hehner, University of Toronto
   hehner at cs.utoronto.ca

The Second Working Conference on Verified Software: Theories,
Tools, and Experiments follows a successful inaugural working conference
at Zurich, Switzerland in 2005. This conference formally inaugurates the
Verified Software Initiative (VSI), a fifteen-year, cooperative,
international project directed at the scientific challenges of large- 
scale
software verification. The Working Conference is open to anyone who is
interested in participating actively in the VSI effort.

There will be plenary sessions Monday (6 Oct) through Thursday (9 Oct).
Thursday is also devoted to three workshops: one on Theories, one on
Tools, and one on Experiments. There will be a conference dinner on
Wednesday evening on a boat that tours the Toronto harbour and  
Scarborough
Bluffs and the shore of Lake Ontario.

Registration can be made online at http://www.regonline.ca/VSTTE08
Regular registration is CAN $550; student registration is CAN $275.

Local information can be found at http://www.cs.york.ac.uk/vstte08/

The Conference Venue is the Novotel Toronto Centre; all sessions for the
conference will take place at this hotel. Please make your own
reservation, and quote "Verified Software Conference" to obtain the
conference rate of $169 (plus taxes) per night.
http://www.novotel-toronto-centre.com/


Invited Talks:

   * Andreas Podelski, University of Freiburg.
     Verification, Least-Fixpoint Checking, Abstraction
   * Sriram Rajamani, Microsoft Research.
     Combining Tests and Proofs
   * John Reynolds, Carnegie-Mellon University.
     Readable Formal Proofs
   * Moshe Vardi, Rice University.
     From Verification to Synthesis

Tutorials:

   * Eric Hehner.
     Practical Predicative Programming Primer
   * Ernie Cohen.
     Verifying the Microsoft Hypervisor
   * Leonardo de Moura.
     SMT at Microsoft

Accepted Papers:

   * Artem Starostin and Alexandra Tsyban.
     Verified Process-Context Switch for C-Programmed Kernels
   * Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa and Koichi
Takahashi.
     Verification of the Deutsch-Schorr-Waite marking algorithm with
Modal Logic
   * Xinyu Feng, Zhong Shao, Yu Guo and Yuan Dong.
     Combining Domain-Specific and Foundational Logics to Verify  
Complete
Software Systems
   * Bruce Weide, Murali Sitaraman, Heather K. Harton, Bruce Adcock,
Paolo Bucci, Derek Bronish, Wayne D. Heym, Jason Kirschenbaum and
David Frazier.
     Incremental Benchmarks for Software Verification Tools and  
Techniques
   * Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone.
     Verified Protection Model of the seL4 Microkernel
   * Gerwin Klein and Rafal Kolanski.
     Mapped Separation Logic
   * Eyad Alkassar, Mark Hillebrand, Dirk Leinenbach, Norbert W.  
Schirmer
and Artem Starostin.
     The Verisoft Approach to Systems Verification
   * Eyad Alkassar and Mark Hillebrand.
     Formal Functional Verification of Device Drivers
   * Mark Bickford.
     Unguessable Atoms: A Logical Foundation for Security
   * Joey Coleman.
     Expression Decomposition in a Rely/Guarantee Context
   * Matthias Daum, Jan Dörrenbächer, Burkhart Wolff and Mareike  
Schmidt.
     A Verification Approach for System-level Concurrent Programs
   * Anindya Banerjee, Michael Barnett and David Naumann.
     Boogie Meets Regions: a Verification Experience Report
   * Rustan Leino, Peter Müller and Angela Wallenburg.
     Flexible Immutability with Frozen Objects
   * Patrice Chalin, Perry R. James and George Karabotsos.
     JML4: Towards an Industrial Grade IVE for Java and Next Generation
Research Platform for JML
   * Gregory Dennis, Kuat Yessenov and Daniel Jackson.
     Bounded Verification of Voting Software
   * Daniel Leivant.
     Propositional dynamic logic for recursive procedures

Workshops:

* Workshop on Theories (David Naumann and Peter O'Hearn)
http://www.cs.stevens.edu/~naumann/vstte-theory-2008/

* Workshop on Tools (Daniel Kroening and Tiziana Margaria)
http://www.verify.ethz.ch/vstte-tools-2008/

* Workshop on Experiments (Rajeev Joshi and Joe Kiniry)
http://web.mac.com/kiniry/VS-EXPERIMENTS_2008/Workshop_on_Experiments_in_Verified_Software.html


Program Committee:

Egon Borger, Supratik Chakraborty, Patrick Cousot, Jin Song Dong,
Jose Luiz Fiadeiro, Kokichi Futatsugi, Chris George, Ian Hayes,
Eric Hehner, Rajeev Joshi, Joseph Kiniry, Yassine Lakhnech,
Gary Leavens, Zhiming Liu, Peter Manolios, Tiziana Margaria,
David Naumann, Peter O'Hearn, Ernst-Rudiger Olderog, Wolfgang Paul,
Augusto Sampaio, Mark Utting, Jian Zhang

Steering Committee:
Tony Hoare, Jay Misra


_______________________________________________
Kestrel-announcements mailing list
Kestrel-announcements at kestrel.edu