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.
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.
Functional Reactive Synthesis
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,
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.
Mark Santolucito, Ennan Zhai, Rahul Dhodapkar, Aaron Shim, and Ruzica Piskac.
Synthesizing configuration file specifications with association rule
PACMPL, 1(OOPSLA):64:1–64:20, 2017.