by Santosh Nagarakatte and Jay Lim on Apr 28, 2022 | Tags: awards, correct math libraries, optimization, runtimes
To create a single polynomial approximation that produces correct results for multiple representations and rounding modes, we propose to generate a polynomial that generates the correctly rounded result of f(x) using the non-standard round-to-odd rounding mode with 2 additional precision bits compared to the largest floating point representation that we wish to support. We provide a proof that this method produces correctly rounded results for multiple representations and for all the standard rounding modes. More detailed explanation of our approach can be found in our POPL 2022 distinguished paper.
Read more...
by Sara Achour on Dec 14, 2021 | Tags: compilers, hardware, optimization, unconventional computing
Modern analog computers a host of analog behaviors that affect the fidelity of the mapped computation. How can we mitigate these analog behaviors in compilation?
Read more...
by Peter Sewell on Dec 7, 2021 | Tags: Reviewing
Peer review is an essential aspect of academic research, giving a feedback loop that stimulates and rewards high-quality work – but as we all know, it doesn’t always function well. To help maintain a consensus of what constitutes good reviewing, this note spells out some bad and good reasons to reject and accept papers.
Read more...
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...
