AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo
This tool addresses debugging and interaction challenges for users and developers of SMT solvers, though it is incremental as it builds on existing solver technology.
The authors tackled the problem of SMT solvers failing to terminate or taking too long by developing AltGr-Ergo, an interactive graphical interface for Alt-Ergo that provides real-time feedback and manipulation options to help users guide the solver, as demonstrated through usage scenarios.
Due to undecidability and complexity of first-order logic, SMT solvers may not terminate on some problems or require a very long time. When this happens, one would like to find the reasons why the solver fails. To this end, we have designed AltGr-Ergo, an interactive graphical interface for the SMT solver Alt-Ergo which allows users and tool developers to help the solver finish some proofs. AltGr-Ergo gives real time feedback in order to evaluate and quantify progress made by the solver, and also offers various syntactic manipulation options to allow a finer grained interaction with Alt-Ergo. This paper describes these features and their implementation, and gives usage scenarios for most of them.