A coalgebraic decision procedure for NetKAT
- Submitting institution
-
University College London
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 14208
- Type
- E - Conference contribution
- DOI
-
10.1145/2676726.2677011
- Title of conference / published proceedings
- Conference Record of the Annual ACM Symposium on Principles of Programming Languages
- First page
- 343
- Volume
- 2015-January
- Issue
- -
- ISSN
- 0730-8566
- Open access status
- Out of scope for open access requirements
- Month of publication
- January
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
https://ndownloader.figstatic.com/files/7128245
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
4
- Research group(s)
-
-
- Citation count
- 26
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Provides the decision procedure for equivalence of NetKAT programs, which enables verification of important properties in networks, eg reachability. The equivalence method we proposed performed better than state of the art algorithms and has since been integrated in the Frenetic tool suite, used in practical network verification tasks. The research in this paper formed the basis of my ERC starting grant (1.5M euros). I gave a keynote on this topic at CONCUR 2015.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -