Zero-Knowledge Model Checking

Pascal Berrang, Mirco Giacobbe, Jacob Swales +1

We introduce a technology to formally verify that a software system satisfies a temporal specification of functional correctness, without revealing the system itself. Our method co…