Miyaji Laboratory

Abstract

Today, research is being conducted on methods for verifying software to ensure that network functions operate safely according to specifications. Arseniy Zaostrovnykh and colleagues have proposed a method [1] for verifying C language software using Lazy Proofs. In this paper, we propose a method of verifying C language software by using F* language with a different approach. In addition, this method is simpler than existing methods because it does not use complicated proof combinations.