Automated Verification of RPC Stub Code

Select |


Fernandez, Matthew; Andronick, June; Klein, Gerwin; Kuz, Ihor

Fernandez, Matthew; Andronick, June; Klein, Gerwin; Kuz, Ihor


Conference Material

International Symposium on Formal Methods

Oslo, Norway


Formal verification has been successfully applied to provide strong correctness guarantees of software systems, but its application to large code bases remains an open challenge. The technique of component-based software devel- opment, traditionally employed for engineering benefit, also aids reasoning about such systems. While there exist compositional verification techniques that lever- age the separation implied by a component system architecture, they implicitly rely on the component platform correctly implementing the isolation and com- position semantics they assume. Any property proven using these techniques is vulnerable to being invalidated by a bug in the code of the platform itself. In this paper, we show how this assumption can be eliminated by automatically gener- ating machine-checked proofs of the correctness of a component platform’s gen- erated Remote Procedure Call (RPC) code. We demonstrate how these generated proofs can be composed with hand-written proofs to yield a system-level property with equivalent assurance to an entirely hand-written proof. This technique forms the basis of a scalable approach to formal verification of large software systems.


Fernandez, Matthew; Andronick, June; Klein, Gerwin; Kuz, Ihor. Automated Verification of RPC Stub Code. In: International Symposium on Formal Methods; Oslo, Norway. 2015-06-20. 273-290.

Loading citation data...

Citation counts
(Requires subscription to view)