Towards Robust and Explainable Artificial Intelligence

Deep learning has led to rapid progress being made in the field of machine learning and artificial intelligence, leading to dramatically improved solutions of many challenging problems such as image understanding, speech recognition, and control systems. Despite these remarkable successes, researchers have observed some intriguing and troubling aspects of the behaviour of these models. A case in point is the presence of adversarial examples which make learning based systems fail in unexpected ways. Such behaviour and the difficulty of interpreting the behaviour of neural networks is a serious hindrance in the deployment of these models for safety-critical applications. In this talk, I will review the challenges in developing models that are robust and explainable and discuss the opportunities for collaboration between the formal methods and machine learning communities.

Pushmeet Kohli 
DeepMind, UK

Pushmeet Kohli is the Head of research for the "AI for science" and "Robust & Reliable AI"  groups at DeepMind. His research revolves around Intelligent Systems and Computational Sciences. His current research interests include Safe and Verified AI, Probabilistic Programming, Interpretable and Verifiable Knowledge Representations of Deep Models. In terms of application domains, he is interested in goal-directed conversation agents, machine learning systems for healthcare, and 3D reconstruction and tracking for augmented and virtual reality. Pushmeet’s research has appeared in conferences in the field of machine learning, computer vision, game theory and human computer interaction and have won awards in CVPR, WWW, CHI, ECCV, ISMAR, TVX and ICVGIP. His research has also been the subject of a number of articles in popular media outlets such as Forbes, Wired, BBC, New Scientist and MIT Technology Review. Pushmeet is on the editorial board or PAMI, JMLR, IJCV and CVIU.

Gradient Descent: The Ultimate Optimizer

Working with any gradient-based machine learning algorithm requires the tedious task of tuning its hyperparameters, such as the learning rate. There exist more advanced techniques for automated hyperparameter optimization, but they themselves introduce even more hyperparameters to control the optimization process. We propose to learn the hyperparameters by gradient descent, and furthermore to learn the hyper-hyperparameters by gradient descent as well, and so on. As these towers of optimizers grow, they become significantly less sensitive to the choice of top-level hyperparameters, hence decreasing the burden on the user to search for optimal values.

Erik Meijer (Facebook)

Bio: Wikipedia

What is a Programming Language? What is a Program? What is a Programmer?

It is becoming clear that traditional software development activities, like editing, testing, debugging, etc. need to be carried out by many individuals who are not typical software developers. Tools as diverse as spreadsheets, Jupyter notebooks, and deep learning frameworks all seek to empower users to create solutions that have much in common with traditional software. Unfortunately, typical software tools do not directly translate into these new development processes. In my talk, I will follow the path of the revolution that empowers more and more people to easily leverage computational resources for problem solving.

I will use spreadsheets as a starting point for illustrating the incredible opportunities but also the technical challenges of empowering users to quickly build correct and meaningful spreadsheets. Spreadsheets combine code (formulas), data, and presentation in a way that makes understanding the user intent (and the “specification”) difficult. I will briefly mention program synthesis technologies like Excel FlashFill and FlashRelate but focus more on my recent efforts to combine spatial analysis, statistical analysis, and deep learning to find bugs in spreadsheets. In the ExceLint project, with Daniel Barowy and Emery Berger, we use a combination of program analysis, spatial, analysis, and statistical analysis to highlight unusual anomalous formulas in spreadsheets. In the Jura project, with Saswat Padhi, Alex Polozov and Dany Rouhana, we apply deep neural networks trained on thousands of spreadsheets to predict properties of sheets including where tables are located and whether cells should contain formulas.

Understanding how to combine an understanding of program structure with human intent is central to empower any individual in data science, ML model training, etc. to more effectively create software solutions that are efficient and correct. The resulting opportunities and impact of work in this area is enormous.

Ben Zorn
Microsoft Research

Ben Zorn is a Partner Researcher in the Research in Software Engineering (RiSE) group in Microsoft Research, Redmond. After receiving a PhD in Computer Science from UC Berkeley in 1989, he served eight years on the Computer Science faculty at the University of Colorado in Boulder, receiving tenure and being promoted to Associate Professor in 1996. He left the University of Colorado in 1998 to join Microsoft Research, where he currently works. Dr. Zorn’s research interests include programming language design and implementation for reliability, security, and performance. He has served as both Program Chair and General Chair of the PLDI conference, as an Associate Editor of the ACM journals Transactions on Programming Languages and Systems and Transactions on Architecture and Code Optimization. He has also served seven years as a Member-at-Large of the SIGPLAN Executive Committee and currently serves on the Computing Community Consortium (CCC) Council, a committee of the Computing Research Association.

Compiler Verification: The Next Generation

Compiler verification is an old problem, with results stretching back beyond the last half century. In the last dozen years, following the pioneering work on CompCert, the field has witnessed remarkable progress in fully machine-verified compilers. Yet, until quite recently, despite some truly impressive verification efforts, the theorems being proved were only about correctness of whole-program compilers whose output we assume is never linked with any other code--an unrealistic assumption that ignores the reality of how we use these compilers.

In this talk, I'll discuss the next generation of compiler-verification challenges that arise when we acknowledge that compilers are used to compile program fragments, not whole programs, which are then linked with code produced by different compilers, from different languages, often by potentially malicious actors. A verified compiler should preserve source-code behavior as well as source-level safety and security guarantees, but even specifying these properties is nontrivial in the presence of interactions with foreign code. I'll present the formidable verification challenges we face when compiling, for instance, programs with FFIs, DSLs that offer security guarantees, and languages that rely on cryptographically enforced security. I will discuss how to structure future research efforts so we can build compilers that are correct, secure, and performant.

Amal Ahmed
Northeastern University

Amal Ahmed holds the Sy and Laurie Sternberg Associate Professorship at Northeastern University. She received her Bachelor's from Brown University, her Master's from Stanford, and her PhD from Princeton, all in Computer Science. Her interests include type systems and semantics, compiler verification, language interoperability, gradual typing, and dependent types. She is known for showing how to scale the logical relations proof method, via step-indexing, to realistic languages with features such as higher-order mutable state and concurrency, leading to widespread use of the technique. Her recent work has focused on developing an architecture for building correct and secure compilers that support safe inter-language linking of compiled code. Her awards include an NSF Career Award and a Google Faculty Research Award.

A Dependently-Typed Core Calculus for GHC

In this talk, I will give an overview of a proposed intermediate language that adds dependent types to the Glasgow Haskell Compiler (GHC). This challenge has forced my collaborators and I to consider how dependency interacts with GHC's many language features, including nontermination, parametric polymorphism, type families, GADTs and safe coercions. In response to these constraints, we have developed a core calculus that integrates dependent types while remaining backwards compatible with existing Haskell. Furthermore, to make sure that this core calculus is a firm foundation for Haskell, we have used the Coq proof assistant to verify its metatheoretic properties, including type soundness.

Stephanie Weirich
University of Pennsylvania

Stephanie Weirich is a Professor of Computer and Information Science at the University of Pennsylvania. She has made contributions in the areas of functional programming, type systems, machine-assisted theorem proving and dependent types. Dr. Weirich has served as the program chair of POPL 2019, ICFP 2010, the 2009 Haskell Symposium, and as an editor for the Journal of Functional Programming. She has also been recognized by the SIGPLAN Milner Young Researcher award (2016), a Microsoft Outstanding collaborator award, and a most influential ICFP paper award (awarded in 2016, for 2006).

(Programming Languages) in Agda = Programming (Languages in Agda)

The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of an implication is a function, proof by induction is just recursion. Dependently-typed programming languages, such as Agda, exploit this pun. To prove properties of programming languages in Agda, all we need to do is program a description of those languages in Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking a program.

Accordingly, I have written a new textbook, Programming Language Foundations in Agda (PLFA), as a literate script for the proof assistant Agda. In this talk I will describe three things I learned from writing PFLA, and I will touch on the role Agda plays in IOHK's new cryptocurrency.

The textbook can be found here: http://plfa.inf.ed.ac.uk

Philip Wadler
University of Edinburgh and IOHK

Philip Wadler likes to introduce theory into practice, and practice into theory. An example of theory into practice: GJ, the basis for Java with generics, derives from quantifiers in second-order logic. An example of practice into theory: Featherweight Java specifies the core of Java in less than one page of rules. He is a principal designer of the Haskell programming language, contributing to its two main innovations, type classes and monads. The YouTube video of his Strange Loop talk Propositions as Types has over 50,000 views.

Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh and Senior Research Fellow at IOHK. He is an ACM Fellow, a Fellow of the Royal Society of Edinburgh, and editor-in-chief of Proceedings of the ACM for Programming Languages. He is past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, winner of the SIGPLAN Distinguished Service Award, and a winner of the POPL Most Influential Paper Award. Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris. He has an h-index of 71 with more than 24,000 citations to his work, according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004), Generics and Collections in Java (O'Reilly, 2006), and Programming Language Foundations in Agda (2018). He has delivered invited talks in locations ranging from Aizu to Zurich.

Compiling Domain Specific Languages to Domain Specific Architectures

The slow down of Moore’s Law and the performance demands of machine leaning applications calls for new ways of designing computer systems. Two ideas that have gained currency recently are the use of Domain Specific Languages (DSLs) to improve the productivity of software developers especially for machine learning applications and the use of Domain Specific Architectures (DSAs) to increase energy efficiency. In this talk I will describe how DSLs can be designed for programmability and performance using advanced compilation technology based on parallel patterns. These DSLs and compiler technology can be used to bridge the gap between application programmers and efficient execution on specialized architectures. Plasticine is a spatially reconfigurable dataflow architecture designed to efficiently execute applications composed of parallel patterns. I will describe the Plasticine architecture: the compute pipeline that exploits nested parallel patterns, the configurable memory system that captures data locality and sustains compute throughput with multiple banking modes, and the on-chip interconnect that supports communication at multiple levels of granularity.

Kunle Olukotun
Stanford University

Kunle Olukotun is the Cadence Design Professor of Electrical Engineering and Computer Science at Stanford University. Olukotun is well known as a pioneer in multicore processor design and the leader of the Stanford Hydra chip multipocessor (CMP) research project. Olukotun founded Afara Websystems to develop high-throughput, low-power multicore processors for server systems. The Afara multicore processor, called Niagara, was acquired by Sun Microsystems. Niagara derived processors now power all Oracle SPARC-based servers. Olukotun currently directs the Stanford Pervasive Parallelism Lab (PPL), which seeks to proliferate the use of heterogeneous parallelism in all application areas using Domain Specific Languages (DSLs). Olukotun is a member of the Data Analytics for What’s Next (DAWN) Lab which is developing infrastructure for usable machine learning. Olukotun is an ACM Fellow and IEEE Fellow for contributions to multiprocessors on a chip and multi-threaded processor design and is the recipient of of the 2018 IEEE Harry H. Goode Memorial Award. Olukotun received his Ph.D. in Computer Engineering from The University of Michigan.

Software for AI and AI for Software

Lin Tan, Purdue University

In this talk, I will discuss some of our recent research focuses on using software engineering approaches such as differential testing to improve the dependability of machine learning software, and leveraging machine learning and natural language processing techniques to improve software dependability.

Machine learning software is widely used in domains including aircraft collision avoidance systems, Alzheimer’s disease diagnosis, and autonomous driving cars. Despite the requirement for high reliability, machine learning software is difficult to test. Thus, I will describe a new approach that (1) performs cross-implementation inconsistency checking to detect bugs in deep learning software, and (2) analyzes anomaly propagation to localize faulty functions in deep learning software that cause the bugs.

On the other hand, AI techniques such as machine learning techniques and natural language processing can be used to improve software dependability and software engineering processes. I will briefly talk about some examples such as building machine learning models to automatically fix bugs and learning program specifications from software text.

New Directions in Representation Learning of Logical Formulae

Bruno Ribeiro, Purdue University

My talk starts by turning back the clock to 1931 and 1981, introducing the ideas that culminated with the fundamental representation theorem of graphs (the Aldous–Hoover theorem). I will then show how these ideas connect to logical formulae, introducing a few applications, and explaining why existing representation methods of logical formulae are not as expressive as they could be. I will then introduce the concept of learning invariant representations through a general framework of graph representation learning using deep neural networks, which is directly rooted in the ideas that gave us the Aldous–Hoover representation theorem. Finally, I will show how this new representation framework points to novel representation learning methods of logical formulae. I will end my talk with a few open problems.

Memory Hard Functions and Password Hashing

Jeremiah Blocki, Purdue University

In the last few years breaches at organizations like Yahoo!, Dropbox, Lastpass, AshleyMadison and Adult FriendFinder have exposed billions of user passwords to offline brute-force attacks. Password hashing algorithms are a critical last line of defense against an offline attacker who has stolen password hash values from an authentication server. An attacker who has stolen a user's password hash value can attempt to crack each user's password offline by comparing the hashes of likely password guesses with the stolen hash value. Because the attacker can check each guess offline it is no longer possible to lockout the adversary after several incorrect guesses. The attacker is limited only by the cost of computing the hash function. Offline attacks are increasingly commonplace and dangerous due to weak password selection and improved cracking hardware such as a GPU, Field Programmable Gate Array (FPGA) or an Application Specific Integrated Circuit (ASIC).

A secure password hashing algorithm should have the properties that (1) it can be computed quickly (e.g., at most one second) on a personal computer, (2) it is prohibitively expensive for an attacker to compute the function millions or billions of times to crack the user's password even if the attacker uses customized hardware. The first property ensures that the password hashing algorithm does not introduce an intolerably long delay for the user during authentication, and the second property ensures that an offline attacker will fail to crack most user passwords. Memory hard functions (MHFs), functions whose computation require a large amount of memory, are a promising cryptographic primitive to enable the design of a password hashing algorithm achieving both goals.

The talk will introduce and motivate the notion of memory hard functions and survey recent advances in the theory of MHFs. These results include (1) an attack on the Argon2i MHF, winner of the password hashing competition, which could reduce an amortized costs for a password attacker, (2) security lower bound for the SCRYPT MHF and (3) construction of the first provably secure data-independent memory hard function.

Discover[i]: Component-based Parameterized Reasoning for Distributed Applications

Roopsha Samanta, Purdue University

In this talk, I will present our Discover[i] project which seeks to automate reasoning about new classes of distributed applications, built on top of verified components and parameterized by the number of processes. I will focus on parameterized verification and synthesis of systems that use consensus protocols, such as Paxos, as a building block to provide higher-level functionality. I will explain the key ingredients of our framework: (1) an abstraction of consensus with a simple atomic primitive, (2) a decidability result and algorithm for parameterized verification of safety properties of systems with such consensus primitives, and (3) an algorithm for parameterized synthesis of coordination for such systems.

This is joint work with Nouraldin Jaber, Swen Schewe and Milind Kulkarni.

Naturally Editing Typed Expressions with Holes

Cyrus Omar & David Moon, University of Michigan

We present a progress report on the Hazel (hazel.org) program editor. Hazel is unique in that every editor state in Hazel has a type and a result, possibly with holes. Maintaining this strong edit-time invariant, which we have previously formally established, presents usability challenges. To address these challenges, we are working on developing a number of user interface techniques, including (1) sequential representations of infix operator sequence and line items in programs, so that familiar sequential editing operations work as expected and less intuitive local tree transformations are not needed; (2) staging modes that allow for the movement of delimiters to new positions without going through meaningless intermediate stages; and (3) a mechanism for filling typed holes by interacting with live GUIs associated with the type, e.g. a color chooser for filling a hole of Color type. The talk will include a demo of our prototype implementation.

Learning Network Design Objectives Using A Program Synthesis Approach

Yanjun Wang, Purdue University

While the networking community has extensively tackled network design problems using optimization or other techniques, (e.g., in areas such as traffic-engineering, and resource allocation), much of this work focuses on efficiently generating designs assuming well-defined objectives. In this paper, we argue that in practice, the objectives of a network design task may not be easy to specify for an architect. We argue for, and present a structured approach where the objectives of a network design task are learnt through iterative interactions with the architect. Our approach is inspired by a programming-by-examples approach that has seen success in the programming languages community. However, conventional program synthesis techniques do not apply because in our context a user can only provide a relative comparison between multiple choices on which one is more desirable, rather than provide an exact output for a given input. We propose a novel comparative synthesis approach to tackle these challenges. We sketch the approach, present promising preliminary results, and discuss future research questions.

Program Synthesis with Live Bidirectional Evaluation

Justin Lubin, University of Chicago

We present an algorithm for completing program sketches (partial programs, with holes), in which evaluation and example-based synthesis are interleaved until the program is complete and produces a value. Our approach combines and extends recent advances in live programming with holes and type-and-example-directed synthesis of recursive functions over algebraic data types. Novel to our formulation is the ability to simultaneously solve interdependent synthesis goals—the key ideas are to iteratively solve constraints that arise during "forward" evaluation of candidate completions and to propagate examples "backward" through partial results. We implement our approach in a prototype system, called Sketch-n-Myth, and develop several examples that demonstrate how live example-directed program synthesis enables a novel workflow for programming with synthesis. Our techniques thus contribute to ongoing efforts to develop synthesis algorithms that can be deployed in future programming environments.

On the correctness of electronic documents: studying, finding, and localizing inconsistency bugs in PDF readers and files

Thibault Lutellier, Waterloo University

Electronic documents are widely used to store and share information such as bank statements, contracts, articles, maps and tax information. Many different applications exist for displaying a given electronic document, and users rightfully assume that documents will be rendered similarly independently of the application used. However, this is not always the case, and these inconsistencies, regardless of their causes—bugs in the application or the file itself—can become critical sources of miscommunication. In this paper, we present a study on the correctness of PDF documents and readers. We start by manually investigating a large number of real-world PDF documents to understand the frequency and characteristics of cross-reader inconsistencies, and find that such inconsistencies are common—13.5% PDF files are inconsistently rendered by at least one popular reader. We then propose an approach to detect and localize the source of such inconsistencies automatically. We evaluate our automatic approach on a large corpus of over 230 K documents using 11 popular readers and our experiments have detected 30 unique bugs in these readers and files. We also reported 33 bugs, some of which have already been confirmed or fixed by developers.

Algebraic Program Analysis

John Cyphert, University of Wisconsin

In this talk, I will present an overview of a line of recent work on Algebraic Program Analysis. This style of analysis stands in contrast to the classic iterative style of program analysis by directly computing abstract summaries for iterative program behavior. This approach has the advantage of not relying on brittle widening operators to ensure that an analyzer terminates. I will explain the algebraic approach using Compositional Recurrence Analysis (CRA) as a specific instantiation of the algebraic-analysis framework. CRA generates program invariants in the style of an effective denotational semantics, building abstract transition formulas in a bottom-up manner over the syntax of the program. CRA summarizes iterative behavior by extracting and solving implied recurrences from loop bodies to yield abstract summaries, which can include polynomials, exponentials, and logarithms. I will also explain how the predictability of algebraic analysis can be exploited to yield program transformations that are guaranteed to not decrease analysis precision. We have briefly explored some of CRA's capabilities including numerical invariant generation, complexity analysis, and assertion checking; furthermore, we are interested in discovering additional applications.

Optimistic Hybrid Analysis for Fast Dynamic Information Flow Tracking

Subarno Bannerjee, University of Michigan

Optimistic Hybrid Analysis makes expensive dynamic analyses practical by assuming likely program invariants to improve static analysis' precision thereby inducing more dynamic analysis optimizations. We present a rollback-free construction of OHA and apply it to achieve low-overhead solutions to two important dynamic analyses- (1) taint tracking; (2) pointer type and provenance tracking for safe garbage collection in type-unsafe languages.

Decidable Synthesis of Uninterpreted Programs

Paul Krogmeier, UIUC

We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class use uninterpreted functions and relations, and abide by a restriction called coherence that was recently identified to yield decidable verification. We formulate a powerful grammar-restricted (syntax-guided) synthesis problem for coherent uninterpreted programs and show the problem to be decidable. We identify its precise complexity, which is doubly exponential in the set of program variables and linear in the size of the grammar. The decision procedure uses tree automata which accept finite syntax trees of all correct programs. It checks that each of the infinitely many executions for a given program is correct using a finite memory streaming congruence closure algorithm. We also study variants of uninterpreted program synthesis: synthesis of transition systems with lower complexity (EXPTIME), synthesis of recursive programs, and synthesis of Boolean programs. We also show undecidability results that argue the necessity of our restrictions.

The verified-classes library: big proofs, little tedium

Ryan Scott. Indiana University

The verified-classes library is your one-stop shop for implementing proofs of type class laws without significant amounts of boilerplate. Based on our Haskell'19 paper, verified-classes offers a framework for writing generic proofs that can be reused across many different data types. Moreover, the size of these proofs does not change as the size of the data types involved grows, whereas direct proofs of class laws often grow superlinearly. In this talk, we examine the design of verified-classes, some of the challenges that Haskell poses that we must overcome, and discuss a case study involving class laws from Haskell's standard library.

CLOTHO: Directed Test Generation for Weakly Consistent Database Systems

Kia Rahmani, Purdue University

Relational database applications are notoriously difficult to test and debug. Concurrent execution of database transactions may violate complex structural invariants that constraint how changes to the contents of one (shared) table affect the contents of another. Simplifying the underlying concurrency model is one way to ameliorate the difficulty of understanding how concurrent accesses and updates can affect database state with respect to these sophisticated properties. Enforcing serializable execution of all transactions achieves this simplification, but it comes at a significant price in performance, especially at scale, where database state is often replicated to improve latency and availability.

To address these challenges, this paper presents a novel testing framework for detecting serializability violations in (SQL) database-backed Java applications executing on weakly-consistent storage systems. We manifest our approach in a tool, CLOTHO, that combines a static analyzer and model checker to generate abstract executions, discover serializability violations in these executions, and translate them back into concrete test inputs suitable for deployment in a test environment. To the best of our knowledge, CLOTHO, is the first automated test generation facility for identifying serializability anomalies of Java applications intended to operate in geo-replicated distributed environments. An experimental evaluation on a set of industry-standard benchmarks demonstrates the utility of our approach.

Privacy-Preserving Event Frequency Analysis for Deployed Software

Hailong Zhang, Ohio State University

Field data generated by deployed software provides exhaustive information about users' interactions with the software. There are significant concerns about the collection and use of such data, e.g., for targeted advertisement. Differential privacy is a powerful machinery that enables principled and quantifiable analysis of the trade-offs between the benefits of data gathering (for software developers) and the corresponding privacy loss (for software users). In this talk, we demonstrate a preliminary exploration in the field of mobile app analytics showing the practicality of DP based approaches. Finally, we discuss the open questions and future work in the increasingly important area of privacy-preserving software analysis.

Learning from, Understanding, and Supporting DevOps Artifacts

Jordan Henkel, University of Wisconsin

With the growing use of DevOps tools and frameworks, there is an increased need for tools and techniques that support more than code. The current state-of-the-art in static developer assistance for tools like Docker is limited to shallow syntactic validation. In this talk, we identify three core challenges in the realm of learning from, understanding, and supporting developers writing DevOps artifacts: (i) nested languages in DevOps artifacts, (ii) the lack of semantic rule-based analysis, and (iii) idiom mining. To address these challenges we introduce a tool, binnacle, that allowed us to ingest about 900,000 GitHub repositories. From this large set of repositories, we found that over 25% used some kind of DevOps artifact.

Focusing on Docker, we extracted approximately 240,000 Dockerfiles, and also identified a Gold Set of Dockerfiles written by Docker experts. We addressed challenge (i) by reducing the number of effectively uninterpretable nodes in our ASTs by over 80% via a technique we call phased parsing. To address challenge (ii), we manually collected a set of idioms for Dockerfiles from commits to the files in the Gold Set. We created an analyzer that used these rules, and found that, on average, Dockerfiles on GitHub violated the rules six times more frequently than the Dockerfiles in our Gold Set. Finally, to address challenge (iii), we introduced a novel idiom-mining technique and recovered 26 idioms, automatically, from our data. Of these 26 idioms, 6 matched idioms that we had manually mined, 4 were interesting rules that we had overlooked in our manual extraction, 12 were uninteresting but correct (e.g., the cp command takes at least two paths in its argument list), and 4 were correct but reflected quirks of the data in our Gold Set.

Storm: Program Reduction for Testing and Debugging Probabilistic Programming Systems

Saikat Dutta, UIUC

Probabilistic programming languages offer an intuitive way to model uncertainty by representing complex probability models as simple probabilistic programs. Probabilistic programming systems (PP systems) hide the complexity of inference algorithms away from the program developer. Unfortunately, if a failure occurs during the run of a PP system, a developer typically has very little support in finding the part of the probabilistic program that causes the failure in the system. This paper presents Storm, a novel general framework for reducing probabilistic programs. Given a probabilistic program (with associated data and inference arguments) that causes a failure in a PP system, Storm finds a smaller version of the program, data, and arguments that cause the same failure. Storm is language-agnostic: it translates programs from the existing systems to a common intermediate representation: Storm-IR. Storm leverages both generic code and data transformations from compiler testing and domain-specific, probabilistic transformations. This paper presents new transformations that reduce the complexity of statements and expressions, reduce data size, and simplify inference arguments (e.g., the number of iterations of the inference algorithm). We define all our analyses and transformations on Storm-IR and finally output the reduced program back to the source language. We evaluated Storm on 47 programs that caused failures in two popular probabilistic programming systems, Stan and Pyro. Our experimental results show Storm’s effectiveness. For Stan, our minimized programs have 49% less code, 67% less data, and 96% fewer iterations. For Pyro, our minimized programs have 58% less code, 96% less data, and 99% fewer iterations. Storm shows a significant improvement in the number of removed data points and program constructs over the baseline approach that applies only generic transformations. We also show the benefits of Storm when debugging probabilistic programs. This paper was accepted and will be presented in ESEC/FSE '19.

Decidable Verification of Uninterpreted Programs

Umang Mathur, UIUC

In this talk, I will talk about our recent decidability result on verifying uninterpreted programs. Uninterpreted programs are written using uninterpreted functions, constants and relations in their syntax, and are meant to work over arbitrary data models that provide interpretations to these uninterpreted symbols. The verification problem asks whether a given program satisfies a postcondition written using quantifier-free formulas with equality on the final state, with no loop invariants, contracts, etc. being provided. While this problem is undecidable in general, we introduce a novel subclass of programs, called coherent programs that admits decidable verification, and can be decided in PSPACE. We then extend this class of programs to classes of programs that are k-coherent, where k ∈ ℕ, obtained by (automatically) adding k ghost variables and assignments that make them coherent. We also extend the decidability result to programs with recursive function calls and prove several undecidability results that show why our restrictions to obtain decidability seem necessary. Our new decidability results have opened up several new avenues for PL research, which I will discuss in the talk.

ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks

Xuankang Lin, Purdue University

Artificial neural networks (ANNs) have demonstrated remarkable utility in a variety of challenging machine learning applications. However, their complex architecture makes asserting any formal guarantees about their behavior difficult. Existing approaches to this problem typically consider verification as a post facto white-box process, one that reasons about the safety of an existing network through exploration of its internal structure.

In this talk, we present a novel learning framework ART that enables the construction of provably correct networks with respect to a broad class of safety properties, a capability that goes well-beyond existing approaches. Our key insight is that we can integrate an optimization-based abstraction refinement loop into the learning process that dynamically splits the input space from which training data is drawn, based on the efficacy with which such a partition enables safety verification. In addition to some theoretical results for the soundness of our approach, we empirically demonstrate that realizing soundness does not come at the price of accuracy, giving us a meaningful pathway for building both precise and correct networks.

Verifying Safety and Accuracy of Approximate Parallel Programs via Canonical Sequentialization

Vimuth Fernando, UIUC

Parallely is a programming language and a system for verification of approximations in parallel message-passing programs. Parallely’s language can express various software and hardware level approximations that reduce the computation and communication overheads at the cost of result accuracy.

Parallely’s safety analysis can prove the absence of deadlocks in approximate computations and its type system can ensure that approximate values do not interfere with precise values. Parallely’s quantitative accuracy analysis can reason about the frequency and magnitude of error. To support such analyses, Parallely presents an approximation-aware version of canonical sequentialization, a recently proposed verification technique that generates sequential programs that capture the semantics of well-structured parallel programs (i.e., ones that satisfy a symmetric nondeterminism property). To the best of our knowledge, Parallely is the first system designed to analyze parallel approximate programs.

We demonstrate the effectiveness of Parallely on eight benchmark applications from the domains of graph analytics, image processing, and numerical analysis. We also encode and study five approximation mechanisms from literature. Our implementation of Parallely automatically and efficiently proves type safety, reliability, and accuracy properties of the approximate benchmarks

Rethinking (and Replacing) Regular Expressions After 50 Years

Jamie Jennings. NCSU

ABSTRACT TO COME

Partial Type Constructors; Or, Making ad hoc datatypes less ad hoc

Garrett Morris, University of Kansas

Functional programming languages assume that type constructors are total. Yet functional programmers know better: counterexamples range from container types that make limiting assumptions about their contents (e.g., requiring computable equality or ordering functions) to type families with defining equations only over certain choices of arguments. We present a language design and formal theory of partial type constructors, capturing the domains of type constructors using qualified types. Our design is both simple and expressive: we support partial datatypes as first-class citizens (including as instances of parametric abstractions, such as the Haskell Functor and Monad classes), and show a simple type elaboration algorithm that avoids placing undue annotation burden on programmers. We show that our type system rejects ill-defined types and can be compiled to a semantic model based on System F. Finally, we have conducted an experimental analysis of a body of Haskell code, using a proof-of-concept implementation of our system; while there are cases where our system requires additional annotations, these cases are rarely encountered in practical Haskell code.

Architecting Query Compilers for Diverse Workloads

Ruby Tahboub, Purdue University

To leverage modern hardware platforms to their fullest, more and more database systems embrace compilation of query plans to native code. In the research community, there is an ongoing debate about the best way to architect such query compilers. This is perceived to be a difficult task, requiring techniques fundamentally different from traditional interpreted query execution.In this talk, I will draw attention to an old but underappreciated idea known as Futamura projections, which fundamentally link interpreters and compilers. Guided by this idea, realizing efficient query compilation can actually be very simple, using techniques that are no more difficult than writing a query interpreter in a high-level language. To support compiling relational workloads, I will demonstrate the LB2 query compiler implemented in this generative style that is competitive with the best compiled query engines both in sequential and parallel execution on the standard TPC-H benchmark.

Furthermore, several spatial and graph engines are implemented as extensions to relational query engines to leverage optimized memory, storage, and evaluation. Still, the performance of these extensions is often stymied by the interpretive nature of the underlying data management, generic data structures, and the need to execute domain-specific external libraries. On that basis, compiling spatial and graph queries to native code is a desirable avenue to mitigate existing limitations and improve performance. To support compiling spatial and graph workloads, I will demonstrate two extensions: LB2-Spatial and LB2-Graph that extend LB2 with spatial indexing structures, graph adjacency structures, and operators. The performance of LB2-Spatial and LB2-graph matches, and sometimes outperforms, low-level graph engines.

Programming with Rational Coinductive Streams

Jean-Baptiste Jeannin, University of Michigan

Some ML-family languages such as OCaml allow the definition of coinductive types as well as their inhabitants using a let rec construct. An example of such elements is coinductive streams. However, there is very little that one can do to manipulate them: pattern matching on the top elements is possible, but recursion will never finish. More importantly, it is virtually impossible to generate coinductive elements on the fly. Recent work with the CoCaml language has started fixing this issue, but it is limited to regular coinductive types, that is where the elements eventually point to themselves. For coinductive streams, this corresponds to streams that have a pattern that eventually repeats (e.g., [3;4;5;1;2;1;2;1;2]. In this talk we will show initial work on how to build on well-established theory on rational streams – a much more comprehensive family of streams – to extend CoCaml to deal with those rational streams.

Space-Efficient Monotonic References

Deyaa Almahallawi, Indiana University

Integrating static typing and dynamic typing has been popular in academia and industry. Gradual typing is one approach to this integration that preserves type soundness by casting values at runtime. For higher order values such as functions and references, a cast typically wraps them in proxy that performs casts at use sites. This approach suffers from two problems: (1) chains of proxies can grow and consume unbounded space, and (2) statically typed code regions need to check whether the value being used is proxied. Monotonic references [Siek et al. 2015c] solve the later problem for references by directly casting the heap cell instead of wrapping the reference in a proxy. In this talk we show that monotonic references can also solve the former problem. We present a space-efficient version of the semantics for monotonic references and prove an upper bound on space overhead.

Bunched Separation Polymorphism

Apoorv Ingle, University of Kansas

The logic of bunched implications (BI) is widely used in program logics for heap manipulation, and applicable to other resource-centric program models. However, a Curry-Howard interpretation of BI, capturing correct resource usage in typing, remains an open problem. In this talk, I will describe a type system built on bunched implications, and show how it models resources as first class citizens. In particular, our language incorporates polymorphism over types, as usual, but also over degrees of separation between expressions.

Recovering Purity with Comonads and Capabilities

Vikraman Choudhury, Indiana University

We take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to extend it to permit capturing pure expressions with types. Our key observation is that, just as the pure simply-typed lambda calculus can be extended to support effects with a monadic type discipline, an impure typed lambda calculus can be extended to support purity with a comonadic type discipline. We establish the correctness of our type system via a simple denotational model, which we call the capability space model. Our model formalizes the intuition common to systems programmers that the ability to perform effects should be controlled via access to a permission or capability, and that a program is capability-safe if it performs no effects that it does not have a runtime capability for. We then identify the axiomatic categorical structure that the capability space model validates, and use these axioms to give a categorical semantics for our comonadic type system. We then give an equational theory (substitution and the call-by-value β and η laws) for the imperative lambda calculus, and show its soundness relative to this semantics. Finally, we give a translation of the pure simply-typed lambda calculus into our comonadic imperative calculus, and show that any two terms which are βη-equal in the STLC are equal in the equational theory of the comonadic calculus, establishing that pure programs can be mapped in an equation-preserving way into our imperative calculus.

Formal Verification of a Finite Difference Scheme

Mohit Tekriwal, University of Michigan

Natural and physical systems are typically modeled by differential equations, which are often difficult to solve analytically. The current state-of-the-art is to perform numerical simulations of those differential equations to get numerical approximate solutions, using techniques such as finite differences or finite elements. The results of those simulations are used to perform critical engineering tasks, such as design of aircraft wings, engine internal components, or nuclear power plants. It is thus important to have a high degree of confidence in the results of the simulations and ensure that they are not producing erroneous solutions. Today this is typically achieved using two heuristics: comparing the results with known analytical solutions or experimental results, and looking at the numerical rate of convergence of the simulation. In contrast and to enhance the confidence in the results of simulations, we propose the use of formal verification techniques, and we perform the formal verification in the Coq proof assistant of the consistency of a numerical second-order finite difference scheme. This provides a much higher-level of guarantee that the simulation produces accurate results.

In a finite difference scheme, differential equations are expressed in terms of function values in a discretized space. Computing solutions to these discretized equations involves matrix operations like inversion and multiplication, which are vulnerable to floating point errors and might lead to numerical instability. The challenge here is to ensure that the computed solution matches the true solution. To achieve this, a numerical scheme has to go through three basic checks: Consistency, Stability and Convergence. While the consistency property ensures how close the discretized differential equation is to the actual differential equation, the convergence property ensures how close the computed solution is to the true solution, in the limit that the discretization interval is infinitesimally small. All three properties are related to each other by the widely used Lax-Richtmyer Equivalence Theorem which states that a numerical scheme is convergent if it is consistent and stable.

We use the Coq proof assistant to formally verify the consistency of a second-order accurate finite difference discretization on a uniform grid of spacing dx. This scheme can be obtained by Taylor expansion of the numerical solution at the grid nodes in the limit of infinite resolution, and we formally prove the order of accuracy of the numerical scheme. A challenge has been to use and adapt existing Coq library proofs of the Taylor-Lagrange theorem to prove that the remainder is O(dx^2). The approach is general and can be applied to perform consistency proofs on any finite difference schemes

Proving Robustness to Training Set Poisoning Attacks

Samuel Drews, University of Wisconsin

The intersection of security and machine learning highlights the potential for adversarial attacks at each stage of the machine-learning pipeline. One such problem concerns the power that an adversary could have by altering (or "poisoning") the training data so that the resultant learned model exhibits some undesired behavior. The efficacy of such poisoning attacks has been studied in, for example, linear classifiers, where results are heavily reliant on the somewhat continuous nature of the learner. Decision tree learning, however, is less well-behaved, as a small change to the training set can cause different predicates to be chosen at early stages, and it is difficult to reason about how this could affect the selection of predicates for subsequent nodes during the remainder of training. In this work, I propose leveraging abstract interpretation to analyze the following: for a fixed training set T and test input x, if an attacker is allowed to remove up to n-many elements from T (resulting in T'), what are the possible results of learning a new decision tree on T' and subsequently classifying x? The composition of decision-tree learning on T and classification of x can be succinctly represented, as it corresponds to learning the single path that x follows through the tree (instead of the entire tree model)--In fact, by constructing a domain-specific language in which a simple form of the tree-learning-classification composition can be written, and by constructing a suitable abstract domain for representing many possible training sets, preliminary experiments are able to formally prove the robustness property for shallow trees learned from the MNIST dataset.

Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems

Qinheping Hu, University of Wisconsin

Program synthesis is the classic problem of automatically finding a program implementation in some search space that satisfies a given correctness specification. However, it is usually not enough to produce any correct solution. For program synthesis problems with multiple potential correct solutions in the search space, synthesizers are unpredictable–users have no way to prefer one correct solution over others. Thus, sometimes synthesizers may produce a correct but unusable solution, for example, the size of the solution is too large to be read. Besides, on problems with infinite search space containing no correct solution, enumeration-based synthesizers will timeout to exhaust the search space. That is, when a solver timeouts, users won't know whether the solving is not finished within the time limit, or the given synthesis problem is unrealizable–no solution in the search space satisfies the correctness specification.

In this talk, we introduce two types of guarantees in program synthesis: 1) quantitative objectives with which users can prefer one solution than others, and 2) the abilities to prove unrealizability which allow users to learn more about unrealizable problems instead of timeout. We first show how to introduce quantitative syntactic objectives into syntax guided synthesis (SyGuS) by extending the grammar in SyGuS to weighted grammar, and then show how to prove unrealizability for SyGuS by reducing synthesis problems to reachability problems.

Coming Soon!

More information will be available shortly.