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

4 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 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

Keywords

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

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Model and program repair via SAT solving'. Together they form a unique fingerprint.

  • 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