Title: Micromodels of Software

Abstract: What kind of design representation is practical for software development?  I'll argue that what we need are "micromodels": tiny models that capture tricky aspects of a system. We have developed a language called Alloy that allows micromodels to be built easily and incrementally. Like the languages of model checkers, Alloy can be analyzed fully automatically. But unlike them, Alloy is declarative, so you can express abstract and partial properties very succinctly, and is based on relational logic, so you can easily describe complex state structures.

Biography: Daniel Jackson is the Ross Career Development Professor of Software Technology, and leads the Laboratory for Computer Science's Software Design Group. He received an MA from Oxford University (1984) in Physics, and his SM (1988) and PhD (1992) from MIT in Computer Science. He was Assistant Professor of Computer Science at Carnegie Mellon University (1992-1997), and has been Associate Professor at MIT (since 1997). He sits on the editorial board of ACM TOPLAS, ACM TOSEM and Springer Verlag's Software Tools for Technology Transfer, and has served on the programme committee of more than 20 international conferences, including FSE, ISSTA, OOPSLA and CAV. He has broad interests in several areas of software construction, including development methods, automatic analysis of designs and specifications, and reverse engineering of code.