by Aws Albarghouthi on Nov 4, 2021 | Tags: AI safety, deep learning, neural networks, verification
Deep learning has transformed the way we think of software and what it can do. But deep neural networks are fragile and their behaviors are often surprising. In many settings, we need to provide formal guarantees on the safety, security, correctness, or robustness of neural networks. In this post, I will talk about the verification problem for neural networks and some of the prominent verification techniques that are being developed. I will also discuss the great challenges that our community is well positioned to address and some of the ideas that we can port from the machine-learning community.
Read more...
by Michael Greenberg, Konstantinos Kallas, and Nikos Vasilakis on Oct 12, 2021 | Tags: correctness, distribution, future, HCI, parallelism, research, safety, security, semantics, shell, synthesis, Unix
With about half a century of life, the Unix shell is pervasive and entrenched in our computing infrastructure—with recent virtualization and containerization trends only propelling its use. A fresh surge of academic research highlights show potential for tackling long-standing open problems that are central to the shell and enable further progress. A recent panel discussion at HotOS ’21 concluded that improvements and research on the shell can be impactful and identified several such research directions. Maybe it’s time for your research to be applied to the shell too?
Read more...
by Sumit Gulwani on Sep 14, 2021 | Tags: Flash Fill, MIP award, program synthesis, Programming by Examples
My POPL 2011 “Flash Fill” paper was the most important turning point in my research career. I went from searching for the hardest problem I can solve to searching for the simplest problem that will have the most impact. It sensitized me to customer connection and enlightened me to how practical requirements can inspire foundational research ideas and directions. And most of all, it led to a blissful connection with my loved ones.
Read more...
by Sumanth Prabhu, Grigory Fedyukovich, Kumar Madhukar, and Deepak D'Souza on Sep 2, 2021 | Tags: automated programming, automated reasoning, logic-based verification
The problem of program verification is to find whether a program meets its specification. But if a program calls functions whose bodies are missing, the verification aims at finding the most general implementations of these functions. In this post we show how advances in automated reasoning allow for doing it efficiently.
Read more...
by Jay Lim and Santosh Nagarakatte on Aug 26, 2021 | Tags: awards, correct math libraries, optimization, program synthesis, runtimes
Everyone uses math libraries. Surprisingly, mainstream math libraries do not produce correct results for several thousands of inputs. Developers are seldom aware of them, which affects reproducibility and portability. We describe our new method for synthesizing elementary functions that produces correct results for all inputs but is also significantly faster than the state of the art libraries, which have been optimized for decades.
Read more...
by Christos Kozyrakis and Emery Berger on Aug 19, 2021 | Tags: ASPLOS, conferences, extended abstract, program committees, Review, Reviewing
Note: This is a cross-post from the ACM SIGARCH blog; see the original post for additional comments and discussion from the SIGARCH community. Background When we started planning the ASPLOS’21 program committee in Spring 2020, we asked ourselves what we could do to...
Read more...
by Nada Amin on Aug 12, 2021 | Tags: language design, programming, reflection
We give an introduction to reflective towers of interpreters, a semantic model of reflection with a user level interpreted by a meta level interpreted by a meta meta level and so on.
Read more...
by Shravan Narayan and Deian Stefan on Jul 27, 2021 | Tags: computer security, information flow control, sandboxing, type systems, WebAssembly
Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. The idea of SFI is old. Its use in production, to sandbox third-party libraries in Firefox, is new. We describe the PL techniques—notably static information flow control—that were key to deploying SFI in practice and their use in tackling software security more generally.
Read more...
by Alejandro Aguirre on Jul 15, 2021 | Tags: awards, formal verification, probabilistic programming
Sensitivity properties study how the output of a program changes when we make small changes to its input. How can we reason about sensitivity of programs that have probabilistic behavior?
Read more...
by Michael Hicks and Adrian Sampson on Jul 12, 2021 |
A brief farewell from Mike Hicks, outgoing co-editor at PL Perspectives, and a brief hello by Adrian Sampson, co-editor incoming!
Read more...
