- Ph.D. Student (5th year)
- Cornell University, Computer Science
- Advisor: Joseph Halpern
- Knowledge-based synthesis of distributed systems using event structures by Mark Bickford, Robert C. Constable, Joseph Halpern, Sabina Petride
- We show how to extend the mechanism of extracting a program that satisfies a specification from a
a proof that the specification is satisfiable to account for epistemic specifications and programs with
knowledge tests. As an application, extraction of a knowledge-based program and a standard program
(essentially Stenning's protocol) that solve the sequence
transmission problem is carried out in the Nuprl system.
- in 11th International Conference on Logic for Programming,
Artificial Intelligence and Reasoning (LPAR 2004)
project site
- in 11th International Conference on Logic for Programming,
Artificial Intelligence and Reasoning (LPAR 2004)
- Expressing security properties using selective interleaving functions by Joseph Halpern and Sabina Petride
- We make the observation that nondeducibility on strategies (NOS) cannot be expressed as closure under a certain type or set of interleaving functions, in the terminology of McLean. A natural extension of the selective interleaving functions framework is proposed and shown to capture NOS.
- Knowledge-based synthesis of distributed systems using event structures LPAR 04 (previous version as a PRL seminar, Cornell University)
- Noninterference and selective interleaving functions FOSAD '02 student presentation
- A knowledge-based analysis of global function computation by Joseph Halpern and Sabina Petride (Feb. 2005)
- We give a general characterization of networks on which a global function is computable, taking into account agents' knowledge about the network. This characterization proves useful in explaining why a simple flooding protocol solves the global function computation whenever possible. An improved version of this protocol, in which agents act based on what they know and send only messages they believe are necessary to be sent is derived. This counterfactual-belief based program still solves global computation whenever possible and is implemented by a number of known leader election algorithms, most notably Peterson's algorithm.
- Secrecy in multiagent systems under symbolic cryptography by Sabina Petride and Riccardo Pucella (Feb. 2005)
- We consider a setting in which agents use observational algorithms to distinguish the possible states of the system. By adjusting both the kind of observations and the capabilities of the adversaries, we capture in a natural way both secrecy in the presence of Dolev-Yao adversaries and lack of information flow in the presence of perfect encryption.
I am currently working on verification of timing-based protocols in the Nuprl system. I am interested in finding good abstractions of such protocols (such as knowledge-based programs) that are easier to verify. Once an abstract program is proven correct, all its implementations are automatically correct; this means that no separate proofs of correctness are needed.
- A review of Concurrent and Real-time Systems: The CSP Approach by Steve Schneider (SIGACT News, 2004)
Recently taught CS214 Advanced UNIX