The goal of the Plato project is to develop software engineering tools and techniques that help modern programmers create more reliable and secure component software systems.  In order to accomplish our goal, we are developing a system of logical type refinements (LTR) that conservatively extend type systems for modern programming languages like Java, C# and ML.  

LTR guarantee properties of programs as they are written, linked together, executed and evolve through all aspects of the software lifecycle.  More specifically, we are developing LTR that allow programmers to specify a rich of collection of domain-specific invariants involving

• the contents of component data structures,
• the ordering and effect of operations specified in an interface,
• the safety of components acquired from different sources, and
• the distribution of data and computations over a network. 

LTR are specified in a concise notation familiar to programmers.  In addition, sophisticated refinement checking and refinement inference techniques allow programmers to minimize the number of annotations they need to put on their programs.  

Publications

Project Members

Faculty

David Walker

Graduate Students

Limin Jia

Alumni

Amal Ahmed

Yitzie Mandelbaum

Plato Walker, Philosopher Canine pub

External Collaborators

Robert Harper and Members of the Triple Project (CMU)

Secure Internet Programming Home