Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Announcement: Boogie Workshop affiliated to CADE 2011

  • Subject: [Frama-c-discuss] Announcement: Boogie Workshop affiliated to CADE 2011
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Tue, 01 Mar 2011 13:56:43 +0100
Please find below the announcement for the next Boogie workshop, 
affiliated to CADE 2011 Conference.

Let me emphasized the sentence: *The workshop is intended for topics 
related to any intermediate verification language, not just Boogie.*

- Claude

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |




Boogie 2011: First International Workshop on Intermediate Verification Languages
co-located with CADE-23, Wroc?aw, Poland, August 1st 2011
http://research.microsoft.com/~moskal/boogie2011/


An intermediate verification language (IVL), like Boogie or Why, is
used as a stepping stone between a source language and a reasoning
engine. IVLs promote modularization and sharing of infrastructure. For
example, the same IVL can have multiple source language front-ends and
multiple reasoning engine back-ends, forming a verification tool bus.
The goal of the Boogie Workshop is to advance theory and techniques
supporting IVLs, to bring together researchers working with IVLs, and
to promote sharing of infrastructure that they build.

The workshop is intended for topics related to any intermediate
verification language, not just Boogie.

We welcome submissions up to 12 pages in LLNCS format. The accepted
papers will be printed in informal proceedings distributed to the
participants of the workshop. With the exception of survey and history
papers, the papers should contain original work which has not been
submitted or accepted for publication elsewhere.

Make sure to visit workshop?s webpage, which will describe the
submission method in due time, and currently has a colorful flyer
(looks excellent printed on A0 paper!).

Topics

? IVL tools
? language features of an IVL (e.g., angelic choice, tressa)
? type systems for an IVL
? translation from a source language to an IVL
? property inference at the level of an IVL (e.g., predicate
abstraction, abstract interpretation, termination metric inference,
Houdini-style inference)
? IVL to IVL translations (e.g., optimizations, slicing, translation
between different IVLs)
? translation from an IVL to reasoning engine (SMT, ATP, HOL) input
? interaction with reasoning engines
? interpretation of reasoning engine output in terms of the source
language via an IVL
? symbolic execution for an IVL
? axiomatizations of useful theories (like sets, sequences, heaps, ...)
? user experience improvements (e.g., caching of verification results)
? novel uses of IVLs (e.g., refinement or symbol diff)
? experimental evaluations (e.g., comparing different logical encoding
or reasoning engines)

Dates

submissions: May 1st, 2011
notification: June 1st, 2011
final versions: July 1st, 2011
workshop: August 1st, 2011

Program committee

Tayfun Elmas, UC Berkeley
K. Rustan M. Leino, Microsoft Research (co-chair)
Claude March?, INRIA
Micha? Moskal, Microsoft Research (co-chair)
Shaz Qadeer, Microsoft Research
Jan Smans, KU Leuven
Alexander J. Summers, ETH Z?rich