Version 0.6.0 has been yanked.
Today, I have a quick update with some good news and some slightly worse news.
The good news is that I have started working at the Chair of Computer Architecture at the University of Freiburg! There is a lot of interesting things to be done.
The bad news is that I rushed the release of version 0.6.0 and didn't thoroughly test and bomb-proof it. Since then, I found that
- the chapter on μ-calculus verification featured a wrong translation of LTL property FG to μ-calculus,
- some μ-calculus properties panicked during double-checking between the incremental and fresh computations of the same property at the end of verification.
While the panics prevented the verification issues from breaking soundness (as in, a panic does not give a valid result, so the result cannot be wrong), I also found a corner case during bug-fixing where soundness could potentially be impacted without triggering a panic. Due to this, I yanked the version 0.6.0.
In the new version 0.6.1, I fixed the bugs and also added more safeguards. The examples from the book, as well as additional examples, are now a part of the test suite of machine-check. The incremental μ-calculus verification is now not just double-checked, but triple-checked: a separate non-incremental algorithm for μ-calculus computation is now used to further ensure that the result is correct (panicking if it is not). Fortunately, the impact on verification time seems to be negligible as the main expensive part of verification is computing the refinements.
You can ensure that version 0.6.1 is used by editing your Cargo.toml:
[dependencies]
machine-check = "0.6.1"
Until next time.