Library
home (Home) TU Delft Repository login Login

LTL-based Specifications for P4 Program Synthesis

Conference Paper (2025)
Author(s)

Lorenzo Theunissen (TU Delft - Electrical Engineering, Mathematics and Computer Science)

Sebastijan Dumančić (TU Delft - Electrical Engineering, Mathematics and Computer Science)

Fernando Kuipers (TU Delft - Electrical Engineering, Mathematics and Computer Science)

Research Group
Networked Systems
DOI related publication
https://doi.org/10.1145/3750022.3750456 Final published version
More Info
expand_more
Publication Year
2025
Language
English
Research Group
Networked Systems
Pages (from-to)
7-12
Publisher
ACM
ISBN (electronic)
979-8-4007-2103-8
Event
2nd Workshop on Formal Methods Aided Network Operation, FMANO 2025, Part of SIGCOMM 2025 (2025-09-08 - 2025-09-08), Coimbra, Portugal
Downloads counter
98
Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Abstract

Programmable networks enable us to define the behaviour of a network through software. This added freedom comes with added complexity because multiple switches need to coordinate and be programmed correctly. To ease this task, we focus on intent-based networking via program synthesis. In this paper, we explain how to leverage linear temporal logic to describe the desired behaviour of a program, how to verify a P4 program against that description, and how to use the formula describing the program's behaviour to reduce the search space of the program synthesiser.