A Type-based Framework for Automatic Debugging.
Ozan Hafizogullari, Christoph Kreitz.
Technical Report, Cornell University, Ithaca, NY, September 1998.
Abstract
	We present a system for automatic debugging in typed functional languages. The system checks program properties specified by a user and finds bugs as well as conditions necessary to avoid them. It applies type-checking techniques built on top of the existing type system of the programming language. Its type system is based on the notion of set types, extended through type constructors, polymorphism and dependent types. Subtyping is used to allow finer specification. Type checking is achieved by collecting flow information through flow types and constraints on them. By solving the constraints we obtain instances for flow type variables and a set of conditions that make the typing provable. These conditions are converted into arithmetical formulae that can be checked by a common decision procedure. Our approach has a modular structure and can also be used for array bounds checking and other program analysis problems.

			Back to overview of papers
Bibtex Entry
	@TechReport{tr:HafizogullariKreitz98b, author = "Ozan Haf{\i}zo\~{g}ullar{\i} and Christoph Kreitz", title = "A Type-based Framework for Automatic Debugging", institution = "Cornell University. Department of Computer Science", year = "1998" }