|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
An Efficient Equivalence-Checking Algorithm for a Model of Programs with Commutative and Absorptive Statementsстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 30 декабря 2016 г.
- Автор: Vladislav Podymov
- Журнал: Fundamenta Informaticae
- Том: 147
- Номер: 2-3
- Год издания: 2016
- Издательство: I O S press
- Местоположение издательства: Netherlands
- Первая страница: 315
- Последняя страница: 336
- DOI: 10.3233/FI-2016-1410
- Аннотация: For many program analysis problems it is useful to have means to efficiently prove that given programs have similar (equivalent) behaviors. Unfortunately, in most cases to prove the behavioral equivalence is an undecidable problem. A common way to overcome such undecidability is to consider a model of programs with an abstract semantics based on the real one, in which only some simple properties are captured, and to provide an efficient equivalence-checking algorithm for the model. We focus on two kinds of properties of data-modifying statements of imperative programs. Statements a and b are commutative, if the execution of sequences ab and ba lead to the same result. A statement b is (left-)absorptive for a statement a, if the execution of sequences ab and b lead to the same result. We consider propositional program models in which commutativity and absorption properties are caprtured (CA-models). Formally, data states for a CA-model are elements of a monoid over the set of statement symbols, defined by an arbitrary set of relations of the form ab = ba (for commutativity) and ab = b (for absorption). We propose an equivalence-checking algorithm for CA-models based on (what we call) progressive monoids. The algorithm terminates in time polynomial in size of programs. As a consequence, we prove a polynomial-time decidability for the equivalence problem in such CA-models.
- Добавил в систему: Подымов Владислав Васильевич