MuVal

MuVal is a validity checker for $\mu$CLP, a fixpoint logic modulo theories.

What inputs are supported?

The following input formats are supported:

• C Integer
• Integer Transition Systems (ITS)
• T2
• $\mu$CLP

For which programming languages has it support?

MuVal supports C programs.

What properties can be verified?

MuVal supports (non-)termination verification and temporal verification (e.g., LTL, CTL, and modal $\mu$-calculus).

What are the tool’s main techniques for the supported (input, property) pairs?

CounterExample Guided Inductive Synthesis (CEGIS), template-based synthesis of inductive invariants, ranking functions, and Skolem functions, ...

What external tools are used? (e.g., compilers, SMT solvers)

• SAT solver: MiniSat
• SMT solver: Z3

What is the tool’s URL?

https://github.com/hiroshi-unno/coar

Example(s)

Example files are available from: https://github.com/hiroshi-unno/coar/tree/main/benchmarks

References

The following papers describe the technical details of MuVal:

1. Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen: Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification. Proc. ACM Program. Lang. 7(POPL): 2111-2140 (2023)
2. Satoshi Kura, Hiroshi Unno, Ichiro Hasuo: Decision Tree Learning in CEGIS-Based Termination Analysis. CAV (2) 2021: 75-98
3. Hiroshi Unno, Tachio Terauchi, Eric Koskinen: Constraint-Based Relational Verification. CAV (1) 2021: 742-766