VMCAI 2012 Program, January 22-24

13th International Conference on
Verification, Model Checking, and Abstract Interpretation



Location/Venue: http://www.cse.psu.edu/popl/12/

Registration: https://regmaster3.com/2012conf/POPL12/register.php

Early registration ends 24 December.

Note about the program: The afternoon keynote talks are in the same session as two talks afterwards, to maintain the same breaks as those of events taking place in parallel.

Sunday, 22 January 2012

09:00 Computer augmented program engineering Rajeev Alur
10:00 coffee break
10:30 Synthesizing Efficient Controllers Christian Von Essen and Barbara Jobstmann
11:00 Lazy Synthesis Bernd Finkbeiner and Swen Jacobs
11:30 Effective Synthesis of Asynchronous Systems from GR(1) Specifications Uri Klein, Nir Piterman and Amir Pnueli
12:00 Catered lunch at the hotel Soup, Salad, and Sandwich Wrap
13:30 Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data Ahmed Bouajjani
14:30 On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking Dmitry Bugaychenko
15:00 A general framework for probabilistic characterizing formulae Joshua Sack and Lijun Zhang
15:30 coffee break
16:00 Automatic Inference of Access Permissions Pietro Ferrara and Peter Müller
16:30 Synthesizing Protocols for Digital Contract Signing Krishnendu Chatterjee and Vishwanath Raman
17:00 Model Checking Secrecy in Reactive Systems Rayna Dimitrova, Bernd Finkbeiner, Mate Kovacs, Markus Rabe and Helmut Seidl
17:30 VMCAI Business Meeting

Monday, 23 January 2012

09:00 Teaching Semantics with a Proof Assistant: Teach Proofs, not Logic! Tobias Nipkow
10:00 coffee break
10:30 On the Termination of Integer Loops Amir Ben-Amram, Samir Genaim and Abu Naser Masud
11:00 Inferring Canonical Register Automata Falk Howar, Bernhard Steffen, Sofia Cassel and Bengt Jonsson
11:30 Verification of gap-order constraint abstractions of counter systems Laura Bozzelli and Sophie Pinchinat
12:00 Lunch on your own Check the Walnut and Chestnut streets north of the hotel
13:30 A Verified Modern SAT Solver Duckki Oe, Aaron Stump, Corey Oliver and Kevin Clancy
14:00 Decision Procedures for Region Logic Stan Rosenberg, Anindya Banerjee and David Naumann
14:30 Crowfoot: a verifier for higher order store programs Nathaniel Charlton, Ben Horsfall and Bernhard Reus
15:00 Automating induction with an SMT solver Rustan Leino
15:30 coffee break
16:30 Modeling Asynchronous Message Passing for C Programs Everett Morse, Eric Mercer and Jay Mccarthy
17:00 Symbolic Execution with Collective Loop Invariants Stephen F. Siegel and Timothy Zirkel
19:00-22:00 Reception at http://www.moshulu.com, a ship moored close by A 5-minute walk: exit south from the hotel, turn left onto Spruce Street, then right onto S Columbus Blvd, then left onto Lombard Circle

Reception address:

Penn's Landing
401 S. Columbus Blvd
Philadelphia, PA 19106
Tel : 215.923.2500
Fax : 215.829.1604

Tuesday, 24 January 2012

09:00 Software Verification with Liquid Types Ranjit Jhala
10:00 coffee break
10:30 Local Symmetry and Compositional Verification Kedar Namjoshi and Richard Trefler
11:00 Regression Verification for Multi-Threaded Programs Sagar Chaki, Arie Gurfinkel and Ofer Strichman
11:30 Ideal Abstractions for Well-Structured Transition Systems Damien Zufferey, Thomas Wies and Thomas Henzinger
12:00 Lunch on your own Check the Walnut and Chestnut streets north of the hotel
13:30 New Applications of Underapproximations in Static Analysis Alex Aiken
14:30 Whale: An Interpolation-based Algorithm for Inter-procedural Verification Aws Albarghouthi, Arie Gurfinkel and Marsha Chechik
15:00 Splitting via Interpolants Evren Ermis, Jochen Hoenicke and Andreas Podelski
15:30 coffee break
16:00 Alternating Control Flow Reconstruction Johannes Kinder and Dmitry Kravchenko
16:30 Donut Domains: Efficient Non-Convex Domains for Abstract Interpretation Khalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda and Aarti Gupta
17:00 Sound Non-Statistical Clustering of Static Analysis Alarms Woosuk Lee, Wonchan Lee and Kwangkeun Yi
17:30 Synchronizability for Verification of Asynchronously Communicating Systems Samik Basu, Tevfik Bultan and Meriem Ouederni