38. POPL 2011: Austin, TX, USA

Invited talk

• Xavier Leroy:
  Verified squared: does critical software deserve verified tools? 1-2
  

Point analyis

• Ondrej Lhoták, Kwok-Chiang Andrew Chung:
  Points-to analysis with efficient strong updates. 3-16
  
• Yannis Smaragdakis, Martin Bravenboer, Ondrej Lhoták:
  Pick your contexts well: understanding object-sensitivity. 17-30
  
• Percy Liang, Omer Tripp, Mayur Naik:
  Learning minimal abstractions. 31-42
  

Semi-automated verification

• Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell:
  Relaxed-memory concurrency and verified compilation. 43-54
  
• Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber:
  Mathematizing C++ concurrency. 55-66
  
• Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy:
  Formal verification of object layout for c++ multiple inheritance. 67-80
  

Static analysis

• Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto Tatsuta:
  Static analysis of multi-staged programs via unstaging translation. 81-92
  
• Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Peter Lammich, Markus Müller-Olm:
  Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. 93-104
  
• Patrick Cousot, Radhia Cousot, Francesco Logozzo:
  A parametric segmentation functor for fully automatic and scalable array content analysis. 105-118
  

Semantic models and translations

• Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, Hongseok Yang:
  Step-indexed kripke models over recursive worlds. 119-132
  
• Chung-Kil Hur, Derek Dreyer:
  A kripke logical relation between ML and assembly. 133-146
  
• François Pottier:
  A typed store-passing translation for general references. 147-158
  

Shape analysis

• Dimitrios Prountzos, Roman Manevich, Keshav Pingali, Kathryn S. McKinley:
  A shape analysis for optimizing parallel graph programs. 159-172
  
• Xavier Rival, Bor-Yuh Evan Chang:
  Calling context abstraction with shapes. 173-186
  
• Isil Dillig, Thomas Dillig, Alex Aiken:
  Precise reasoning for programs using containers. 187-200
  

Type abstractions

• Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, Philip Wadler:
  Blame for all. 201-214
  
• Christos Dimoulas, Robert Bruce Findler, Cormac Flanagan, Matthias Felleisen:
  Correct blame for contracts: no more scapegoating. 215-226
  
• Stephanie Weirich, Dimitrios Vytiniotis, Simon L. Peyton Jones, Steve Zdancewic:
  Generative type abstraction and type-level computation. 227-240
  

Invited talk

• Matthew MacLaurin:
  The design of kodu: a tiny visual programming language for children on the Xbox 360. 241-246
  

Separation logic

• Aaron Joseph Turon, Mitchell Wand:
  A separation logic for refining concurrent objects. 247-258
  
• Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson:
  Modular reasoning for deterministic parallelism. 259-270
  
• Bart Jacobs, Frank Piessens:
  Expressive modular fine-grained concurrency specification. 271-282
  

Automata

• P. Madhusudan, Gennaro Parlato:
  The tree width of auxiliary storage. 283-294
  
• Nikos Tzevelekos:
  Fresh-register automata. 295-306
  
• Jérôme Leroux:
  Vector addition system reachability problem: a short self-contained proof. 307-316
  

Synthesis

• Sumit Gulwani:
  Automating string processing in spreadsheets using input-output examples. 317-330
  
• Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko:
  Predicate abstraction and refinement for verifying multi-threaded programs. 331-344
  
• Dan R. Ghica, Alex Smith:
  Geometry of synthesis III: resource management through type inference. 345-356
  

Algebra

• Jan Hoffmann, Klaus Aehlig, Martin Hofmann:
  Multivariate amortized resource analysis. 357-370
  
• Martin Hofmann, Benjamin C. Pierce, Daniel Wagner:
  Symmetric lenses. 371-384
  
• Fritz Henglein, Lasse Nielsen:
  Regular expression containment: coinductive axiomatization and computational interpretation. 385-398
  

Model checking

• Byron Cook, Eric Koskinen:
  Making prophecies with decision predicates. 399-410
  
• Michael Emmi, Shaz Qadeer, Zvonimir Rakamaric:
  Delay-bounded scheduling. 411-422
  
• Nishant Sinha, Chao Wang:
  On interference abstractions. 423-434
  

Types

• Pierre-Malo Deniélou, Nobuko Yoshida:
  Dynamic multirole session types. 435-446
  
• Jesse A. Tov, Riccardo Pucella:
  Practical affine types. 447-458
  
• Jong-hoon (David) An, Avik Chaudhuri, Jeffrey S. Foster, Michael Hicks:
  Dynamic inference of static types for ruby. 459-472
  

Invited talk

• Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell:
  Robin Milner 1934--2010: verification, languages, and concurrency. 473-474
  

Complexity

• Anna Bendersky, Erez Petrank:
  Space overhead bounds for dynamic memory management with partial compaction. 475-486
  
• Hagit Attiya, Rachid Guerraoui, Danny Hendler, Petr Kuznetsov, Maged M. Michael, Martin T. Vechev:
  Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated. 487-498
  
• Javier Esparza, Pierre Ganty:
  Complexity of pattern-based verification for multithreaded programs. 499-510
  

Medley

• Tarun Prabhu, Shreyas Ramalingam, Matthew Might, Mary W. Hall:
  EigenCFA: accelerating flow analysis with GPUs. 511-522
  
• Yuan Feng, Runyao Duan, Mingsheng Ying:
  Bisimulation for quantum processes. 523-534
  
• Robert L. Bocchino Jr., Stephen Heumann, Nima Honarmand, Sarita V. Adve, Vikram S. Adve, Adam Welc, Tatiana Shpeisman:
  Safe nondeterminism in a deterministic-by-default parallel language. 535-548
  

Compilation

• Louis-Noël Pouchet, Uday Bondhugula, Cédric Bastoul, Albert Cohen, J. Ramanujam, P. Sadayappan, Nicolas Vasilache:
  Loop transformations: convexity, pruning and optimization. 549-562
  
• Shu-yu Guo, Jens Palsberg:
  The essence of compiling with traces. 563-574
  
• Norman Ramsey, João Dias:
  Resourceable, retargetable, modular instruction selection using a machine-independent, type-based tiling of low-level intermediate code. 575-586
  

Verification

• C.-H. Luke Ong, Steven James Ramsay:
  Verifying higher-order functional programs with pattern-matching algebraic data types. 587-598
  
• Rajeev Alur, Pavol Cerný:
  Streaming transducers for algorithmic verification of single-pass list-processing programs. 599-610
  
• P. Madhusudan, Gennaro Parlato, Xiaokang Qiu:
  Decidable logics combining heap structures and data. 611-622
  

8.1 + 8.2

• Pramod G. Joisha, Robert S. Schreiber, Prithviraj Banerjee, Hans-Juergen Boehm, Dhruva R. Chakrabarti:
  A technique for the effective and automatic reuse of classical compiler optimizations on multithreaded code. 623-636
  

Last update Tue May 21 17:52:09 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page