First, I present Wys*, a new SMC domain-specific language hosted in F*, a verification-oriented programming language developed at Microsoft Research. Wys* allows programmers to program rich, reactive SMC applications as if they were regular, single-threaded F* programs, and execute them using a low-level distributed semantics. The single-threaded semantics enables programmers to seamlessly use F*'s logic for verifying the correctness and security properties of their SMC programs. We have formally proved (again, using F*) that the properties verified for the Wys* source programs carry over when the programs are run using the low-level semantics. We have programmed and verified several SMC applications in Wys*, including a novel card dealing application.
Bio: Aseem Rastogi is a PhD candidate in the Computer Science Department at the University of Maryland, College Park. His research applies formal methods in programming languages to design abstractions that simplify the task of programming software systems, and enable programmers to state and enforce crucial invariants such as those related to the correctness and security of the software. Before joining the University of Maryland, Aseem obtained an MS in Computer Science from the State University of New York at Stony Brook.