Mailing list for all users of the OCaml language and system.
 help / color / mirror / Atom feed
From: Sam Owre <owre@csl.sri.com>
To: Undisclosed recipients: ;
Subject: [Caml-list] VSTTE 2013 Call for Participation
Date: Tue, 23 Apr 2013 14:16:55 -0700	[thread overview]
Message-ID: <29931.1366751815@ubi> (raw)


                    CALL FOR PARTICIPATION
                  Fifth Working Conference on
            Verified Software: Theories, Tools, and Experiments
                          (VSTTE 2013)
                       May 17--19, 2013,
	         Menlo College, Atherton, California
  	        [https://sites.google.com/site/vstte2013/]

The Fifth IFIP Working Conference on Verified Software: Theories,
Tools, and Experiments follows a successful inaugural working
conference at Zurich in 2005 followed by conferences in Toronto
(2008), Edinburgh (2010), and Philadelphia (2012).  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.

Invited speakers:
  Alex Aiken (Stanford), Sandrine Blazy (Rennes),
  Nikhil Swamy (Microsoft), Andre Platzer (CMU)

Accepted papers:
  Daniel Jost and Alexander J. Summers.
    An automatic encoding of VeriFast Predicates into Implicit Dynamic Frames
  Philipp Ruemmer, Hossein Hojjat and Viktor Kuncak.
    Classifying and Solving Horn Clauses for Verification
  Tuan-Hung Pham and Michael Whalen.
    An Improved Unrolling-Based Decision Procedure for Algebraic Data Types
  Olivier Bouissou, Eric Goubault, Sylvie Putot, Jean Goubault-Larrecq and Assale Adje.
    Static Analysis of Programs with Imprecise Probabilistic Inputs
  Etienne Kneuss, Viktor Kuncak and Philippe Suter.
    Effect Analysis for Programs with Callbacks
  K. Rustan M. Leino and Nadia Polikarpova.
    Verified Calculations   
  Jean-Christophe Filliatre, Claude Marché, François Bobot, Andrei Paskevich and Guillaume Melquiond.
    Preserving User Proofs Across Specification Changes   
  Pamela Zave and Jennifer Rexford.
    Compositional Network Mobility
  Julian Tschannen, Carlo A. Furia, Martin Nordio and Bertrand Meyer.
    Program Checking With Less Hassle
  Nicolas Rosner, Carlos Gustavo Lopez Pombo, Nazareno Aguirre, Ali Jaoua, Ali Mili and Marcelo Frias.
    Parallel Bounded Verification of Alloy Models by TranScoping
  Stephan Falke, Florian Merz and Carsten Sinz.
    Extending the Theory of Arrays: memset, memcpy, and Beyond
  Sandrine Blazy, André Maroneze and David Pichardie.
    Formal Verification of Loop Bound Estimation for WCET Analysis
  Frédéric Besson, Pierre-Emmanuel Cornilleau and Thomas Jensen.
    Result Certification of Static Program Analysers with Automated Theorem Provers
  Anthony Narkawicz and Cesar Munoz.
    A Formally Verified Generic Branching Algorithm for Global Optimization
  Shilpi Goel and Warren Hunt.
    Automated Code Proofs on a Formal Model of the X86
  Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein.
    seL4: from General Purpose to a Proof of Information Flow Enforcement
  Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler and Wolfgang Reif.
    Verification of a Virtual Filesystem Switch
  Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan and Yu Liu.
    Verifying Chinese Train Control System Under a Combined Scenario by Theorem Proving

School/Workshops:
  The conference will be colocated with the Third Summer School on Formal
  Techniques, and is preceded by NFM 2013 at NASA Ames and followed by ICSE
  2013 at San Francisco.

Conference Chair: Natarajan Shankar, SRI International

Program Chairs: Ernie Cohen, Microsoft, Andrey Rybalchenko, TU Munich 

Program Committee: Josh Berdine, Ahmed Bouajjani, Marsha Chechik,
Jean-Christophe Filliatre, Silvio Ghilardi, Aarti Gupta, Arie Gurfinkel,
Andrew Ireland, Ranjit Jhala, Cliff Jones, Rajeev Joshi, Gerwin Klein,
Daniel Kroening, Gary Leavens, Xavier Leroy, Zhiming Liu, Pete
Manolios, Tiziana Margaria, David Monniaux, Peter Mueller, David
Naumann, Aditya Nori , Peter O'Hearn, Matthew Parkinson, Wolfgang
Paul, Andreas Podelski, Zhang Shao, Willem Visser, Thomas Wies, Jim
Woodcock, Kwangkeun Yi, Pamela Zave, Lenore Zuck

Publicity Chair: Sam Owre,  SRI International

Steering Committee: Tony Hoare, Andrew Ireland, Jay Misra, Natarajan
Shankar, Jim Woodcock

             reply	other threads:[~2013-04-23 21:18 UTC|newest]

Thread overview: 2+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2013-04-23 21:16 Sam Owre [this message]
2013-05-02  3:32 Sam Owre

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=29931.1366751815@ubi \
    --to=owre@csl.sri.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox