Existing approaches for detecting type errors in unsafe languages are limited. Static analysis methods are imprecise, and often require source-level changes, while most dynamic methods check only memory properties (bounds, liveness, etc.), owing to a lack of run-time type information. This paper describes libcrunch, a system for binary-compatible run-time type checking of unmodified unsafe code, currently focusing on C. Practical experience shows that our prototype implementation is easily applicable to many real codebases without source-level modification, correctly flags programmer errors with a very low rate of false positives, offers a very low run-time overhead, and covers classes of error caught by no previously existing tool.
I did my Bachelor’s and PhD degrees at the University of Cambridge. My initial research background was in operating systems, hypervisors and the like, with a little networking and distributed systems thrown in. Moving some way up the stack, my PhD work centred on the programmer-facing problem of building software by composition of ill-matched components, for which I developed the Cake language. From January 2011 until March 2012 I was a James Martin Fellow in the Department of Computer Science at the University of Oxford, mostly focused on program analysis and the problem of combining state-space methods (e.g. symbolic execution) with syntactic methods (e.g. type checking). From May 2012 to May 2013, I was a postdoctoral researcher at USI’s Faculty of Informatics in Lugano, Switzerland, working on programmer-facing dynamic analysis infrastructure for Java-like virtual machines. From May until October 2013 I was temporarily a Research Assistant at Oracle Labs, on the Alphabet Soup project, working on native object code and debugging support in the Truffle/SubstrateVM stack. Since 2013 I have been a Research Associate back at the University of Cambridge Computer Laboratory, working on various topics with robustness in low-level programming as a recurring theme. I have also worked (some time ago) for Opal Telecom and ARM, and (more recently) and as a consultant for Ellexus.
Fri 4 NovDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10 | Typing, in PracticeOOPSLA at Matterhorn 1 Chair(s): Sebastian Erdweg Delft University of Technology, Netherlands | ||
10:30 25mTalk | A Practical Framework for Type Inference Error Explanation OOPSLA Calvin Loncaric University of Washington, Satish Chandra Samsung Research America, Manu Sridharan Samsung Research America, Cole Schlesinger Samsung Research America DOI Pre-print Media Attached | ||
10:55 25mTalk | Dynamically Diagnosing Type Errors in Unsafe Code OOPSLA Stephen Kell University of Cambridge DOI Media Attached | ||
11:20 25mTalk | First-Class Effect Reflection for Effect-Guided Programming OOPSLA DOI | ||
11:45 25mTalk | Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers OOPSLA Link to publication DOI Pre-print |