People
Faculty Members
|
Riccardo Pucella |
|
Professor Pucella's research revolves around the study of formal models and logics to reason about properties of software and systems. Formal models are used to understand what is meant by assertions such as "this piece of software or this system is correct." Logics are used to prove formally that a piece of software or system is indeed correct within the formal model under consideration.
Professor Pucella's recent research focus is on advanced type systems for statically enforcing properties of programs, including probabilistic properties and resource-usage properties. Past projects include: (1) the development of a formal model for understanding a computer defense technique known as obfuscation that allows a cluster of machines to implement a fault-tolerant service in such as a way that not all the machines are vulnerable to the same attacks from malicious attackers, and (2) the development of a type system for a programming language that lets a programmer express very precise behavioral properties of programs written in the language, including role-based access control properties.
Professor Pucella earned his BSc in Mathematics and MSc in Computer Science at McGill University in Montreal, after which he joined Bell Labs to work on the SML/NJ compiler. He completed a PhD in Computer Science at Cornell University, working with Joe Halpern and later Fred Schneider on foundations of security, uncertainty in AI, programming language semantics, and type systems. He also spent some time as a visiting researcher at Microsoft Research in Cambridge, UK. He is a member of the PRL group and the Institute for Information Assurance at Northeastern University.