Model and program repair via SAT solving

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

doi:10.1109/MEMCOD.2015.7340481

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 proceeding › Conference contribution

7 Scopus citations

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 language	English (US)
Title of host publication	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
Number of pages	10
ISBN (Electronic)	9781509002375
DOIs	https://doi.org/10.1109/MEMCOD.2015.7340481
State	Published - Nov 30 2015
Externally published	Yes
Event	ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015 - Austin, United States Duration: Sep 21 2015 → Sep 23 2015

Publication series

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

Conference

Conference	ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015
Country/Territory	United States
City	Austin
Period	9/21/15 → 9/23/15

Keywords

Computational modeling
Concurrent computing
Labeling
Maintenance engineering
Polynomials
Programming
Semantics

ASJC Scopus subject areas

Software
Hardware and Architecture

Access to Document

10.1109/MEMCOD.2015.7340481

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). Article 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 et al.
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 proceeding › Conference 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). doi: 10.1109/MEMCOD.2015.7340481

@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",

note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015 ; Conference date: 21-09-2015 Through 23-09-2015",

year = "2015",

month = nov,

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.

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

Y2 - 21 September 2015 through 23 September 2015

ER -

Model and program repair via SAT solving

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this