The DOI matches its Crossref record, with a small difference in title or year.
Network-Wide Configuration Synthesis
Overview
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
The most common sources of ambiguity witnesses are rule overlap and priority conflicts, where an operator's intent does not specify precedence even though the configuration must.
“In practice, the most common sources of such witnesses are rule overlap and priority conflicts, where an operator's intent does not specify precedence even though the configuration must [114], [17], [117].”
From Large language models for agentic NetOps and AIOps: Architectures, evaluation, and safety (2027) · cites this paper as [17]
Prior to the advent of LLMs, research approached configuration as a synthesis problem defined by explicit correctness criteria.
“Prior to the advent of LLMs, research approached configuration as a synthesis problem defined by explicit correctness criteria, which typically focused on translating high level policies into device-level configurations, ensuring invariants are maintained, and protocol semantics are respected [115], [116], [17], [117].”
From Large language models for agentic NetOps and AIOps: Architectures, evaluation, and safety (2027) · cites this paper as [17]
Advancement in the field has been limited by the reliance on proprietary incident corpora, heterogeneous telemetry infrastructures, and insufficiently robust ground truth.
“Advancement in the field has been limited by the reliance on proprietary incident corpora, heterogeneous telemetry infrastructures, and insufficiently robust ground truth [135], [18].”
From Large language models for agentic NetOps and AIOps: Architectures, evaluation, and safety (2027) · cites this paper as [135]
Citations
Cites
No references could be resolved yet.
Research works printed but not linked: 35
- Fogel, A., Fung, S., Pedrosa, L., Walraed-Sullivan, M., Govindan, R., Mahajan, R., Millstein, T.: A general approach to network configuration analysis. In: NSDI (2015)
- Feamster, N., Balakrishnan, H.: Detecting BGP configuration faults with static analysis. In: NSDI (2005)
- Vanbever, L., Quoitin, B., Bonaventure, O.: A hierarchical model for BGP routing policies. In: ACM SIGCOMM PRESTO (2009) · DOI
- Chen, X., Mao, M., Van der Merwe, J.: PACMAN: a platform for automated and controlled network operations and configuration management. In: CoNEXT (2009) · DOI
- Enck, W., Moyer, T., McDaniel, P., Sen, S., Sebos, P., Spoerel, S., Greenberg, A., Sung, Y.-W.E., Rao, S., Aiello, W.: Configuration management at massive scale: system design and experience. IEEE J. Sel. Areas Commun. (2009) · DOI
- Gottlieb, J., Greenberg, A., Rexford, J., Wang, J.: Automated provisioning of BGP customers. IEEE Netw. 17, 44–55 (2003) · DOI
- El-Hassany, A., Miserez, J., Bielik, P., Vanbever, L., Vechev, M.: SDNRacer: concurrency analysis for SDNs. In: PLDI (2016) · DOI
- Canini, M., Venzano, D., Peresini, P., Kostic, D., Rexford, J., et al.: A NICE way to test OpenFlow applications. In: NSDI (2012)
- Scott, C., Wundsam, A., Raghavan, B., Panda, A., Or, A., Lai, J., Huang, E., Liu, Z., El-Hassany, A., Whitlock, S., Acharya, H.B., Zarifis, K., Shenker, S.: Troubleshooting Blackbox SDN control software with minimal causal sequences. In: ACM SIGCOMM (2014) · DOI
- Ball, T., Bjørner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: VeriCon: towards verifying controller programs in software-defined networks. In: PLDI (2014) · DOI
- Subramanian, K., D’Antoni, L., Akella, A.: Genesis: synthesizing forwarding tables in multi-tenant networks. In: POPL (2017) · DOI
- Kang, N., Liu, Z., Rexford, J., Walker, D.: Optimizing the “One Big Switch” abstraction in software-defined networks. In: CoNEXT (2013) · DOI
- Benson, T., Akella, A., Maltz, D.A.: Mining policies from enterprise network configuration. In: IMC (2009) · DOI
- Fortz, B., Rexford, J., Thorup, M.: Traffic engineering with traditional IP routing protocols. IEEE Commun. Mag. 40, 118–124 (2002) · DOI
- Halevy, A.Y., Mumick, I.S., Sagiv, Y., Shmueli, O.: Static analysis in datalog extensions. J. ACM 48, 971–1012 (2001) · DOI
- Mumick, I.S., Shmueli, O.: How expressive is stratified aggregation? Ann. Math. Artif. Intell. 15, 407–435 (1995) · DOI
- El-Hassany, A., Tsankov, P., Vanbever, L., Vechev, M.T.: Network-wide configuration synthesis. CoRR, abs/1611.02537 (2016). http://arxiv.org/abs/1611.02537 · arXiv
- Abiteboul, S., Hull, R., Vianu, V. (eds.): Foundations of Databases: The Logical Level (1995)
- Ullman, J.D.: Principles of Database and Knowledge-Base Systems. Computer Science Press, New York (1989)
- De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS (2008) · DOI · Paper page
- Knight, S., Nguyen, H.X., Falkner, N., Bowden, R.A., Roughan, M.: The internet topology zoo. IEEE J. Sel. Areas Commun. 29, 1765–1775 (2011) · DOI
- Doyle, J., Carroll, J.: Routing TCP/IP, vol. 1. Cisco Press, Indianapolis (2005)
- Smaragdakis, Y., Bravenboer, M.: Using datalog for fast and easy program analysis. In: de Moor, O., Gottlob, G., Furche, T., Sellers, A. (eds.) Datalog Reloaded. LNCS, vol. 6702, pp. 245–251. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24206-9_14 · DOI
- Zhang, X., Mangal, R., Grigore, R., Naik, M., Yang, H.: On abstraction refinement for program analyses in datalog. In: PLDI (2014) · DOI
- Madsen, M., Yee, M.-H., Lhoták, O.: From datalog to flix: a declarative language for fixed points on lattices. In: PLDI (2016) · DOI
- Hoder, K., Bjørner, N., De Moura, L.: $$\mu Z$$: an efficient engine for fixed points with constraints. In: CAV (2011) · DOI
- Jackson, E.K., Sztipanovits, J.: Towards a formal foundation for domain specific modeling languages. In: EMSOFT (2006) · DOI
- Jackson, E.K., Schulte, W.: Model generation for horn logic with stratified negation. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 1–20. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68855-6_1 · DOI
- Jackson, E.K. Kang, E., Dahlweid, M., Seifert, D., Santen, T.: Components, platforms and possibilities: towards generic automation for MDA. In: EMSOFT (2010) · DOI
- Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 26, 82–90 (2013) · DOI
- Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. TACAS 2014, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_26 · DOI
- Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24730-2_15 · DOI · Paper page
- Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial Sketching for Finite Programs. In: ASPLOS (2006) · DOI
- Beckett, R., Mahajan, R., Millstein, T., Padhye, J., Walker, D.: Don’t mind the gap: bridging network-wide objectives and device-level configurations. In: SIGCOMM (2016) · DOI
- Narain, S., Levin, G., Malik, S., Kaul, V.: Declarative infrastructure configuration synthesis and debugging. J. Netw. Syst. Manag. 16, 235–258 (2008) · DOI
Cited by
Sorted by citations
Large language models for agentic NetOps and AIOps: Architectures, evaluation, and safety
Bilal, M., Crowcroft, J., Wang, R., Xu, X., & Dustdar, S. (2027) · Computer Science Review · doi:10.1016/j.cosrev.2026.101075 · Cited by 10
Metadata
- Authors
- El-Hassany, A., Tsankov, P., Vanbever, L., & Vechev, M.
- Affiliations
- ETH Zurich (CH)
- Corresponding author
- El-Hassany, Ahmed
- Venue
- Lecture Notes in Computer Science
- Publisher
- Springer International Publishing
- Published
- 2017
- Pages
- 261-281
- ISSN
- 0302-9743 (ISSN-L)
- 1611-3349
- OpenAlex
- W2552298303
- Cited by
- 93
- References
- 0
- Citations by year
- 2026: 13 · 2025: 16 · 2024: 13 · 2023: 12 · 2022: 3 · 2021: 5 · 2020: 11 · 2019: 13 · 2018: 3 · 2017: 4
- FWCI
- 6.76
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- Lecture notes in computer science (publishedVersion)
- Topics
- Physical Sciences › Computer Science › Computer Networks and Communications › Software-Defined Networks and 5G
- Physical Sciences › Computer Science › Information Systems › Advanced Database Systems and Queries
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
- Keywords
- network management, router configuration, routing protocols, OSPF, BGP, network reachability, network security
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
