About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
Computer Networks
Paper
Verification of protocols using symbolic execution
Abstract
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.