Bestavros – Computer Science

Azer Bestavros
best@bu.edu
Options: Volunteer Basis, Independent Funding Available, Potential for UROP Funding, Potential for Work-Study, Potential for Academic Credit

Modeling Language Translation
Expected number of students: 3-6
The BU ibench initiative has developed a modeling language, VML, which can be used to formally specify distributed systems. Students will build a translator from VML to one of three existing verification languages: Promela, Alloy, or PRISM. VML allows both imperative and declarative modeling. Promela is an imperative C-like language, Alloy is a purely declarative language based on constraints over sets and relations, and PRISM is an imperative, low-level language for constructing probabilistic state machines. Previous experience with compilers is useful, but not required.