Andrew D. Gordon

Irene Vlassi Pandi, Earl T. Barr, Andrew D. Gordon et al.

We present a new approach to the type inference problem for dynamic languages. Our goal is to combine \emph{logical} constraints, that is, deterministic information from a type system, with \emph{natural} constraints, that is, uncertain statistical information about types learnt from sources like identifier names. To this end, we introduce a framework for probabilistic type inference that combines logic and learning: logical constraints on the types are extracted from the program, and deep learning is applied to predict types from surface-level code properties that are statistically associated. The foremost insight of our method is to constrain the predictions from the learning procedure to respect the logical constraints, which we achieve by relaxing the logical inference problem of type prediction into a continuous optimisation problem. We build a tool called OptTyper to predict missing types for TypeScript files. OptTyper combines a continuous interpretation of logical constraints derived by classical static analysis of TypeScript code, with natural constraints obtained from a deep learning model, which learns naming conventions for types from a large codebase. By evaluating OptTyper, we show that the combination of logical and natural constraints yields a large improvement in performance over either kind of information individually and achieves a 4% improvement over the state-of-the-art.

Judith Borghouts, Andrew D. Gordon, Advait Sarkar et al.

Spreadsheet users regularly deal with uncertainty in their data, for example due to errors and estimates. While an insight into data uncertainty can help in making better informed decisions, prior research suggests that people often use informal heuristics to reason with probabilities, which leads to incorrect conclusions. Moreover, people often ignore or simplify uncertainty. To understand how people currently encounter and deal with uncertainty in spreadsheets, we conducted an interview study with 11 spreadsheet users from a range of domains. We found that how people deal with uncertainty is influenced by the role the spreadsheet plays in people's work and the user's aims. Spreadsheets are used as a database, template, calculation tool, notepad and exploration tool. In doing so, participants' aims were to compute and compare different scenarios, understand something about the nature of the uncertainty in their situation, and translate the complexity of data uncertainty into simplified presentations to other people, usually decision-makers. Spreadsheets currently provide limited tools to support these aims, and participants had various workarounds.

François Dupressoir, Andrew D. Gordon, Jan Jürjens et al.

We describe how to verify security properties of C code for cryptographic protocols by using a general-purpose verifier. We prove security theorems in the symbolic model of cryptography. Our techniques include: use of ghost state to attach formal algebraic terms to concrete byte arrays and to detect collisions when two distinct terms map to the same byte array; decoration of a crypto API with contracts based on symbolic terms; and expression of the attacker model in terms of C programs. We rely on the general-purpose verifier VCC; we guide VCC to prove security simply by writing suitable header files and annotations in implementation files, rather than by changing VCC itself. We formalize the symbolic model in Coq in order to justify the addition of axioms to VCC.