Axiom-based property verification for P4 programs
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 understan...
Elmentve itt :
| Szerzők: | |
|---|---|
| Testületi szerző: | |
| Dokumentumtípus: | Könyv része |
| Megjelent: |
2018
|
| Sorozat: | Conference of PhD Students in Computer Science
11 |
| Kulcsszavak: | P4 - programozási nyelv, Programozás, Számítástechnika |
| Online Access: | http://acta.bibl.u-szeged.hu/61771 |
| Tartalmi kivonat: | 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. |
|---|---|
| Terjedelem/Fizikai jellemzők: | 80-83 |