[isabelle] Final Call for Participation: VSTTE'08
- To: formal-methods at cs.uidaho.edu, isabelle-users at cl.cam.ac.uk, qpq-general at qpq.org, pvs at csl.sri.com, theorem-provers at ai.mit.edu, types at cis.upenn.edu, lics at research.bell-labs.com, acl2 at cs.utexas.edu, formal-methods at cs.uidaho.edu, fsdm at it.uq.edu.au, lfcs-interest at dcs.ed.ac.uk, zeves at ora.on.ca, amast at cs.utwente.nl, concurrency at cwi.nl, calculemus-ig at mathweb.org, lprolog at cs.umn.edu, caml-list at pauillac.inria.fr, categories at mta.ca, comlab at comlab.ox.ac.uk, complog at cs.nmsu.edu, compulognet-parimp at dia.fi.upm.es, coq-club at pauillac.inria.fr, hol-info at lists.sourceforge.net, info-hol at cs.uidaho.edu, prog-lang at diku.dk, theorem-provers at ai.mit.edu, theory-logic at cs.cmu.edu, theorynt at listserv.nodak.edu, types at cis.upenn.edu, mizar-forum at mizar.uwb.edu.pl, poplmark at lists.seas.upenn.edu, rewriting at ens-lyon.fr, event at in.tu-clausthal.de, puml-list at cs.york.ac.uk
- Subject: [isabelle] Final Call for Participation: VSTTE'08
- From: paige at cs.york.ac.uk
- Date: Thu, 11 Sep 2008 19:45:42 +0100 (BST)
- Importance: Normal
- User-agent: SquirrelMail/1.4.15
FINAL CALL FOR PARTICIPATION
Second Working Conference on
Verified Software: Theories, Tools, and Experiments (VSTTE 2008)
Oct 6--9, 2008, Toronto, Canada
Jim Woodcock, University of York
jim at cs.york.ac.uk
Natarajan Shankar, SRI International
shankar at csl.sri.com
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.
* 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
* Eric Hehner.
Practical Predicative Programming Primer
* Ernie Cohen.
Verifying the Microsoft Hypervisor
* Leonardo de Moura.
SMT at Microsoft
* Artem Starostin and Alexandra Tsyban.
Verified Process-Context Switch for C-Programmed Kernels
* Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa and Koichi
Verification of the Deutsch-Schorr-Waite marking algorithm with
* Xinyu Feng, Zhong Shao, Yu Guo and Yuan Dong.
Combining Domain-Specific and Foundational Logics to Verify Complete
* Bruce Weide, Murali Sitaraman, Heather K. Harton, Bruce Adcock,
Paolo Bucci, Derek Bronish, Wayne D. Heym, Jason Kirschenbaum and
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
* Workshop on Theories (David Naumann and Peter O'Hearn)
* Workshop on Tools (Daniel Kroening and Tiziana Margaria)
* Workshop on Experiments (Rajeev Joshi and Joe Kiniry)
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
Tony Hoare, Jay Misra
This archive was generated by a fusion of
Pipermail (Mailman edition) and