Axiom-based property verification for P4 programs

Tóth, Gabriella and Tejfel, Máté: Axiom-based property verification for P4 programs. Conference of PhD Students in Computer Science, (11). pp. 80-83. (2018)

Cikk, tanulmány, mű cscs_2018_093-096.pdf Download (206kB)

Abstract

We produce an axiom-based program properties verification method for P4 programs. P4 is a special, domain specific, declarative programming language to develop network packet forwarding. P4 is quite new, and different from general-purpose programming languages so it is an important idea to understand its behavior and to verify it. The operational semantics of P4 is reachable in K framework, so there is an opportunity to do its verification based on its operational semantics, but it is a low level solution, therefore the proof of complex properties can be too difficult and costly. So we would like to verify the program in a higher abstraction level, in which we would introduce axioms, which are correct in the operational semantics. Using these axioms we can create easier and more transparent proof.

Actions (login required)

View Item