No subject

Sebastien Mondet, Ashish Agarwal, Paul Scheid, Aviv Madar, Richard
Bonneau, Jane Carlton, Kristin C. Gunsalus
Managing and Analyzing Big-Data in Genomics


12:30-1:40 Lunch


1:40-2:55 Program Analysis and Verification
(3 25-minute slots)

J. Ian Johnson
Designing Precise Higher-Order Pushdown Flow Analyses

Eric Koskinen
Temporal property verification as a program analysis task

Gregory Malecha, Adam Chlipala, Patrick Hulin, and Edward Yang
A Framework for Verifying Low-level Programs


2:55-3:10 Break


3:10-4:00 Runtime Issues
(2 25-minute slots)

Kangkook Jee
A General Approach for Efficiently Accelerating Software-based Dynamic
Data Flow Tracking on Commodity Hardware

Jose Castanos, David Edelsohn, Kazuaki Ishizaki,Toshio Nakatani,
Takeshi Ogasawara, Priya Nagpurkar, Peng Wu
On the Benefits and Pitfalls of Extending a Statically Typed Language
JIT Compiler for Dynamic Scripting Languages

-------------------------------------------------------
Program Details

10:00-11:00 Keynote
Shriram Krishnamurthi
Securing JavaScript on the Web

JavaScript is the principal language for Web clients. =C2=A0It powers both
the content of pages and, in many cases, the browser itself.
JavaScript is also a large language with a complex semantics. =C2=A0In this
talk I will discuss our efforts to faithfully capture the essence of
JavaScript through an operational semantics and type system, and the
application of these to verifying multiple real-world systems.

Joint work with Arjun Guha, Joe Gibbs Politz, Ben Lerner, Claudiu
Saftoiu, Matt Carroll, and Hannah Quay-de la Vallee.


11:15-12:30 Concurrency
(3 25-minute slots)

Stephen Freund
Cooperative Concurrency for a Multicore World

Multithreaded programs are notoriously prone to unintended
interference between concurrent threads. =C2=A0To address this
problem, we argue that yield annotations in the source code
should document all thread interference, and we present a type
system for verifying the absence of undocumented interference.
Well-typed programs behave as if context switches occur only at
yield annotations. =C2=A0Thus, they can be understood using intuitive
sequential reasoning, except where yield annotations remind the
programmer to account for thread interference.

Experimental results show that our type system for yield
annotations is more precise at capturing thread interference than
prior techniques based on method-level atomicity specifications
and reduces the number of interference points a programmer must
reason about by an order of magnitude. The type system is also
more precise than prior methods targeting race freedom. =C2=A0In
addition, yield annotations highlight all known concurrency
defects in the Java programs studied.

This is joint work with Cormac Flanagan, Tim Disney, Caitlin
Sadowski, and Jaeheon Yi at UC Santa Cruz.


Y. Annie Liu