You are viewing a single comment's thread from:
RE: Tauchain Update: Significant code changes in Github and discussion of progress
I was reading about TML and wondering what are the plans for verification. Curious and it will be helpful if you can share your thoughts.
If you mean formal verification this is covered by the "model checking" capacity of BDD.
References
By formal verification I meant "program verification"
Quoting the paper below, "the runtime safety and the functional correctnes"
https://www.cs.umd.edu/~aseem/solidetherplas.pdf
Right, that will be a result of BDD as I said in my response. Model checking performs formal verification in a process outlined below which I will discuss:
So what we have to understand is every program or software can be thought of as a state machine. There can be said that there are software which has a finite amount of possible states (iterations/combinations/permutations) or an infinite (unknown amount or uncountable is more likely) of possible states. If we are dealing with software which has a finite amount of possible states then it becomes possible to verify that program by simply doing an exhaustive search of the entire map of possible states the program can take in the design. Think of it like the ability to simply play through all possible levels in a game in all possible ways during the design of the game so that when the code is created it's impossible to violate the hard rules such as the laws of physics.
So the answer is yes you get formal verification as an aspect of model checking in Tauchain. In specific the BDD data structure allows for efficient model checking.
https://www.cs.cmu.edu/~aldrich/courses/654-sp05/handouts/model-checking-3.pdf
https://en.wikipedia.org/wiki/Finite-state_machine
http://wiki.c2.com/?InfiniteStateMachine
Thank you - I will revert after having bit more understanding.