Colloquium 9/16 - Michael Greenberg, Stevens Institute of Technology

Computer Science Colloquium

Friday, September 23

2:35pm in Wege Auditorium


Formal Support for the POSIX Shell

The POSIX shell is a widely deployed, powerful tool for managing computer systems. The shell is the expert’s control panel, a necessary tool for configuring, compiling, installing, maintaining, and deploying systems. Even though it is powerful, critical infrastructure, the POSIX shell is maligned and misunderstood. Its power and its subtlety make for a dangerous combination.

How can we support the POSIX shell? I’ll describe two recent lines of work—Smoosh, a formal, mechanized, executable small-step semantics for the POSIX shell—and ffs—a tool for helping users manipulate semi-structured data (like JSON and YAML) in the shell.

Michael Greenberg is an assistant professor at Stevens Institute of Technology. He received BAs in Computer Science and Egyptology from Brown University (2007) and his PhD in Computer Science from the University of Pennsylvania (2013); previously, he was an assistant professor at Pomona College. His work has ranged from functional-reactive JavaScript (with Shriram Krishnamurthi at Brown) to runtime verification of higher-order programs (with Benjamin Pierce at Penn) to software-defined networking (with Dave Walker at Princeton) to present activities focused on the POSIX shell and executable formalism.