Bringing Invariant Analysis to modern IDEs: The DIG+ Extension for VS Code

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.