Proceedings:
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.
| 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 | |
| 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:
Moshulu Penn's Landing 401 S. Columbus Blvd Philadelphia, PA 19106 Tel : 215.923.2500 Fax : 215.829.1604 info@moshulu.comhttp://www.moshulu.com/site/aboutus.asp
| 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 |