A Better SMT Language: Design & Tooling

Background

external page SMT-LIB is the standard input language for SMT (satisfiability modulo theories) solvers, which are the main reasoning engines used by various formal methods tools, in particular program verifiers such as those from the Viper verification infrastructure developed in our group.

Developers of such tools often need to understand and modify SMT-LIB files, e.g. to experiment with SMT encodings. This task, however, is complicated in three major ways:

1. SMT-LIB's syntax, a fully parenthesized prefix notation similar to Lisp, impedes focusing on the logical assertions an SMT-LIB program corresponds to.
2. SMT-LIB, as a language of first-order logic, requires encoding foundational aspects of programming languages, in particular data flow properties such as whether a variable is read or written.
3. Domain-specific knowledge about the tool that generated the SMT encoding is typically needed for understanding the encoding, but is usually obscured, or even completely lost.

Project

This project, carried out in the context of Viper, aims at designing an alternative syntax for SMT encodings that mitigates aforementioned problems; implementing high-performance parsers and pretty-printers for working with the new syntax that can handle SMT encodings up to millions of lines of code; and investigating domain-specific analysis tools for SMT encodings created by Viper.

Potential Project Goals

• Identify the SMT encoding features Viper requires, and design a more convenient source syntax for them. Inspiration can be drawn from existing, related languages such as Viper itself, external page Boogie and external page Dafny.
• Investigate possible implementations for parsers and pretty-printers that deliver high performance and can be integrated into external page VSCode. Promising candidates are Rust and C++, since both aim for performance, allow reusing existing SMT-LIB parsers, and can be compiled to WebAssembly.
• Implement a high-performance parser and pretty-printer for the new language (and for SMT-LIB, if necessary)
• Enable users to customise the textual representation: e.g. by representing a nested function application combine(t1, combine(t2, t3)) as combine(t1, t2, t3), [t1, t2, t3] or t1 🞼 t2 🞼 t3.
• Develop a simple VSCode plugin: syntax highlighting, converting from/to SMT-LIB, and invoking the external page Z3 SMT solver.
• Extend the plugin with useful analysis features, such as visualising data flow implicitly encoded in an SMT program.

Opportunities

• Gain experience with developing programming language tools
• Learn about SMT encodings
• Contribute to a state-of-the-art, open-source verification infrastructure
• Collaborate within a team of researchers on a current research project

Contact