G2 is a symbolic execution engine for Haskell, a non-strict, functional programming language.
Learn More
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.
A new temporal logic that separates control and data, which provides an attractive trade-off for synthesis
Learn More
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
A tool that can automatically detect complex configuration errors involving multiple configuration options.
Learn More
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.
