[PRL] SafeJava

Mitchell Wand wand at ccs.neu.edu
Fri Dec 12 16:26:38 EST 2003


------- start of forwarded message (RFC 934 encapsulation) -------
Sender: seminars-bounces at lists.csail.mit.edu
To: <seminars at csail.mit.edu>
Date: Fri, 12 Dec 2003 16:18:47 -0500

An Invitation to Attend A PhD Thesis Defense by Chandrasekhar Boyapati

SafeJava: A Unified Type System for Safe Programming
                              
Tuesday, December 23, 2003

10:00 AM

(refreshments & snacks)
MIT Computer Science and Artificial Intelligence Lab (CSAIL)
200 Tech Square, NE 43 - RM Room 518

Making software reliable is one of the most important technological
challenges facing our society today.

This thesis presents a new type system that addresses this problem by
statically preventing several important classes of programming errors.
If a program type checks, we guarantee at compile time that the program
does not contain any of those errors.

We designed our type system in the context of a Java-like
object-oriented language; we call the resulting system SafeJava.  The
SafeJava type system offers significant software engineering benefits.
Specifically, it provides a statically enforceable way of specifying
object encapsulation and enables local reasoning about program
correctness; it combines effects clauses with encapsulation to enable
modular checking of methods in the presence of subtyping; it statically
prevents data races and deadlocks in multithreaded programs, which are
known to be some of the most difficult programming errors to detect,
reproduce, and eliminate; it enables software upgrades in persistent
object stores to be defined modularly and implemented efficiently; it
statically ensures memory safety in programs that manage their own
memory using regions; and it also statically ensures that real-time
threads in real-time programs are not interrupted for unbounded amounts
of time because of garbage collection pauses.  Moreover, SafeJava
provides all the above benefits in a common unified type system
framework, indicating that seemingly different problems such as
encapsulation, synchronization issues, software upgrades, and memory
management have much in common.

We have implemented several Java programs in SafeJava.  Our experience
shows that SafeJava is sufficiently expressive to support common
programming patterns, its type checking is fast and scalable, and it
requires little programming overhead.  In addition, the type
declarations in SafeJava programs serve as documentation that lives with
the code, and is checked throughout the evolution of code.  The SafeJava
type system thus has significant software engineering benefits and it
offers a promising approach for improving software reliability.

------- end -------


More information about the PRL mailing list