Autumn 2018 — Friday, 3:30pm — CSE 203

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.

Date	Who	What
Sep 28	Everyone!	Specifying 590P and Synthesizing the Schedule
Oct 5	Max Willsey, Chandrakana Nandi, Remy Wang	Liquid Types Read the abstract and intro (and maybe overview) of the original paper. Do a little bit (suggestion: first 3 sections) of the Liquid Haskell tutorial. For the curious, other liquid types papers can be found here.
Oct 12	Doug Woos, Sorawee Porncharoenwase	Who Tests the Testers Read this blog post about the paper
Oct 19	Talia Ringer, Jacob Van Geffen	BP: Formal Proofs, the Fine Print and Side Effects
Oct 26	Nate Yazdani	Verifying concurrent software using movers in CSPEC
Nov 2	Gus, Steven	Build systems a la carte
Nov 9	James Wilcox	The Left Hand of Equals (ONWARD 2016)
Nov 16	No one	PLDI: No Meeting
Nov 23	No Meeting	Thanksgiving Holiday
Nov 30	Jared Roesch, Marisa Kirasame	Programming with a Differentiable Forth Interpreter
Dec 7	No Meeting	CSE Holiday Party

Reading Papers

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.

Scheduling

Feel free to swap papers and dates or add yourself as a co-presenter to a topic.

Some Options for Autumn

• 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)
  • Talk at ICFP 2018 here
• Build Systems a la Carte
  • Talk at ICFP 2018 here.
• 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 asynchronous operations.
• 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)
  • This is the original paper describing the techniques used in the famous MOSS software plagarism detector used in many CS courses. A good companion reading might be Experience Using ”MOSS” to Detect Cheating On Programming Assignments. Discussion of this paper might touch on code clone detection and past papers we have discussed on copy and paste, and related blog posts.
• 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 is safe.
• 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 projects.

• 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

Previous suggestions:

• Are Mutation Scores Correlated with Real Fault Detection? A Large Scale Empirical study on the Relationship Between Mutants and Real Faults
• Efficient Sampling of SAT Solutions for Testing
• Inferring and Asserting Distributed System Invariants
• RFC-Directed Differential Testing of Certificate Validation in SSL/TLS Implementations
• Statistical Errors in Software Engineering Experiments: A Preliminary Literature Review
• Symbolic Verification of Regular Properties
• The Road to Live Programming: Insights From the Practice
• Practical Partial Evaluation for High-Performance Dynamic Language Runtimes
• Simple Testing Can Prevent Most Critical Failures: An Analysis of Production Failures in Distributed Data-Intensive Systems
• Automating Failure Testing Research at Internet Scale
• Lineage-driven Fault Injection
• Weird machines, exploitability, and provable unexploitability
• Complexity verification using guided theorem enumeration
• Keep It SIMPLEX: Satisfying Multiple Goals with Guarantees in Control-Based Self-Adaptive Systems
• Towards Automatic Resource Bound Analysis for OCaml
• Repairing Decision-Making Programs Under Uncertainty
• Paxos Made EPR: Decidable Reasoning about Distributed Protocols
• Towards Complete Specification and Verification with SMT
• Taming the Length Field in Binary Data: Calc-Regular Languages
• Dead Store Elimination (Still) Considered Harmful
• Growing a Protocol
• Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2
• Turing-Completeness Totally Free
• Optimizing Dynamically-Typed Object-Oriented Languages With Polymorphic Inline Caches
• Guarded recursive datatype constructors
• Towards Efficient, Typed LR Parsers
• Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections