4 papers
Solver-based Gradual Type Migration
Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg +1
Gradually typed languages allow programmers to mix statically and dynamically typed code, enabling them to incrementally reap the benefits of static typing as they add type annotat…
Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic
Eric Campbell, Michael Greenberg
Temporal logics over finite traces are not the same as temporal logics over potentially infinite traces. Roşu first proved completeness for linear temporal logic on finite traces (…
Formulog: Datalog for SMT-Based Static Analysis (Extended Version)
Aaron Bembenek, Michael Greenberg, Stephen Chong
Satisfiability modulo theories (SMT) solving has become a critical part of many static analyses, including symbolic execution, refinement type checking, and model checking. We prop…
Executable formal semantics for the POSIX shell
Michael Greenberg, Austin J. Blatt
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,…