7 ms·

There is no algorithm in the world for how to check whether a video codec is working correctly or not

• afiori 5y ago
  The model checking would not check the output but the trace of operations. It might prove that all bytes of the output were written to at least once, that dereferenced pointers point toward either the input or some other valid structure, and other properties like this.