From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 44CD1BBAF for ; Mon, 14 Dec 2009 13:29:16 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqYAAJe+JUuKZAhMkWdsb2JhbACEBpc0AQEBAQkLCgcTBa1UjCOEKwSBYg X-IronPort-AV: E=Sophos;i="4.47,395,1257116400"; d="scan'208";a="39840027" Received: from relay.fi.upm.es (HELO relay3.fi.upm.es) ([138.100.8.76]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 14 Dec 2009 13:29:15 +0100 Received: from localhost (localhost.localdomain [127.0.0.1]) by relay3.fi.upm.es (Postfix) with ESMTP id 856C8ACDA60 for ; Mon, 14 Dec 2009 13:29:15 +0100 (CET) X-Virus-Scanned: by amavisd-new using ClamAV at efiltro.fi.upm.es Received: from clip.dia.fi.upm.es (clip.dia.fi.upm.es [138.100.11.74]) (using TLSv1 with cipher AES256-SHA (256/256 bits)) (No client certificate requested) by relay3.fi.upm.es (Postfix) with ESMTP id 66C09ACDA4A for ; Mon, 14 Dec 2009 13:29:15 +0100 (CET) Received: from herme by clip.dia.fi.upm.es with local-rmail (Exim 4.69) (envelope-from ) id 1NJzcz-0004AM-CM for caml-list@inria.fr; Mon, 14 Dec 2009 02:21:33 +0100 X-Mailer: emacs 22.2.1 (via feedmail 11-beta-1 Q); VM 7.19 under Emacs 22.3.1 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <19237.37539.366300.240322@gazelle.local> Date: Mon, 14 Dec 2009 02:19:31 +0100 Reply-To: Manuel Hermenegildo From: vmcai10-announce@clip.dia.fi.upm.es To: caml-list@inria.fr Subject: VMCAI 2010 - Call for Participation - Early Reg: Dec 22 X-SA-Exim-Connect-IP: X-SA-Exim-Mail-From: herme@clip.dia.fi.upm.es X-SA-Exim-Scanned: No (on clip.dia.fi.upm.es); SAEximRunCond expanded to false X-Spam: no; 0.00; redistribute:01 model:01 co-located:01 popl:01 model:01 rustan:01 leino:01 saarland:01 giacobazzi:01 pieter:01 katoen:01 aachen:01 popl:01 saarland:01 reachability:01 ---------------------------------------------------------------------- *** CALL FOR PARTICIPATION *** [ Please redistribute. Apologies for multiple postings. ] VMCAI 2010 The Eleventh International Conference on Verification, Model Checking, and Abstract Interpretation Madrid, Spain, January 17-19, 2010 (Co-located with POPL 2010) http://software.imdea.org/events/vmcai10/ Early registration deadline: December 22, 2009 Hotel registration deadline: December 28, 2009 ---------------------------------------------------------------------- VMCAI provides a forum for researchers from the communities of Verification, Model Checking, and Abstract Interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods. The program of VMCAI'10 will consist of invited lectures, invited tutorials, and 21 contributed talks. The full programme is available at the conference web site. * Invited Talks: Javier Esparza (Technical University of Munich): Analysis of Systems with Stochastic Process Creation Rustan Leino (Microsoft Research): Verifying Concurrent Programs with Chalice Reinhard Wilhelm (Saarland University): Static Timing Analysis for Hard Real-Time Systems * Invited Tutorials: Roberto Giacobazzi (University of Verona): Abstract Interpretation-based Protection Joost Pieter Katoen (Aachen University): Advances in Probabilistic Model Checking Viktor Kuncak (EPFL Lausanne): Building a Calculus of Data Structures * Registration: Further information on registration for VMCAI is available at the conference web site: http://software.imdea.org/events/vmcai10/ Further information on accommodation is available at the POPL web site: http://www.cse.psu.edu/popl/10/ * Program: Sunday, January 17, 2010 9:00-10:00 Invited Talk * Reinhardt Wilhelm (Saarland University) Static Timing Analysis for Hard Real-Time Systems Coffee break 10:30-11:30 Automata and Monitors * RoLei Bu, Jianhua Zhao and Xuandong Li. Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming * Meera Sridhar and Kevin Hamlen. Model-Checking In-lined Reference Monitors Coffee break 12.00-13.30 Abstract interpretation * Liqian Chen, Antoine Mine, Ji Wang and Patrick Cousot. An abstract domain for discovering interval linear equalities * Valentin Perrelle and Nicolas Halbwachs. An analysis of permutations in arrays * Andy King and Harald Sondergaard. Automatic Abstraction for Congruences Lunch break 15.30-16.30 Model Checking * Jori Dubrovin. Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing * Benjamin Aminof, Orna Kupferman and Aniello Murano. Improved Model Checking of Hierarchical Systems Coffee break 17:00-18.30 Invited Tutorial * Roberto Giaccobazzi (University of Verona) Abstract Interpretation-based Protection Monday, January 18, 2010 9.00-10.00 Invited Talk * Rustan Leino (Microsoft Research) Verifying Concurrent Programs with Chalice Coffee break 10.30-11:30 Logical Methods * Vijay D'silva, Daniel Kroening, Mitra Purandare and Georg Weissenbacher. Interpolant Strength * Kuat Yessenov, Ruzica Piskac and Viktor Kuncak. Collections, Cardinalities, and Relations Coffee break 12.00-13.30 Program Verification * Alexander Summers and Sophia Drossopoulou. A Considerate Specification of the Composite Pattern * Thomas Henzinger, Thibaud B. Hottelier, Laura Kovacs and Andrei Voronkov. Invariant and Type Inference for Matrices * Yungbum Jung, Soonho Kong, Bow-Yaw Wang and Kwangkeun Yi. Deriving Invariants in Propositional Logic by Algorithmic Learning, Decision Procedure, and Predicate Abstraction Lunch break 15.30-16.30 Quantitative Analysis * Bjorn Wachter and Lijun Zhang. Best Probabilistic Transformers * Rohit Chadha, Axel Legay, Pavithra Prabhakar and Mahesh Viswanathan. Complexity bounds for the verification of real-time software Coffee break 17:00-18.30 Invited Tutorial * Joost Pieter Katoen (University of Twente) Advances in Probabilistic Model Checking Tuesday, January 19, 2010 9.00-10.00 Invited Talk * Javier Esparza (Technical University of Munich) Analysis of Systems with Stochastic Process Creation Coffee break 10.30-11:30 Temporal Logic * Rajeev Alur and Swarat Chaudhuri. Temporal Reasoning for Procedural Programs * Cesar Sanchez and Martin Leucker. Regular Linear Temporal Logic with Past Coffee break 12.00-13.30 Shape Analysis * Matthew Might. Shape Analysis of Higher-Order Programs via Abstract Interpretation * Mark Marron, Rupak Majumdar, Darko Stefanovic and Deepak Kapur. Shape Analysis with Reference Set Relations * Jorg Kreiker, Helmut Seidl and Vesal Vojdani. Shape Analysis of Low-level C with Overlapping Structures Lunch break 15.30-16.30 Concurrency * Viktor Vafeiadis. RGSep Action Inference * Alexander Malkis, Shaz Qadeer and Shuvendu Lahiri. Abstract Threads Coffee break 17:00-18.30 Invited Tutorial * Viktor Kuncak (EPF Lausanne) Building a Calculus of Data Structures ----------------------------------------------------------------------