The Bronx Google Development Group is hosting a Machine Learning workshop followed by a panel for moving forward in CS.
Program reification is a new approach to the construction of verified concurrent programs and their proofs. This approach simplifies and scales (human and automated) reasoning by enabling a concurrent program to be represented and manipulated at multiple layers of abstraction. These abstraction layers are chained together via simple program transformations; each transformation is justified by a collection of automatically checked verification conditions.
An operating-system (OS) kernel is arguably the most important piece of software in a computer. Modern OS kernels have become extremely large and complex, containing millions of lines of code. As a result, they are unfortunately very buggy, and a single security bug (or vulnerability) may compromise the whole computer. Detecting and eliminating security bugs in OS kernels are thus imperative. However, kernel-bug detection has been considered a hard problem due to inherent limitations with whole-kernel analysis and the lack of bug specifications or detection oracles.
The cloud model can be viewed as a contract between customers and providers: customers program against the cloud model, and the cloud provider faithfully implements the model. In this talk, we focus on the problem of access control.
Gradual typing combines static and dynamic typing in the same program. Siek et al. (2015) describe five criteria for gradually typed languages, including type soundness and the gradual guarantee. A significant number of languages have been developed in academia and industry that support some of these criteria (TypeScript, Typed Racket, Safe TypeScript, Transient Reticulated Python, Thorn, etc.) but relatively few support all the criteria (Nom, Gradualtalk, Guarded Reticulated Python). Of those that do, only Nom does so efficiently.