uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Optimizing Horn Solvers for Network Repair
Cornell Univ, Ithaca, NY 14853 USA..
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.ORCID iD: 0000-0002-2733-7098
CU Boulder, Boulder, CO USA..
CU Boulder, Boulder, CO USA..
Show others and affiliations
2016 (English)In: Proceedings of the 2016 16Th Conference on Formal Methods In Computer-Aided Design (FMCAD 2016) / [ed] Piskac, R Talupur, M, IEEE , 2016, p. 73-80Conference paper, Published paper (Refereed)
Abstract [en]

Automatic program repair modifies a faulty program to make it correct with respect to a specification. Previous approaches have typically been restricted to specific programming languages and a fixed set of syntactical mutation techniques-e.g., changing the conditions of if statements. We present a more general technique based on repairing sets of unsolvable Horn clauses. Working with Horn clauses enables repairing programs from many different source languages, but also introduces challenges, such as navigating the large space of possible repairs. We propose a conservative semantic repair technique that only removes incorrect behaviors and does not introduce new behaviors. Our proposed framework allows the user to request the best repairs-it constructs an optimization lattice representing the space of possible repairs, and uses a novel local search technique that exploits heuristics to avoid searching through sub-lattices with no feasible repairs. To illustrate the applicability of our approach, we apply it to problems in software-defined networking (SDN), and illustrate how it is able to help network operators fix buggy configurations by properly filtering undesired traffic. We show that interval and Boolean lattices are effective choices of optimization lattices in this domain, and we enable optimization objectives such as modifying the minimal number of switches. We have implemented a prototype repair tool, and present preliminary experimental results on several benchmarks using real topologies and realistic repair scenarios in data centers and congested networks.

Place, publisher, year, edition, pages
IEEE , 2016. p. 73-80
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:uu:diva-341872ISI: 000406120700017ISBN: 978-0-9835678-6-8 (electronic)OAI: oai:DiVA.org:uu-341872DiVA, id: diva2:1183150
Conference
16th Conference on Formal Methods in Computer-Aided Design (FMCAD), OCT 03-06, 2016, Mountain View, CA
Available from: 2018-02-15 Created: 2018-02-15 Last updated: 2018-02-15Bibliographically approved

Open Access in DiVA

No full text in DiVA

Authority records BETA

Rümmer, Philipp

Search in DiVA

By author/editor
Rümmer, Philipp
By organisation
Computer Systems
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 10 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf