ROSE is a Yale Computer Science laboratory that focuses on using formal methods to improve software reliability. In particular, we are now working on functional reactive synthesis, symbolic execution engine for Haskell, and verification of configuration files.


Lazy counterfactual symbolic execution

G2 is a symbolic execution engine for Haskell, a non-strict, functional programming language.

Learn More
Temporal Stream Logic

A new temporal logic that separates control and data, which provides an attractive trade-off for synthesis

Learn More
Verifications for Configuration Files

A tool that can automatically detect complex configuration errors involving multiple configuration options.

Learn More


December 21, 2019
Programming-by-example (PBE) is a synthesis paradigm that allows users to generate functions by simply providing input- output examples. While a promising interaction...
August 9, 2019
Ruzica Piskac, recently appointed as the Donna L. Dubinsky Associate Professor of Computer Science , focuses her research on programming languages, software verification,...
July 5, 2019
Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP...
June 21, 2019
Reactive systems that operate in environments with complex data, such as mobile apps or embedded controllers with many sensors, are difficult to synthesize. Synthesis tools...
June 19, 2019
We present counterfactual symbolic execution, a new approach that produces counterexamples that localize the causes of failure of static verification. First, we develop a...
May 2, 2019
Congratulations to Professor Ruzica Piskac as the recipient of the 2019 Ackerman Teaching and Mentoring Award. This award, sponsored by SEAS alum Robert Ackerman (‘60),...