Terrier: A real-time, embedded operating system using advanced types for safety - Matthew Danish, PhD Proposal

11:00 am on Monday, December 16, 2013
1:00 pm on Monday, December 16, 2013
MCS 137
Abstract: Advanced type systems for modern programming languages provide an alternative to hardware-based or run-time safety checks. ATS is a dependent and linearly-typed language that compiles to C code requiring no additional run-time support, making it suitable for low-level programming. ATS supports an incremental approach towards verification, giving the programmer the flexibility to decide the strength of desired theorems. Terrier is an embedded operating system with a new design that uses advanced types to safely deploy non-traditional, yet better-fitting, programming models for real-time applications. Terrier is intended to run on ARM processors, and integrates with the ATS programming language. One of the primary reasons for using ATS in Terrier is attainment of memory safety, but the language is powerful enough to specify and prove almost any property, given sufficient time and effort.