Physical Sciences and Mathematics Commons^™

Resource Bound Guarantees Via Programming Languages, Michael J. Burrell

Electronic Thesis and Dissertation Repository

We present a programming language in which every well-typed program halts in time polynomial with respect to its input and, more importantly, in which upper bounds on resource requirements can be inferred with certainty. Ensuring that software meets its resource constraints is important in a number of domains, most prominently in hard real-time systems and safety critical systems where failing to meet its time constraints can result in catastrophic failure. The use of test- ing in ensuring resource constraints is of limited use since the testing of every input or environment is impossible in general. Static analysis, whether via the …