Axiom-based property verification for P4 programs

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

[img] 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.

Item Type: Article
Journal or Publication Title: Conference of PhD Students in Computer Science
Date: 2018
Volume: 11
Page Range: pp. 80-83
Event Title: Conference of PhD students in computer science (11.) (2018) (Szeged)
Uncontrolled Keywords: P4 - programozási nyelv, Programozás, Számítástechnika
Additional Information: Bibliogr.: 83. p. ; összefoglalás angol nyelven
Date Deposited: 2019. Nov. 04. 09:43
Last Modified: 2019. Nov. 04. 09:43
URI: http://acta.bibl.u-szeged.hu/id/eprint/61771

Actions (login required)

View Item View Item