This instance of NJPLS will take place in COS 105 in the Princeton Computer Science Department. Breakfast and lunch will be served just outside the auditorium.
Travel instructions may be found here.
| 9:30am | Breakfast |
| 10:00am |
Vellvm: Verifying Transformations of the LLVM IR
Steve Zdancewic, University of Pennsylvania |
| 11:00am | Coffee |
| 11:15am | Eric Koskinen, New York University (TBD) |
| 11:45am |
Space-efficient Manifest Contracts
Michael Greenberg, Princeton University |
| 12:15pm | Lunch |
| 1:30pm |
Of Ludics and Ludology: Interactive Worlds as Linear Logic Programs
Chris Martens, Carnegie Mellon University |
| 2:15pm | Coffee |
| 2:30pm | Business meeting |
| 2:45pm |
PASKET: Synthesizing Models of the Observer Pattern for Event-Driven Frameworks
Jinseong Jeon, University of Maryland |
| 3:15pm |
Verification of a Cryptographic Primitive: SHA-256
Andrew Appel, Princeton University |
The Low-Level Virtual Machine (LLVM) compiler provides a modern, industrial-strength SSA-based intermediate representation (IR) along with infrastructure support for many source languages and target platforms. Much of the LLVM compiler is structured as IR to IR translation passes that apply various optimizations and analyses.
In this talk, I will describe the Vellvm project, which seeks to provide a formal framework for developing machine-checkable proofs about LLVM IR programs and translation passes. I'll discuss some of the subtleties of modeling the LLVM IR semantics, including nondeterminism and its use of SSA representation. I'll also describe some of the proof techniques that we have used for reasoning about LLVM IR transformations and give two example applications: (1) formal verification of the SoftBound pass, which hardens C programs against memory safety errors, and (2) the mem2reg transformation, which promotes stack-allocated temporaries to registers and converts "trivial" SSA programs to "minimal, pruned" SSA programs.
Vellvm, which is implemented in the Coq theorem prover, provides facilities for extracting LLVM IR transformation passes and plugging them into the LLVM compiler, thus enabling us to create verified optimization passes for LLVM and evaluate them against their unverified counterparts. Our experimental results show that fully verified and automatically extracted implementations can yield competitive performance.
This is joint work with Jianzhou Zhao, Milo Martin, Santosh Nagarakatte, and Dmitri Garbuzov.
The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion. In this work, we show how to achieve space efficiency for contract checking. Working in a manifest context, we define a family of languages: classic λH, which is inefficient; forgetful λH, which is efficient but skips some checks; and heedful λH, which is efficient but may change blame labels. We show first that if classic λH produces a value, then so does forgetful λH (but not vice versa); we then show that classic and heedful λH yield identical values, but possibly differing blame labels.
Linear logic forms the foundation of theoretical and experimental frameworks for describing concurrent, distributed, and state-based systems. The properties that make it amenable to these domains, including resource-awareness, a frame property, and permutable structure in proofs, also work well for describing games (systems of play) and interactive narratives. Further, the tools afforded by focusing and constructivity allow for structural analysis on these encodings.
I'll describe ongoing work for my thesis on this topic, including the specification and "fuzz testing" of interactive stories that's possible with an existing implementation of CLF, a description of the language construct I've worked out on paper for introducing player interaction, and work-in-progress for the automated checking of linear logic programs maintaining author-specified invariants.
Modern applications are built using complex frameworks that are difficult to analyze, forcing analysis tool writers to manually create and maintain models of the framework that are simpler than the original code, a time-consuming and error-prone process. This paper presents PASKET, a new system that adds automation to the model generation process. We focus on models of Java frameworks that use the observer pattern, which is common in event- driven frameworks. PASKET takes as input an annotated API of the framework and tutorial programs that exercise the framework. From these artifacts, PASKET synthesizes an executable code model that matches the observer pattern- relevant behavior of the framework on the tutorial programs. We evaluated PASKET by synthesizing models for a subset of Swing based on eight tutorial programs. Our results show that the models derived by PASKET are sufficient to successfully re-execute the tutorials, both concretely and within Java PathFinder.
A full formal machine-checked verification of a C program: the OpenSSL implementation of SHA-256. This is an interactive proof of functional correctness in the Coq proof assistant, using the Verifiable C program logic.
Verifiable C is a separation logic for the C language, proved sound w.r.t. the operational semantics for C, connected to the CompCert verified optimizing C compiler.