Research Projects

Symbolic Execution Engine for Haskell

G2 is a symbolic execution engine for Haskell, a non-strict, functional programming language.  Symbolic execution is a technique that runs a program with symbolic variables as inputs, and gives output in terms of expressions and constraints involving those symbolic variables.  By using SMT solvers to solve the constraints, G2 can find concrete inputs to Haskell programs that satisfy assumptions or violate assertions.

G2 has been applied to generate concrete and counterfactual counterexamples for errors from the LiquidHaskell modular verification tool.  Concrete counterexamples identify actual errors in the users code, while counterfactual counterexamples identify output specifications that must be strengthened to enable verification.

Recent Publications:

William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala and Ruzica Piskac.

Lazy counterfactual symbolic execution.

In Proceedings of the 40th ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA,
June 22-26, 2019., 2019.

bib | DOI | http ]

Functional Reactive Synthesis

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 usually fail for such systems because the state space resulting from the discretization of the data is too large.  
 
In this project, we have introduced Temporal Stream Logic (TSL), a new temporal logic that separates control and data. TSL provides an attractive trade-off for synthesis. On the one hand, synthesis from TSL, unlike synthesis from standard temporal logics, is undecidable in general. On the other hand, however, synthesis from TSL is scalable, because it is independent of the complexity of the handled data. Some of the application domains to which we have successfully used TSL for synthesis include:
- a music player Android app
- a controller for an autonomous vehicle in the Open Race Car Simulator (TORCS)
- a hardware implementation of a kitchen timer
 
Recent Publications:

Mark Santolucito, William T. Hallahan, and Ruzica Piskac.

Live programming by example.

In Extended Abstracts of the 2019 CHI Conference on Human
Factors in Computing Systems, CHI 2019, Glasgow, Scotland, UK, May 04-09,
2019., 2019.

bib | DOI | http ]

Verifications for Configuration Files

Modern verification technologies inherently depend on the availability of formal specifications, yet they are extremely labor intensive to create and maintain. This is especially the case for configuration files, which rarely have any documentation, even in written English form. Configurations are the values of system parameter settings; Incorrect configurations often lead to system misbehaviours such as exceptions, error code return, crashing or even core dump. 

 

We have developed ConfigV, which is the first tool that can automatically detect complex errors involving multiple variables, and learn over a training set of partially incorrect configuration files. Since configuration files lack helpful semantic information to infer types, we use a probabilistic inference method to learn likely types for keywords based on their values from the training set. We combined this new type of information with a generalization of association rule learning that handles not just association rules, but arbitrary, typed predicates. We evaluated ConfigV by verifying public configuration files on GitHub, and we showed that ConfigV can successfully detect configuration errors in these files. 

 

Recent Publications:

Mark Santolucito, Ennan Zhai, Rahul Dhodapkar, Aaron Shim, and Ruzica Piskac.

Synthesizing configuration file specifications with association rule

learning.

PACMPL, 1(OOPSLA):64:1–64:20, 2017.

bib | DOI | http ]