Session chair: David Rosenblum
Mark Harman (KCL)
Title: Why the Virtual Nature of Software Makes it Ideal for Search Based Optimization
Session chair: Andrew D. Gordon
- Formal Verification of Coalescing Graph-Coloring Register Allocation
Sandrine Blazy (IRISA - Universit{\'e} Rennes 1),
Beno{\^\i}t Robillard (CEDRIC-CNAM) and
Andrew W. Appel (Princeton University)
- Deadlock-free Channels and Locks
K. Rustan M. Leino (Microsoft Research)
Peter M\"uller (ETH Zurich)
Jan Smans (Katholieke Universiteit Leuven)
- TRX: A Formally Verified Parser Interpreter
Adam Koprowski (MLstate)
Henri Binsztok (MLstate)
FASE - Model Transformation
Session chair: Hartmut Ehrig
- A Formalisation of Constraint-Aware Model Transformations
Adrian Rutle, Bergen University College, Norway
Alessandro Rossini, University of Bergen, Norway
Yngve Lamo, Bergen University College, Norway
Uwe Wolter, University of Bergen, Norway
- Real-Time Model Transformations in MOMENT2
Artur Boronat, University of Leicester, United Kingdom
Peter Olveczky, University of Oslo, Norway
- Reusing Model Transformations while Preserving Properties
Ethan Jackson, Wolfram Schulte, Microsoft Research, United States
Daniel Balasubramanian, Gabor Karsai, Vanderbilt University, United States
Session chair: Javier Esparza
- Assume-Guarantee Verification for Probabilistic Systems
Marta Kwiatkowska (University of Oxford),
Gethin Norman (University of Glasgow),
David Parker (University of Oxford),
Hongyang Qu (University of Oxford)
- Simple O(mlog n) Time Markov Chain Lumping
Antti Valmari (Tampere University of Technology),
Giuliana Franceschinis (University of East Piedmont)
- Model Checking Interactive Markov Chains
Lijun Zhang (Saarland University),
Martin R. Neuh¨außer (RWTH Aachen
University)
- Approximating the Pareto Front of Multi-Criteria Optimization Problems
Julien Legriel (Verimag),
Colas Le Guernic (Verimag),
Scott Cotton (Verimag),
Oded Maler (Verimag)
Session chair: David Naumann
- CFA2: a Context-Free Approach to Control-Flow Analysis
Dimitrios Vardoulakis (Northeastern University)
Olin Shivers (Northeastern University)
- Weighted Dynamic Pushdown Networks
Alexander Wenner (Westf{\"a}lische Wilhelms-Universit{\"a}t M{\"u}nster)
- Propositional Interpolation and Abstract Interpolation
Vijay D'Silva (Computing Laboratory, Oxford University)
- Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
Assal{\'e} Adj{\'e} (CEA, LIST, and LIX, {\'E}cole Polytechnique (MeASI))
St{\'e}phane Gaubert (INRIA Saclay and CMAP, {\'E}cole Polytechnique)
Eric Goubault (CEA, LIST (MeASI))
Session chair: Vittorio Cortellessa
- Are Popular Classes More Defect Prone?
Alberto Bacchelli, Marco D'Ambros and
Michele Lanza.
University of Lugano, Switzerland
- Operation-based, Fine-grained Version Control Model for Tree-based Representation
Tung Nguyen, Hoan Nguyen, Nam Pham and Tien Nguyen.
Iowa State University, United States
- A Method for Analyzing Code Homology in Genealogy of Evolving Software
Masatomo Hashimoto, AIST, Japan,
Akira Mori, The National Institute of Advanced Industrial Science and Technology, Japan
- Dynamic Resource Scheduling in Disruption-Prone Software Development Environments
Junchao Xiao, Chinese Academy of Sciences, China
Leon Osterweil, UMass Amherst, United States
Qing Wang and Mingshu Li, Chinese Academy of Sciences, China
Session chair: Daniel Kroening
- An Alternative to SAT-based Approaches for Bit-Vectors
Sebastien Bardin (CEA Saclay),
Philippe Herrmann (CEA Saclay),
Florian Perroud (CEA Saclay)
- Satisfiability Modulo the Theory of Costs: Foundations and Applications
Alessandro Cimatti (FBK-IRST),
Anders Franz´en (FBK-IRST and University of Trento),
Alberto Griggio (University of Trento),
Roberto Sebastiani (University of Trento),
Cristian Stenico (University of Trento)
- Optimal Tableau Algorithms for Coalgebraic Logics
Rajeev Gor´e (Australian National University),
Clemens Kupke (Imperial College),
Dirk Pattinson (Imperial College)
- Blocked Clause Elimination
Matti J¨arvisalo (University of Helsinki),
Armin Biere (Johannes Kepler
University),
Marijn Heule (Technical University of Delft)
Session chair: Naoki Kobayashi
- A Theory of Speculative Computation
G{\'e}rard Boudol (INRIA - Sophia Antipolis)
Gustavo Petri (INRIA - Sophia Antipolis)
- Parameterized Memory Models and Concurrent Separation Logic
Rodrigo Ferreira (Yale University)
Xinyu Feng (Toyota Technological Institute at Chicago)
Zhong Shao (Yale University)
- Generative Operational Semantics for Relaxed Memory Models
Radha Jagadeesan (DePaul University)
Corin Pitcher (DePaul University)
James Riely (DePaul University)
Session chair: Gabriele Taentzer
- Incremental Service Composition based on Partial Matching of Visual Contracts
Muhammad Naeem, Reiko Heckel, University of Leicester, United Kingdom
Fernando Orejas, UPC, Spain,
Frank Hermann, Technische Universit\"at Berlin, Germany
- Formal Analysis and Verification of Self-Healing Systems
Claudia Ermel, Hartmut Ehrig, Olga Runge, Technische Universit\"at Berlin, Germany
Antonio Bucchiarone, FBK-IRST, Italy
Patrizio Pelliccione, Universit\'a dell'Aquila, Italy
- Stochastic Simulation of Graph Transformation Systems (TOOL DEMO)
Paolo Torrini, Reiko Heckel, University of Leicester, United Kingdom
Istvan Rath, Budapest University of Technology and Economics, Hungary
Session chair: Antti Valmari
- Boom: Taking Boolean Program Model Checking One Step Further
Gerard Basler (ETH Z¨urich),
Matthew Hague (University of Oxford),
Daniel Kroening (University of Oxford),
Luke Ong (University of Oxford),
Thomas Wahl (University of Oxford),
Haoxian Zhao (University of Oxford)
- The OpenSMT Solver
Roberto Bruttomesso (University of Lugano),
Edgar Pek (University of
Lugano),
Natasha Sharygina (University of Lugano),
Aliaksei Tsitovich
(University of Lugano)
- Stranger: An Automata-based String Analysis Tool for PHP
Fang Yu (University of California at Santa Barbara),
Muath Alkhalaf (University of California at Santa Barbara),
Tevfik Bultan (University
of California at Santa Barbara)
David Naumann (Stevens Institute of Technology)
Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions
Session Chair: Andy Gordon
Session chair: Beppe Castagna
- Explicit Stabilisation for Modular Rely-Guarantee Reasoning
John Wickerson (University of Cambridge)
Mike Dodds (University of Cambridge)
Matthew Parkinson (University of Cambridge)
- Fluid Updates: Beyond Strong vs. Weak Updates
Isil Dillig (Stanford University)
Thomas Dillig (Stanford University)
Alex Aiken (Stanford University)
- A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While
Keiko Nakata (Institute of Cybernetics, Tallinn University of Technology)
Tarmo Uustalu (Institute of Cybernetics, Tallinn University of Technology)
- Faulty Logic: Reasoning about Fault Tolerant Programs
Matthew L. Meola (Princeton University)
David Walker (Princeton University)
Session chair: Marsha Chechik
- Prescriptive Semantics for Big-Step Modelling Languages
Shahram Esmaeilsabzali and Nancy Day, University of Waterloo, Canada
- A Modular Model Composition Technique
Pierre Kelsen and Qin Ma, University of Luxembourg, Luxembourg
- A Verifiable Modeling Approach to Configurable Role-Based Access Control
Dae-Kyoo Kim, Lunjin Lu and Sangsig Kim.
Oakland University, United States
- Incremental Consistency Checking of Dynamic Constraints
Iris Groher, University of Linz, Austria
Alexander Reder and Alexander Egyed, Johannes Kepler University, Austria
Session chair: Javier Esparza
- When Simulation Meets Antichains (On Checking Language Inclusion
of Nondeterministic Finite (Tree) Automata)
Parosh Abdulla (University of Uppsala),
Yu-Fang Chen (University of Uppsala),
Luk´aˇs Hol´ık (Brno University of Technology),
Richard Mayr (University of Edinburgh),
Tom´aˇs Vojnar (Brno University of Technology)
- On Weak Modal Compatibility, Refinement, and the MIO Workbench
Sebastian S. Bauer (LMU Munich),
Philip Mayer (LMU Munich),
Andreas Schroeder (LMU Munich),
Rolf Hennicker (LMU Munich)
- Rational Synthesis
Dana Fisman (Hebrew University and IBM Haifa),
Orna Kupferman (Hebrew University),
Yoad Lustig (Rice University)
- Efficient Buechi Universality Checking
Seth Fogarty (Rice University),
Moshe Y. Vardi (Rice University)
Session chair: Anna Philippou
- Logical Concurrency Control From Sequential Proofs
Jyotirmoy Deshmukh (University of Texas at Austin)
G. Ramalingam (Microsoft Research)
Venkatesh-Prasad Ranganath (Microsoft Research)
Kapil Vaswani (Microsoft Research)
- On the expressive power of primitives for compensation handling
Ivan Lanese (Lab. Focus, University of Bologna/INRIA)
C{\'a}tia Vaz (INESC-ID/ISEL, Polytechnical Institute of Lisbon)
Carla Ferreira (CITI / Departamento de Inform{\'a}tica, FCT Universidade Nova de Lisboa)
- Verifying a Compiler for Java Threads
Andreas Lochbihler (Karlsruher Institut f\"ur Technologie (KIT))
- Stateful Contracts for Affine Types
Jesse A. Tov (Northeastern University)
Riccardo Pucella (Northeastern University)
Session chair: Fernando Orejas
- Proving Consistency and Completeness of Model Classes Using Theory Interpretation
Adam Darvas and Peter M\"uller, ETH Zurich, Switzerland
- Automatic Cross Validation of Multiple Specifications: A Case Study
Carlo Ghezzi and Andrea Mocci, Politecnico di Milano, Italy
- An Automata-Theoretic Approach to Hardware/Software Co-verification
Juncao Li, Fei Xie, Portland State University, United States
Thomas Ball, Microsoft Research, United States
Vladimir Levin and Con McGarvey, Microsoft Corporation, United States
Session chair: Luke Ong
- Automated Termination Analysis for Programs with Second-Order
Recursion
Markus Aderhold (Technical University of Darmstadt)
- Ranking Function Synthesis for Bit-Vector Relations
Byron Cook (Microsoft Research),
Daniel Kroening (University of Oxford),
Philipp R¨ummer (University of Oxford),
Christoph M. Wintersteiger
(ETH Z¨urich)
- Fairness for Dynamic Control
Jochen Hoenicke (University of Freiburg),
Ernst-R¨udiger Olderog (University of Oldenburg),
Andreas Podelski (University of Freiburg)
Session chair: Philip Wadler
- Testing Polymorphic Properties
Jean-Philippe Bernardy (Chalmers University of Technology and University of Gothenburg)
Patrik Jansson (Chalmers University of Technology and University of Gothenburg)
Koen Claessen (Chalmers University of Technology)
- A Grammar-Based Approach to Invertible Programs
Kazutaka Matsuda (University of Tokyo)
Shin-Cheng Mu (Academia Sinica and University of Tokyo)
Zhenjiang Hu (NII)
Masato Takeichi (University of Tokyo)
- A Universal Calculus for Stream Processing Languages
Robert Soul{\'e} (New York University)
Martin Hirzel (IBM Research)
Robert Grimm (New York University)
Bu\u{g}ra Gedik (IBM Research)
Henrique Andrade (IBM Research)
Vibhore Kumar (IBM Research)
Kun-Lung Wu (IBM Research)
Session chair: Reiko Heckel
- Shape Refinement through Explicit Heap Analysis
Dirk Beyer, University of Passau, Germany
Thomas Henzinger, IST Austria, Austria,
Gr\΄egory Th\΄eoduloz, EPFL, Switzerland,
Damien Zufferey, IST Austria, Austria
- Memory Leaks Detection in Java by Bi-Abductive Inference
Dino Distefano and Ivana Filipovic, University of London, United Kingdom
- Analyzing the Impact of Change in Multi-threaded Programs
Krishnendu Chatterjee,
Luca de Alfaro,
Vishwanath Raman and
Cesar Sanchez,
Session chair: Rustan Leino
- JTorX: a Tool for On-Line Model-Driven Test Derivation and Execution
Axel Belinfante (University of Twente),
- SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems
Klaus Dr¨ager (Saarland University),
Andrey Kupriyanov (Saarland
University),
Bernd Finkbeiner (Saarland University),
Heike Wehrheim
(University of Paderborn)
- Tracking Heaps that Hop with Heap-Hop
Jules Villard (LSV, ENS Cachan),
´ Etienne Lozes (LSV, ENS Cachan),
Cristiano Calcagno (Monoidics Ltd and Imperial College)
Joseph Sifakis (Verimag)
Embedded Systems Design – Scientific Challenges and Work Directions
Session chair: Matteo Maffei
- Enforcing Stateful Authorization and Information Flow Policies in Fine
Nikhil Swamy (Microsoft Research)
Juan Chen (Microsoft Research)
Ravi Chugh (University of California, San Diego)
- A Semantic Framework for Declassification and Endorsement
Aslan Askarov (Cornell University)
Andrew Myers (Cornell University)
- Precise and Automated Contract-based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays
Torben Amtoft (Kansas State University)
John Hatcliff (Kansas State University)
Edwin Rodr{\'\i}guez (Kansas State University)
- Automating Security Mediation Placement
Dave King (Pennsylvania State University)
Susmit Jha (University of California, Berkeley)
Divya Muthukumaran (Pennsylvania State University)
Trent Jaeger (Pennsylvania State University)
Somesh Jha (University of Wisconsin)
Sanjit A. Seshia (University of California, Berkeley)
Session chair: David Rosenblum
- Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction Techniques
Steven Lauterburg, Rajesh Karmani, Darko Marinov and Gul Agha,
University of Illinois at Urbana-Champaign, United States
- A Lightweight and Portable Approach to Making Concurrent Failures Reproducible
Qingzhou Luo, Min Hu, Shanghai Jiao Tong University, China
Sai Zhang, Shanghai PRC, China,
Jianjun Zhao, Shanghai Jiao Tong University, China
- Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups
Hermann Lehner and Peter M\"uller, ETH Zurich, Switzerland
Session chair: Simona Ronchi della Rocca
- A Semantic Foundation for Hidden State
Jan Schwinghammer (Saarland University, Saarbr{\"u}cken), Hongseok
Yang (Queen Mary, University of London), Lars Birkedal (IT University
of Copenhagen),
Fran{\c c}ois Pottier (INRIA) and Bernhard Reus
(University of Sussex).
- Linearly-used continuations in the enriched effect
calculus
Jeff Egger (University of Edinburgh), Rasmus Ejlers M{\o}gelberg
(IT University of Copenhagen) and Alex Simpson (University of
Edinburgh).
- Block structure vs scope extrusion: between
innocence and omniscience
Andrzej Murawski (University of Oxford) and Nikos Tzevelekos
(University of Oxford).
- Completeness for algebraic
theories of local state
Sam Staton (University of Cambridge).
Session chair: Moshe Vardi
- Automatic Analysis of Scratch-pad Memory Code for Heterogeneous
Multicore Processors
Alastair Donaldson (University of Oxford),
Daniel Kroening (University
of Oxford),
Philipp R¨ummer (University of Oxford)
- Simplifying Linearizability Proofs with Reduction and Abstraction
Tayfun Elmas (Koc University),
Shaz Qadeer (Microsoft Research),
Ali Sezgin (Koc University),
Omer Subasi (Koc University),
Serdar Tasiran (Koc University)
- A Polymorphic Intermediate Verification Language: Design and Logical
Encoding
Rustan Leino (Microsoft Research),
Philipp R¨ummer (University of
Oxford)
- Trace-based Symbolic Analysis for Atomicity Violations
Chao Wang (NEC Labs),
Rhishikesh Limaye (University of California
at Berkeley),
Malay Ganai (NEC Labs), Aarti Gupta (NEC Labs)
Philip Wadler (University of Edinburgh)
The Audacity of Hope: Thoughts on Reclaiming the Database Dream
Session Chair: Vladimiro Sassone
Session chair: Dino Distefano
- Separating Shape Graphs
Vincent Laviron ({\'E}cole Normale Sup{\'e}rieure)
Bor-Yuh Evan Chang (University of Colorado, Boulder)
Xavier Rival (INRIA / {\'E}cole Normale Sup{\'e}rieure)
- Amortised Resource Analysis with Separation Logic
Robert Atkey (University of Edinburgh)
Session chair: Maura Cerioli
- Performance modeling and analysis of context-aware mobile software systems
Luca Berardinelli, Vittorio Cortellessa and Antinisca Di Marco,
Universit\'a dell'Aquila, Italy
- A Process to Identify ``Guilty'' Antipatterns in Software Performance Analysis
Vittorio Cortellessa, Universit\'a dell'Aquila, Italy
Anne Martens, Ralf Reussner, Karlsruhe Institute of Technology, Germany,
Catia Trubiani, Universitΰ degli Studi di L'Aquila, Italy
Session chair: Javier Esparza
- Fair adversaries and randomization in
two-player games
Eugene Asarin (LIAFA), Rapha{\"e}l Chane-Yack-Fa (LIAFA and
PPS-CNRS, and University Paris Diderot) and Daniele Varacca (PPS-CNRS
and University Paris Diderot).
- Retaining the
Probabilities in Probabilistic Testing Theory
Sonja Georgievska (Technical University of Eindhoven) and Suzana
Andova (Technical University of Eindhoven).
Session chair: Lars Birkedal
- Amortized Resource Analysis with Polynomial Potential---A Static Inference of Polynomial Bounds for Functional Programs
Jan Hoffmann (LMU Munich)
Martin Hofmann (LMU Munich)
- Functional Programming in Sublinear Space
Ugo Dal Lago (Universit{\`a} di Bologna)
Ulrich Sch{\"o}pp (LMU Munich)
- A PolyTime Functional Language from Light Linear Logic
Patrick Baillot (CNRS and ENS Lyon)
Marco Gaboardi (Dip. Informatica - Universita` di TORINO)
Virgile Mogbil (LIPN - CNRS/Universit{\'e} Paris 13)
Session chair: Doron Peled
- ACS: Automatic Converter Synthesis for SoC bus protocols
Karin Avnit (University of New South Wales),
Arcot Sowmya (University
of New South Wales),
Jorgen Peddersen (University of New South
Wales)
- AlPiNA: An Algebraic Petri Net Analyzer
Didier Buchs (University of Geneva),
Steve Hostettler (University of
Geneva),
Alexis Marechal (University of Geneva),
Matteo Risoldi (University
of Geneva)
- PASS: Abstraction Refinement for Infinite Probabilistic Models
Ernst Moritz Hahn (Saarland University),
Holger Hermanns (Saarland
University),
Bj¨orn Wachter (Saarland University),
Lijun Zhang
(Saarland University)
Jean-Fran¸cois Raskin (Free University of Brussels)
Antichain Algorithms for Finite Automata
Session chair: Jens Knoop, the Vienna University of Technology, Austria
Session chair: Rupak Majumdar
- "Mining Opportunities for Code Improvement in a Just-In-Time Compiler"
Adam Jocksch, University of Alberta, Canada
Marcel Mitran, IBM Toronto Software Laboratory, Canada
Joran Siu, IBM Toronto Software Laboratory, Canada
Nikola Grcevski, IBM Toronto Software Laboratory, Canada
Jose Nelson Amaral, University of Alberta, Canada
- "Unrestricted Code Motion: A Program Representation and Transformation Algorithms based on Future Values"
Shuhan Ding, Michigan Tech University, United States
Soner Onder, Michigan Tech University, United States
- "Optimizing MATLAB through Just-In-Time Specialization"
Maxime Chevalier-Boisvert, McGill University, Canada
Laurie Hendren, McGill University, Canada
Clark Verbrugge, McGill University, Canada
- "RATA: Rapid Atomic Types Analysis by Abstract Interpretation. Application to JavaScript optimization"
Francesco Logozzo, Microsoft Research, United States
Herman Venter, Microsoft Research, United States
Session chair: Kohei Honda
- Forward Analysis of Depth-Bounded
ProcessesThomas Henzinger (IST Austria), Thomas Wies (IST Austria) and
Damien Zufferey (IST Austria).
- Incremental
pattern-based coinduction for process algebra and its Isabelle formalization
Andrei Popescu (Uniersity of Illinois at Urbana-Champaign) and
Elsa Gunter (Uniersity of Illinois at Urbana-Champaign).
- Parameterised Multiparty Session Types
Malo Deni{\'e}lou (Imperial College, London), Nobuko Yoshida
(Imperial College, London), Andi Bejleri (Imperial College, London)
and Raymond Hu (Imperial College, London).
- On the relationship between spatial logics and behavioral simulations
Lucia Acciai (DSI: Universita' di Firenze), Michele Boreale
(Universita' di Firenze) and Gianluigi Zavattaro (University of
Bologna).
Session chair: Rupak Majumdar
- Arrival Curves for Real-Time Calculus: the Causality Problem and its
Solutions
Matthieu Moy (Verimag),
Karine Altisen (Verimag)
- Computing the Leakage of Information-Hiding Systems
Miguel E. Andr´es (Radboud University Nijmegen),
Catuscia Palamidessi
(INRIA and ´ Ecole Polytechnique),
Peter van Rossum (Radboud University
Nijmegen),
Geoffrey Smith (Florida International University)
- Statistical Measurement of Information Leakage
Konstantinos Chatzikokolakis (Eindhoven University of Technology),
Tom Chothia (University of Birmingham),
Apratim Guha (University
of Birmingham)
- SAT based Bounded Model Checking with Partial Order Semantics for
timed automata
Janusz Malinowski (University of Provence),
Peter Niebert (University
of Provence)
Session chair: Luke Ong
Colin Stirling.
"An Introduction to Decidability of Higher-Order Matching"
Session chair: Xipeng Shen, the College of William and Mary, USA
- JReq: Database Queries in Imperative Languages
Ming-Yee Iu, EPFL, Switzerland
Emmanuel Cecchet, UMass, United States
Willy Zwaenepoel, EPFL, Switzerland
- Verifying Local Transformations of Concurrent Programs
Sebastian Burckhardt, Microsoft Research, United States
Madanlal Musuvathi, Microsoft Research, United States
Vasu Singh, EPFL, Switzerland
Session chair: Jean-Francois Raskin
An easy completeness
proof for the modal mu-calculus on finite trees
Gaelle Fontaine (ILLC, University of Amsterdam) and Balder ten
Cate (University of California, Santa Cruz).
When Model-Checking Freeze LTL over Counter Machines Becomes
Decidable
St{\'e}phane Demri (CNRS) and Arnaud Sangnier (University of
Torino).
Session chair: Madan Musuvathi, Microsoft Research, USA
- Practical Extensions to the IFDS Algorithm
Nomair Naeem, University of Waterloo, Canada
Ondrej Lhotak, University of Waterloo, Canada
Jonathan Rodriguez, University of Waterloo, Canada
- Using Ownership to Reason about Inherent Parallelism in Object-Oriented Programs
Andrew Craik, Queensland University of Technology, Australia
Wayne Kelly, Queensland University of Technology, Australia
Session chair: Moshe Vardi
- Model Checking is Static
Analysis of Modal Logic
Flemming Nielson (Technical University of Denmark) and Hanne Riis
Nielson (Technical University of Denmark).
- Counting CTL
Fran{\c c}ois Laroussinie (LIAFA, University of Paris 7, CNRS),
Antoine Meyer (IGM, Universit{\'e} Paris Est - Marne-la-Vall{\'e}e)
and Eudes Petonnet (LIAFA, University of Paris 7, CNRS).
- Algorithmic metatheorems for decidable LTL
model checking over infinite systems
Anthony Widjaja To (University of Edinburgh) and Leonid Libkin
(University of Edinburgh).
Session chair: Tomas Vojnar
- Preemption Sealing for Efficient Concurrency Testing
Thomas Ball (Microsoft Research),
Sebastian Burckhardt (Microsoft
Research),
Katherine E. Coons (University of Texas at Austin),
Madanlal
Musuvathi (Microsoft Research),
Shaz Qadeer (Microsoft Research)
- Code Mutation in Verification and Automatic Code Correction
Gal Katz (Bar-Ilan University),
Doron Peled (Bar-Ilan University)
- Efficient Detection of Errors in Java Components Using Random
Environment and Restarts
Pavel Parizek (Charles University in Prague),
Tomas Kalibera (Charles
University in Prage)
James Larus (Microsoft Research, USA)
Programming Clouds
Session chair: Rajiv Gupta, University of California
at Riverside, USA
Session chair: J Nelson Amaral, University of Alberta, Canada
- Punctual Coalescing
Fernando Pereira, The Federal University of Minas Gerais (UFMG), Brazil
Jens Palsberg, UCLA, United States
- Strategies for Predicate-Aware Register Allocation
Gerolf Hoflehner, Intel Corp, United States
- Preference-Guided Register Assignment
Matthias Braun, Universitä Karlsruhe, Germany
Christoph Mallon, Saarland University, Germany
Sebastian Hack, Saarland University, Germany
- Validating register allocation and spilling
Silvain Rideau, Ecole Normale Supéeure, France
Xavier Leroy, INRIA Paris-Rocquencourt, France
Session chair: Markus Muller-Olm
- Toward a compositional theory of leftist grammars and transformations
Pierre Chambart (LSV-CNRS & ENS Cachan) and Philippe Schnoebelen
(LSV-CNRS & ENS Cachan).
- Degrees of Lookahead in Regular Infinite Games
Michael Holtmann (RWTH Aachen), Lukasz Kaiser (RWTH Aachen) and
Wolfgang Thomas (RWTH Aachen).
- Reachability analysis of communicating pushdown systems
Alexander Heu{\ss}ner (LaBRI, Universit{\'e} Bordeaux),
J\'{e}r\^{o}me Leroux (CNRS and LaBRI, Universit{\'e} Bordeaux), Anca
Muscholl (LaBRI, Universit{\'e} Bordeaux), and Gr\'{e}goire Sutre
(CNRS and LaBRI, Universit{\'e} Bordeaux).
- The Complexity of
Synchronous Notions of Information Flow Security
Franck Cassez (National ICT Australia & CNRS), Ron van der Meyden
(UNSW) and Chenyi Zhang (University of Luxembourg).
Session chair: Jan Rutten
- Monads need not be endofunctors
Thorsten Altenkirch (University of Nottingham), James Chapman
(Tallinn University of Technology) and Tarmo Uustalu (Tallinn
University of Technology).
- CIA Structures and the Semantics of Recursion
Stefan Milius (Technische Universit{\"a}t Braunschweig),
Lawrence Moss (Indiana University) and
Daniel Schwencke (Technische Universit{\"a}t Braunschweig).
- Coalgebraic Correspondence Theory
Lutz Schr{\"o}der (DFKI Bremen and Universität Bremen) and
Dirk Pattinson (Imperial College, London).
Session chair: Xavier Leroy, INRIA
Paris-Rocquencourt, France
- Automatic C-to-CUDA Code Generation for Affine Programs
Muthu Manikandan Baskaran, The Ohio State University, United States
J Ramanujam, Louisiana State University, United States
P Sadayappan, The Ohio State University, United States
- Is Reuse Distance Applicable to Data Locality Analysis on Chip Multiprocessors?
Yunlian Jiang, The College of William and Mary, United States
Eddy Zheng Zhang, The College of William and Mary, United States
Kai Tian, The College of William and Mary, United States
Xipeng Shen, The College of William and Mary, United States
- The Polyhedral Model Is More Widely Applicable Than You Think
Mohamed-Walid Benabderrahmane, Alchemy Group, INRIA Saclay and University of Paris-Sud 11, France
Cedric Bastoul, INRIA Saclay and University of Paris-Sud 11 and Reservoir Labs Inc, France
Albert Cohen, INRIA Saclay, France
Louis-Noel Pouchet, INRIA Saclay and University of Paris-Sud 11, France
- The Hot Path SSA Form: Extending the Single Static Assignment Form for Speculative Optimizations
Subhajit Roy, Indian Institute of Science, Bangalore, India
Y.N. Srikant, Indian Institute of Science, Bangalore, India
Session chair: Makoto Tatsuta
- Untyped Recursion Schemes and Infinite Intersection Types
Takeshi Tsukada (Tohoku University) and Naoki Kobayashi (Tohoku
University).
- Solvability in Resource Lambda-Calculus
Michele Pagani (University of Torino) and Simona Ronchi della
Rocca (University of Torino).
- A hierarchy for delimited continuations in call-by-name
Alexis Saurin (PPS & Equipe INRIA Pi.R2).
