Model and program repair via SAT solving

Paul Attie, Ali Cherri, Kinan Dak Al Bab, Mohamad Sakr, Jad Saklawi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We consider the subtractive model repair problem: given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M' that satisfies η. Thus, M can be repaired to satisfy η by deleting states and/or transitions. We give a reduction to boolean satisfiability, and implement the repair method using this reduction. We also extend the basic repair method in three directions: (1) the use of abstraction, and (2) the repair of concurrent Kripke structures and concurrent programs, and (3) the repair of hierarchical Kripke structures. These last two extensions both avoid state-explosion.

Original languageEnglish (US)
Title of host publication2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages148-157
Number of pages10
ISBN (Electronic)9781509002375
DOIs
StatePublished - Nov 30 2015
Externally publishedYes
EventACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015 - Austin, United States
Duration: Sep 21 2015Sep 23 2015

Publication series

Name2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015

Conference

ConferenceACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015
CountryUnited States
CityAustin
Period9/21/159/23/15

Fingerprint

Repair
Explosions

Keywords

  • Computational modeling
  • Concurrent computing
  • Labeling
  • Maintenance engineering
  • Polynomials
  • Programming
  • Semantics

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Cite this

Attie, P., Cherri, A., Dak Al Bab, K., Sakr, M., & Saklawi, J. (2015). Model and program repair via SAT solving. In 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015 (pp. 148-157). [7340481] (2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/MEMCOD.2015.7340481

Model and program repair via SAT solving. / Attie, Paul; Cherri, Ali; Dak Al Bab, Kinan; Sakr, Mohamad; Saklawi, Jad.

2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015. Institute of Electrical and Electronics Engineers Inc., 2015. p. 148-157 7340481 (2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Attie, P, Cherri, A, Dak Al Bab, K, Sakr, M & Saklawi, J 2015, Model and program repair via SAT solving. in 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015., 7340481, 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, Institute of Electrical and Electronics Engineers Inc., pp. 148-157, ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, Austin, United States, 9/21/15. https://doi.org/10.1109/MEMCOD.2015.7340481
Attie P, Cherri A, Dak Al Bab K, Sakr M, Saklawi J. Model and program repair via SAT solving. In 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015. Institute of Electrical and Electronics Engineers Inc. 2015. p. 148-157. 7340481. (2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015). https://doi.org/10.1109/MEMCOD.2015.7340481
Attie, Paul ; Cherri, Ali ; Dak Al Bab, Kinan ; Sakr, Mohamad ; Saklawi, Jad. / Model and program repair via SAT solving. 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015. Institute of Electrical and Electronics Engineers Inc., 2015. pp. 148-157 (2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015).
@inproceedings{ae9d337671604cdfaa2b3ad5407e7d39,
title = "Model and program repair via SAT solving",
abstract = "We consider the subtractive model repair problem: given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M' that satisfies η. Thus, M can be repaired to satisfy η by deleting states and/or transitions. We give a reduction to boolean satisfiability, and implement the repair method using this reduction. We also extend the basic repair method in three directions: (1) the use of abstraction, and (2) the repair of concurrent Kripke structures and concurrent programs, and (3) the repair of hierarchical Kripke structures. These last two extensions both avoid state-explosion.",
keywords = "Computational modeling, Concurrent computing, Labeling, Maintenance engineering, Polynomials, Programming, Semantics",
author = "Paul Attie and Ali Cherri and {Dak Al Bab}, Kinan and Mohamad Sakr and Jad Saklawi",
year = "2015",
month = "11",
day = "30",
doi = "10.1109/MEMCOD.2015.7340481",
language = "English (US)",
series = "2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "148--157",
booktitle = "2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015",

}

TY - GEN

T1 - Model and program repair via SAT solving

AU - Attie, Paul

AU - Cherri, Ali

AU - Dak Al Bab, Kinan

AU - Sakr, Mohamad

AU - Saklawi, Jad

PY - 2015/11/30

Y1 - 2015/11/30

N2 - We consider the subtractive model repair problem: given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M' that satisfies η. Thus, M can be repaired to satisfy η by deleting states and/or transitions. We give a reduction to boolean satisfiability, and implement the repair method using this reduction. We also extend the basic repair method in three directions: (1) the use of abstraction, and (2) the repair of concurrent Kripke structures and concurrent programs, and (3) the repair of hierarchical Kripke structures. These last two extensions both avoid state-explosion.

AB - We consider the subtractive model repair problem: given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M' that satisfies η. Thus, M can be repaired to satisfy η by deleting states and/or transitions. We give a reduction to boolean satisfiability, and implement the repair method using this reduction. We also extend the basic repair method in three directions: (1) the use of abstraction, and (2) the repair of concurrent Kripke structures and concurrent programs, and (3) the repair of hierarchical Kripke structures. These last two extensions both avoid state-explosion.

KW - Computational modeling

KW - Concurrent computing

KW - Labeling

KW - Maintenance engineering

KW - Polynomials

KW - Programming

KW - Semantics

UR - http://www.scopus.com/inward/record.url?scp=84960977110&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84960977110&partnerID=8YFLogxK

U2 - 10.1109/MEMCOD.2015.7340481

DO - 10.1109/MEMCOD.2015.7340481

M3 - Conference contribution

AN - SCOPUS:84960977110

T3 - 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015

SP - 148

EP - 157

BT - 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015

PB - Institute of Electrical and Electronics Engineers Inc.

ER -