11–13 of 13 posts
Earlier quoted context omitted.
Just saying, on your website, the trasparent buttons on the top right really do not mesh well with the background, once you scroll down.
Yeah I know, been focussing only on client projects but luckily we finally got someone to rebuild the frontend.
Application of formal methods is always an interesting read, and this article is a gentle introduction to some of the ideas exploited in probabilistic model checking. However to me, the way the article is written, gives software verification, and CBMC in particular, an unnecessary bad reputation. > There is no need to define “game progress” or implement a naive game AI, as formal verification methods appear to requir…
I didn’t read this so much as a critique of formal program analysis so much as a good excuse to talk about an interesting CS use case for linear algebra.
> The mathematical method described here has a number of advantages over formal verification, including reduced code size and complexity.
My comment was intended to stress that the authors achieved different things. This article proved that the game design is sound, i.e. verification at model-level, while the original one proved that the implementation cannot reach certain undesired states. Both are perfectly reasonable, justifiable and necessary.
Earlier quoted context omitted.
More precisely, construct a graph with vertices (u, v) where u is a prior state and v a possible successor state, then there must not be a node of out-degree zero unless it is an end state. As far as complexity goes, this should be linear in number of vertices. In fact, you don't even really have to construct the graph, just count out degree.
That is not enough, since you may still get stuck in a loop.