APLAS – CPP 2012 Program
December 11 (Tuesday)
9:30
10:00
10:15
11:15
11:30

12:20
14:00

15:40
16:10

17:50

Registration
Opening
APLAS Invited talk by Jan Vitek (chair: Ranjit Jhala)“Planet Dynamic or: How I Learned to Stop Worrying and Love Reflection”(Short break)
APLAS Session 1: Concurrency (chair: Aquinas Hobor)
Siliang Li, Yu David Liu and Gang Tan: “JATO: Native Code Atomicity for Java”
Yi Lu, John Potter and Jingling Xue: “Ownership Types for Object Synchronisation”(Lunch break)
APLAS Session 2: Security (chair: Steve Zdancewic)
Lennart Beringer: “End-to-end multilevel hybrid information flow control”
Thomas Austin, Cormac Flanagan and Martı́n Abadi:“A Functional View of Imperative Information Flow”
Radha Jagadeesan, Corin Pitcher and James Riely:“Succour to the Confused Deputy: Types for Capabilities”
Aseem Rastogi, Avik Chaudhuri and Rob Johnson:“Types and Access Controls for Cross-Domain Security in Flash”(Break)APLAS Session 3: Static Analysis I (chair: Thomas Jensen)
Giulia Costantini, Pietro Ferrara and Agostino Cortesi:“Linear approximation of continuous systems with Trapezoid Step Functions”
Jorge Navas, Peter Schachte, Harald Sondergaard and Peter Stuckey:“Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code”
Pascal Sotin and Xavier Rival:“Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks”
Krystof Hoder, Andreas Holzer, Laura Kovacs and Andrei Voronkov Vinter:“A Vampire-Based Tool for Interpolation (tool)”(Day 1 over)December 12 (Wednesday) morning
9:15

10:05
10:40

11:55

APLAS Session 4: Static Analysis II (chair: Tachio Terauchi)
Kalmer Apinis, Helmut Seidl and Vesal Vojdani:“Side-Effecting Constraint Systems: A Swiss Army Knife for Program Analysis”
Mehdi Bouaziz, Francesco Logozzo and Manuel Fahndrich:“Inference of Necessary Field Conditions with Abstract Interpretation”(Break)APLAS Session 5: Language Design (chair: Keiko Nakata)
Oleg Kiselyov, Simon Peyton-Jones and Amr Sabry:“Lazy v. Yield: Incremental, Linear Pretty-printing”
Gabrielle Anderson and Julian Rathke:“Dynamic Software Update for Message Passing Programs”
Rémy Wyss, Frédéric Boniol, Julien Forget and Claire Pagetti:“A synchronous language with partial delay specification for real-timesystems programming”(Lunch break)December 12 (Wednesday) afternoon
14:00

APLAS Session 6: Dynamic Analysis (chair: Atsushi Igarashi)
Niloofar Razavi, Franjo Ivancic, Vineet Kahlon and Aarti Gupta:“Concurrent Test Generation using Concolic Multi-Trace Analysis”
Lukás̆ Marek, Yudi Zheng, Danilo Ansaloni, Aibek Sarimbekov, Walter Binder,
Petr Tůma and Zhengwei Qi:“Java Bytecode Instrumentation Made Easy: The DiSL Framework for
Dynamic Program Analysis (tool)”

14:50

APLAS Poster and Demo Session
Francois Berenger, Arnout Voet and Kam Y. J. Zhang:“Parallelization of a Computer Aided Drug Design Software with OCaml”
Aquinas Hobor, Soe Lin Myat and Bimlesh Wadhwa:“VisualizeSLE: A Visual Editor for Separation Logic Entailments”
Kanako Homizu, Ken Wakita and Akira Sasaki:“A Proposal of Implementation Technique for Hygienic Syntactic
Macro System for JavaScript”
Shin-ya Katsumata: “A Generic Soundness Result for Effect Systems”
Kazutaka Matsuda and Meng Wang: “FliPpr: A Prettier Invertible Printing System”
Akimasa Morihata and Shigeyuki Sato: “Syntax-Directed Parallel Data Flow Analysis”
Haruna Nishiwaki, Tomoharu Ugawa, Seiji Umatani, Masahiro Yasugi and Taiichi Yuasa:“Detecting Bugs in Android Using a Static Escape Analyzer SEAN for Native Code”
Julian Rathke, Paweł Sobociński and Owen Stephens:“ML kappa: Introducing Monoidal Categories to ML”
Idrisov Renat: “Sisal-based cloud service for educational and computation proposes”
Kanae Tsushima and Kenichi Asai: “An Embedded Type Debugger (demo)”
Masahiro Yasugi:“Typed Construction of Cyclic Data Structures Using Provisional Assumptions”
Oleg Kiselyov: “Can generative programming deliver?”Lukás̆ Marek, Yudi Zheng, Danilo Ansaloni, Aibek Sarimbekov, Walter Binder,Petr Tůma and Zhengwei Qi:“Java Bytecode Instrumentation Made Easy: The DiSL Framework for
Dynamic Program Analysis (tool)”
Pascal Sotin and Xavier Rival:“Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks (demo)”
Mehdi Bouaziz, Francesco Logozzo and Manuel Fahndrich:“Inference of Necessary Field Conditions with Abstract Interpretation”
Krystof Hoder, Andreas Holzer, Laura Kovacs and Andrei Voronkov:“Vinter: A Vampire-Based Tool for Interpolation (demo)”(Break)

15:50
16:20

17:35

APLAS Session 7: Semantics and Complexity (chair: Yukiyoshi Kameyama)
Aloı̈s Brunel and Antoine Madet:“Indexed realizability for bounded-time programming with references and type fixpoints”
Martin Avanzini, Naohi Eguchi and Georg Moser:“A New Order-theoretic Characterisation of the Polytime Computable Functions”
Marek Materzok and Dariusz Biernacki:“A Dynamic Interpretation of the CPS Hierarchy”(Day 2 over)December 13 (Thursday)
9:10
10:10
10:35

12:15
14:00
15:00
15:30

Joint invited talk by Greg Morrisett (chair: Zhong Shao)“Scalable Formal Machine Models”(Break)APLAS Session 8: Program Logics and Theorem Provers (chair: Chung-Kil Hur)Yu Guo, Xinyu Feng, Zhong Shao and Peizhi Shi:
“Modular Verification of Concurrent Thread Management”
David Costanzo and Zhong Shao:“A Case for Behavior-Preserving Actions in Separation Logic”
James Brotherston, Nikos Gorogiannis and Rasmus Petersen:“A Generic Cyclic Theorem Prover”
Xuan Bach Le, Cristian Gherghina and Aquinas Hobor:“Decision Procedures Over Sophisticated Fractional Permissions”(Lunch Break)
Joint invited talk by Xavier Leroy (chair: Dale Miller)“Mechanized Semantics for Compiler Verification”(Break)

17:00

CPP Session 1: Certified Compilation (chair: Chris Hawblitzel)
Valentin Robert and Xavier Leroy: “A formally-verified alias analysis”
Jianzhou Zhao and Steve Zdancewic:“Mechanized Verification of Computing Dominators for Formalizing Compilers”
Dominic Mulligan and Claudio Sacerdoti Coen:“On the correctness of an optimising assembler for the MCS-51 microcontroller”(Day 3 over)

19:00

APLAS – CPP Banquet at The Sodoh Higashiyama

December 14 (Friday) morning
9:10
10:10
10:40

12:10CPP Invited Talk by Gilles Barthe (chair: Gerwin Klein)“Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs”(Break)CPP Session 2: Execution and Testing (chair: Gerwin Klein)
Brian Campbell: “An Executable Semantics for CompCert C”
Pierre-Nicolas Tollitte, David Delahaye and Catherine Dubois:“Producing Certified Functional Code from Inductive Specifications”
Lukas Bulwahn: “The New Quickcheck for Isabelle –Random, Exhaustive and Symbolic Testing Under One Roof”(Lunch break)December 14 (Friday) afternoon
14:00

15:30
16:00

17:30

CPP Session 3: Operating Systems and Security (chair: Chris Hawblitzel)
Andrei Popescu, Johannes Hölzl and Tobias Nipkow:“Proving concurrent noninterference”
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein:“Noninterference for Operating System Kernels”
Alexander Vaynberg and Zhong Shao:“Compositional Verification of a Baby Virtual Memory Manager”(Break)CPP Session 4: Elegant Proofs (chair: Zhong Shao)
Keisuke Nakano: “Shall We Juggle, Coinductively?”
Beniamino Accattoli:“Proof pearl: Abella formalization of lambda calculus cube property”
Hing-Lun Chan and Michael Norrish:“A String of Pearls: Proofs of Fermat’s Little Theorem”(Day 4 over)December 15 (Saturday)
9:10
10:10
10:40

12:10
14:00

CPP Invited Talk by Naoki Kobayashi (chair: Georges Gonthier)“Program Certification by Higher-Order Model Checking”(Break)CPP Session 5: Logic and Types (chair: Dale Miller)
Kaustuv Chaudhuri: “Compact Proof Certificates for Linear Logic”
Christian Doczkal and Gert Smolka:“Constructive Completeness for Modal Logic with Transitive Closure”
Andrea Asperti and Wilmer Ricciotti: “Rating Disambiguation Errors”(Lunch break)
CPP Session 6: Mathematics (chair: Georges Gonthier)
Pierre Neron:“A Formal Proof of Square Root and Division Elimination in Embedded Programs”
Anders Mörtberg, Thierry Coquand and Vincent Siles:“Coherent and Strongly Discrete Rings in Type Theory”
Sylvie Boldo, Catherine Lelay and Guillaume Melquiond:“Improving Real Analysis in Coq: a User-Friendly Approach to Integrals
and Derivatives”