Winter 2019 — Friday, 3:30pm — CSE 403
Subscribe to the calendar: iCal
or Google Calendar
We’ll be reading and discussing exciting recent papers from the broader Software Engineering and Programming Language community, with a slight bias toward topics folks in UW PLSE are exploring.
Some paper links may point into the ACM Digital Library or the Springer online collection. Using a UW IP address, or the UW libraries off-campus access, should provide access.
Room: CSE 203
Specifying 590P and Synthesizing the Schedule
Room: CSE 303
Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)
Destination-Passing Style for Efficient Memory Management
Denali: a goal-directed superoptimizer
Prototyping a Functional Language using Higher-Order Logic Programming: A Functional Pearl on Learning the Ways of Lambda-Prolog/Makam
- If you know prolog well, you can follow the authors’ suggestion and skim the highlighted code chunks.
- Otherwise, try to read sections 1-7 & 11. Section 11 has a nice summary of their contribution.
- If you have never encountered logic programming, Atonis has a simple tutorial.
- There’s also a talk, but I didn’t find it to be too helpful.
Structuring the Synthesis of Heap-Manipulating Programs
code2vec: Learning Distributed Representations of Code
Live Functional Programming with Typed Holes
It may be useful to skim various advice
on how to constructively evaluate research papers. Note that these
principles also apply to reading group discussions! When considering
motivation in particular, the Heilmeier Catechism
is often a useful starting point.
Feel free to swap papers and dates or add yourself as a co-presenter to a topic.
Some Options for Winter
Evolution of Emacs Lisp
Nickel: A Framework for Design and Verification of Information Flow Control Systems
When Good Components Go Bad
Verifying concurrent software using movers in CSPEC
- Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)
- Build Systems a la Carte
- Synthesizing Robust Adversarial Examples
- Synthesizing an Instruction Selection Rule Library from Semantic Specifications
- Learning to Infer Graphics Programs from Hand-Drawn Images
- Premise Selection for Theorem Proving by Deep Graph Embedding
Deep Network Guided Proof Search
- Exploiting Community Structure for Floating-Point Precision Tuning (ISSTA 2018)
- This paper introduces a technique to shrink the search space for numerical
mixed-precision tuning by identifying groups of variables whose precisions
should be related.
- Control Plane Compression
- This paper introduces a technique to shrink control plane configurations
(e.g., for BGP) to smaller configurations. The compression preserves
several properties so that analysis by simulation and other tools is still
useful. Such tools run faster on smaller configurations.
- piCoq: parallel regression proving for large-scale verification projects (ISSTA 2018)
- Rechecking proofs for large projects can be expensive. However, a small
change in one module M often does not affect all the code in other modules
that depend on M. This paper introduce piCoq, a tool which tracks
fine-grained dependencies so that re-checking proofs only involves
running the definitions that may have been affected by a change.
This is a great example of tooling for “proof engineering”.
- Synchronizing the Asynchronous (CONCUR 2018)
- Reasoning about asynchronous programs is challenging because there are
many possible orderings for effects to happen. This paper introduces
a new proof rule for programs that makes reasoning about asynchronous
programs easier and more modular by using a synchronous summary of
- The Design and Implementation of Hyperupcalls (USENIX ATC 2018)
- Isolating code in a virtual machine is great for security and
scaling out, but has performance implications for guest programs
that would like to run on bare metal. This paper introduces
“hyperupcalls” which allow guest programs to get the hypervisor
to directly execute verified code directly on their behalf.
- Winnowing: Local Algorithms for Document Fingerprinting (SIGMOD 2003)
- Machine Learning: The High-Interest Credit Card of Technical Debt
- This paper discusses some of the maintenance and development
challenges that arise with systems based on machine learning.
Could lead to a great conversation about technical debt in
general and what tools or methodoligies can help mitigate it.
What should CI / regression testing / etc. look like for
machine learning? Also saw this,
but not sure how it’s relate (earlier/later version?).
- The Left Hand of Equals (ONWARD 2016)
- As any OOP programmer knows,
.equals() can be a pain.
This paper surveys the history of different ideas about
equality on OOP design and proposes a “left-handed equality”.
Will have to read the paper to figure out what that means,
but discussion could also talk about the challenges of
equality in proof assistants like Coq.
- Compiler Fuzzing through Deep Learning
- The title says it all. Compiler fuzzing is a challenging
area for test generation, but lots of impressive systems
have shown that the practice can find lots of bugs
(CSmith, VMI, etc.). Here the authors bring the
machine learning hammer to the party.
- The Machine that Builds Itself: How the Strengths of Lisp Family Languages Facilitate Building Complex and Flexible Bioinformatic Models
- This paper argues that languages in the Lisp family
are a great fit for artificial intellegence and machine
learning, especially because of how easily they support
building custom DSLs. Since Lisp was originally created
to do AI, it might interesting to get some history into
the discussion if we select this paper.
- BP: Formal Proofs, the Fine Print and Side Effects
- This paper takes a look at verified systems and their
trusted computing bases. In particular, they consider
the tradeoffs of verified guarantees vs. the design
compromises that must be made to actually prove software
- How Verified (or Tested) is My Code? Falsification-Driven Verification and Testing
- This paper applies ideas from mutation testing to help
verification engineers ensure their specifications correctly
capture the intuitive properties they want their systems
to satisfy. Given all the mutation testing and verification
expertise in house, should lead to a lively discussion!
- Logic Programming and Compiler Writing
- This paper from 1980 gives an introduction to logic programming
and discusses its use in building a compiler. It might be useful
to folks who haven’t seen logic programming before, or even to
those who are familiar with contemporary languages and want to
time travel a bit to see what things were like nearly 4 decades
ago. It seems that many popular language implementations these
days are still in low-level languages for performance or in
functional languages for pattern matching; are there any lessons
we should adopt from old ideas in logic programming?
- NetSpectre: Read Arbitrary Memory over Network
- This paper shows how Spectre attacks that leak (potentially secret)
data due to processor speculations can be adapted to remote attacks.
We generally don’t read many attack papers in this reading group,
but this one seems timely.
- A Trustworthy Proof Checker
- This is a classic paper by Appel et al. on minimizing the TCB of
a core proof checker. It could lead to a careful discussion of
TCB issues in general, and would likely be interesting to all the
proof assistant folks. It is also just a cool paper.
- TRIMMER: Application Specialization for Code Debloating (ASE 2018)
- This work introduces new analyses for debloating (optimizing for
program size). The authors provide a mechanism for users to
indicate context that permits cutting more functionality, and
it looks like they measure size in terms of “gadgets”.
- Who Tests the Testers? (ICER 2018)
- This paper lays out models for automated testing techniques
used commonly in CS education, identifies some pitfalls and
basic flaws in those approaches, and suggests ways to remedy
those shortcomings. Super relevant to our mission to impact
the world through CS education! Discussion should be a blast.
We should also read this related blog post.
- Synthesis of Asynchronous Reactive Programs from Temporal Specifications
- The class of reactive programs covers a large swath of important
applications, e.g., web browser kernels, user interfaces,
and many servers. This paper provides simpler, and potentially
more effective, techniques for synthesizing such systems.
- From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis
- (Abstract) This paper describes some of the challenges and opportunities
when deploying static and dynamic analysis at scale, drawing on the
authors’ experience with the Infer and Sapienz Technologies at Facebook,
each of which started life as a research-led start-up that was subsequently
deployed at scale, impacting billions of people worldwide. The paper
identifies open problems that have yet to receive significant attention
from the scientific community, yet which have potential for profound real
world impact, formulating these as research questions that, we believe, are
ripe for exploration and that would make excellent topics for research
Foreshadow Breaking the Virtual Memory Abstraction with Transient Out-of-Order Execution
CraftML: 3D Modeling is Web Programming
Google Vizier: A Service for Black-Box Optimization
Intermediate representations in imperative compilers: A survey
- Towards Certified Meta-Programming with Typed Template-Coq