ISSTA 2025
Wed 25 - Sat 28 June 2025 Trondheim, Norway
co-located with FSE 2025

Program invariants, which are properties that hold at specific program locations, are important in formal program verification and analysis. Traditional invariant generation methods using dynamic and static analyses are abundant and powerful, supporting a wide range of applications. However, these tools often remain underutilized due to their complex command-line interfaces and the technical expertise required for usage.

To bridge the gap between research and practical application, we have developed DIG+, which integrates the DIG invariant generator and the CIVL symbolic execution tool using the Language Server Protocol (LSP) design used in modern IDEs, such as VS Code. DIG+ simplifies the process of invariant generation by automating setup tasks and providing an intuitive and familiar interface for developers in VS Code. This integration allows users to generate and check invariants directly within their favorite IDEs, enhancing accessibility and usability. We hope DIG+ will inspire researchers to develop similar IDE integration for their research tools, making them more attractive to end users.