Conference program: POPL 2010

Tuesday, January 19, 2010

Special session: 18:45-19:45
Session Chair: Lenore Zuck (U. of Illinois, USA)

  • Special VMCAI-POPL joint session in memory of Amir Pnueli

Wednesday, January 20, 2010

Registration: 8:00-...

  • Registration opens (it is also possible to register during the previous POPL-week events).

Invited talk: 9:00-10:00
Session Chair: Jens Palsberg (UCLA)

  • Reconfigurable Asynchronous Logic Automata. Neil Gershenfeld (MIT, USA)

Concurrency: 10:30-11:30
Session Chair: John Field (IBM T. J. Watson Research Center)

  • On the Verification Problem for Weak Memory Models.
    Mohamed Faouzi Atig (LIAFA, University Paris Diderot), Ahmed Bouajjani (LIAFA, University Paris Diderot), Sebastian Burckhardt (Microsoft Research), Madan Musuvathi (Microsoft Research)

  • Coarse-Grained Transactions.
    Eric Koskinen (University of Cambridge), Matthew Parkinson (University of Cambridge), Maurice Herlihy (Brown University)

  • Sequential Verification of Serializability.
    H. Attiya (Technion), G. Ramalingam (Microsoft Research India), N. Rinetzky (Queen Mary University of London)

Static Analysis I: 12:00-1:00
Session Chair: Tayssir Touili (CNRS-LIAFA)

  • Compositional May-Must Program Analysis: Unleashing the Power of Alternation.
    Patrice Godefroid (Microsoft Research Redmond), Aditya V. Nori (Microsoft Research India), Sriram K. Rajamani (Microsoft Research India), Sai Deep Tetali (Microsoft Research India)

  • Continuity Analysis of Programs.
    Authors: Swarat Chaudhuri (Pennsylvania State University), Sumit Gulwani (Microsoft Research), Roberto Lublinerman (Pennsylvania State University)

  • Program Analysis via Satisfiability Modulo Path Programs.
    William R. Harris (University of Wisconsin, Madison, WI), Sriram Sankaranarayanan (NEC Laboratories America, Princeton, NJ), Franjo Ivancic (NEC Laboratories America, Princeton, NJ), Aarti Gupta (NEC Laboratories America, Princeton, NJ)

Verified Compilers: 2:30-3:30
Session Chair: Sorin Lerner (UC San Diego)

  • A simple, verified validator for software pipelining.
    Jean-Baptiste Tristan (INRIA Paris-Rocquencourt), Xavier Leroy (INRIA Paris-Rocquencourt)

  • A Verified Compiler for an Impure Functional Language.
    Adam Chlipala (Harvard University)

  • Verified just-in-time compiler on x86.
    Magnus O. Myreen (University of Cambridge)

Type Inference: 4:00-5:00
Session Chair: Benjamin Pierce (University of Pennsylvania)

  • Dependent Types from Counterexamples.
    Tachio Terauchi (Tohoku University)

  • Low-Level Liquid Types.
    Patrick Rondon (UC San Diego), Ranjit Jhala (UC San Diego), Ming Kawaguchi (UC San Diego)

  • Type Inference for Datalog with Complex Type Hierarchies.
    Max Schaefer (Semmle Ltd., Oxford), Oege de Moor (Semmle Ltd., Oxford)

POPL Community Meeting: 5:15-6:30

  • Most Influential Paper award (Philip Wadler).

  • Chair reports (Jens Palsberg and Manuel Hermenegildo).

  • Announcement of POPL 2011 (Tom Ball and Mooly Sagiv).

  • Discussion of the POPL review process (Philip Wadler).

  • Some words from NSF (Lenore Zuck).

Reception: 8:00-10:30
  • POPL 2010 Reception (at the Prado Museum, check registration packages for details).

Thursday, January 21, 2010

Invited talk: 9:00-10:00
Session Chair: Jens Palsberg (UCLA)

  • From Boolean to Quantitative Notions of Correctness.
    Thomas A. Henzinger (IST, Austria)

Reasoning about Programs: 10:30-11:30
Session Chair: Roberto Giacobazzi (Universita' degli Studi di Verona)

  • Nominal System T.
    Andrew M. Pitts (University of Cambridge)

  • A Theory of Indirection via Approximation.
    Aquinas Hobor (National University of Singapore), Robert Dockins (Princeton University), Andrew W. Appel (Princeton University)

  • A Relational Modal Logic for Higher-Order Stateful ADTs.
    Derek Dreyer (MPI-SWS), Georg Neis (MPI-SWS), Andreas Rossberg (MPI-SWS), Lars Birkedal (ITU-Copenhagen)

Static Analysis II: 12:00-1:00
Session Chair: Andrey Rybalchenko (Max Planck Institute for Software Systems)

  • Decision Procedures for Algebraic Data Types with Abstractions.
    Philippe Suter (EPFL), Mirco Dotta (EPFL), Viktor Kuncak (EPFL)

  • Automatic Numeric Abstractions for Heap-Manipulating Programs.
    Stephen Magill (Carnegie Mellon University), Ming-Hsien Tsai (National Taiwan University), Peter Lee (Carnegie Mellon University), Yih-Kuen Tsay (National Taiwan University)

  • Static Determination of Quantitative Resource Usage for Higher-Order Programs.
    Steffen Jost (University of St Andrews), Hans-Wolfgang Loidl (University of St Andrews), Kevin Hammond (University of St Andrews), Martin Hofmann (Ludwig-Maximilians University, Munich)

Verification:2:30-3:30
Session Chair: Xavier Leroy (INRIA Rocquencourt)

  • Toward a Verified Relational Database Management System.
    Ryan Wisnesky (Harvard University), Gregory Malecha (Harvard University), Avraham Shinnar (Harvard University), Greg Morrisett (Harvard University)

  • Counterexample-Guided Focus.
    Andreas Podelski (University of Freiburg), Thomas Wies (EPFL)

  • Structuring the verification of heap-manipulating programs.
    Aleksandar Nanevski (IMDEA Software, Madrid), Viktor Vefeiadis (Microsoft Research, Cambridge), Josh Berdine (Microsoft Research, Cambridge)

Types: 4:00-5:00
Session Chair: Erik Ernst (Aarhus University)

  • Dependent types and program equivalence.
    Limin Jia (University of Pennsylvania), Jianzhou Zhao (University of Pennsylvania), Vilhelm Sjoberg (University of Pennsylvania), Stephanie Weirich (University of Pennsylvania)

  • Pure Subtype Systems.
    DeLesley Hutchins (MZA Associates Corporation)

  • Modular Session Types for Distributed Object-Oriented Programming.
    Simon J Gay (University of Glasgow, UK), Vasco T Vasconcelos (University of Lisbon, Portugal), Antonio Ravara (Instituto de Telecomunicacoes and Technical University of Lisbon, Portugal), Nils Gesbert (University of Glasgow, UK), Alexandre Z Caldeira (University of Lisbon, Portugal)

Friday, January 22, 2010

Program Synthesis: 9:00-10:00
Session Chair: Cristiano Calcagno (Imperial College, London)

  • From Program Verification to Program Synthesis.
    Saurabh Srivastava (University of Maryland, College Park), Sumit Gulwani (Microsoft Research, Redmond), Jeffrey S. Foster (University of Maryland, College Park)

  • Abstraction-Guided Synthesis of Synchronization.
    Martin Vechev (IBM Research), Eran Yahav (IBM Research), Greta Yorsh (IBM Research)

  • Programming with Angelic Non-determinism.
    Shaon Barman (UC Berkeley), Rastislav Bodik (UC Berkeley), Satish Chandra (IBM TJ Watson Research), Joel Galenson (UC Berkeley), Doug Kimelman (IBM TJ Watson Research), Casey Rodarmor (UC Berkeley), Nicholas Tung (UC Berkeley)

Relating and Integrating Static and Dynamic Checks: 10:30-11:30
Session Chair: Matthias Felleisen (Northeastern University)

  • Contracts Made Manifest.
    Michael Greenberg (University of Pennsylvania), Benjamin Pierce (University of Pennsylvania), Stephanie Weirich (University of Pennsylvania)

  • Threesomes, With and Without Blame.
    Jeremy G. Siek (University of Colorado at Boulder), Philip Wadler (University of Edinburgh)

  • Integrating Typed and Untyped Code in a Scripting Language.
    Tobias Wrigstad (Purdue University), Francesco Zappa Nardelli (INRIA), Sylvain Lebresne (Purdue University), Johan Ostlund (Purdue University), Jan Vitek (Purdue University)

Compilers: 12:00-1:00
Session Chair: Peter Sewell (University of Cambridge)

  • Generating Compiler Optimizations from Proofs.
    Ross Tate (UC San Diego), Michael Stepp (UC San Diego), Sorin Lerner (UC San Diego)

  • Automatically Generating Instruction Selectors Using Declarative Machine Descriptions.
    Joao Dias (Tufts University), Norman Ramsey (Tufts University)

  • Semantics and Algorithms for Data-dependent Grammars.
    Yitzhak Mandelbaum (AT&T Labs - Research), Trevor Jim (AT&T Labs - Research), David Walker (Princeton University)

Security and Ownership: 2:30-3:30
Session Chair: Mads Dam (Royal Institute of Technology, Stockholm)

  • Paralocks : Role-Based Information Flow Control and Beyond.
    Niklas Broberg (Gothenburg University), David Sands (Chalmers University of Technology)

  • Modular Verification of Security Protocol Code by Typing.
    Karthikeyan Bhargavan (Microsoft Research), Cedric Fournet (Microsoft Research), Andrew D. Gordon (Microsoft Research)

  • Dynamically Checking Ownership Policies in Concurrent C/C++ Programs.
    Jean-Phillipe Martin (Microsoft Research Cambridge), Michael Hicks (University of Maryland, College Park), Manuel Costa (Microsoft Research Cambridge), Periklis Akritidis (University of Cambridge), Miguel Castro (Microsoft Research Cambridge)

Medley: 4:00-5:00
Session Chair: Mooly Sagiv (Tel-Aviv University)

  • Nested Interpolants.
    Matthias Heizmann (University of Freiburg, Germany), Jochen Hoenicke (University of Freiburg, Germany), Andreas Podelski (University of Freiburg, Germany)

  • Monads in Action.
    Andrzej Filinski (University of Copenhagen)

  • Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification.
    Naoki Kobayashi (Tohoku University), Naoshi Tabuchi (Tohoku University), Hiroshi Unno (Tohoku University)