Verification of protocols using symbolic execution

A protocol verifier using symbolic execution has been designed and implemented as part of a general verifier (oriented towards microcode). This part describes how this method works for communication protocols involving timing assumptions, state changes depending on message contents, unreliable medium, an arbitrary number of communicating processes, etc. The method can detect design errors such as deadlock and tempo-blocking; in addition the user can add his own assertions to express other desired properties. © 1978.