<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.3 20210610//EN" "https://jats.nlm.nih.gov/publishing/1.3/JATS-journalpublishing1-3.dtd">
<article article-type="research-article" dtd-version="1.3" xml:lang="ru">
  <front>
    <journal-meta>
      <journal-title-group>
        <journal-title>Computing, Telecommunication and Control</journal-title>
        <trans-title-group xml:lang="ru">
          <trans-title>Информатика, телекоммуникации и управление</trans-title>
        </trans-title-group>
      </journal-title-group>
      <issn pub-type="epub">2687-0517</issn>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="publisher-id">23</article-id>
      <title-group>
        <article-title>Verification method based on decomposition of states in rely-guarantee/sep logic</article-title>
        <trans-title-group xml:lang="ru">
          <trans-title>Аксиоматический метод верификации на основе декомпозиции состояний в методе RGSEP</trans-title>
        </trans-title-group>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <name>
            <surname>Prokopenko</surname>
            <given-names>Artem</given-names>
          </name>
          <email>artjom.prokopenko@gmail.com</email>
        </contrib>
        <contrib contrib-type="author">
          <name>
            <surname>Tormasov</surname>
            <given-names>Aleksandr</given-names>
          </name>
          <email>tor@phystech.edu</email>
        </contrib>
      </contrib-group>
      <pub-date publication-format="electronic" date-type="pub" iso-8601-date="2010-12-10">
        <day>10</day>
        <month>12</month>
        <year>2010</year>
      </pub-date>
      <issue>6</issue>
      <issue-id pub-id-type="publisher-id">113</issue-id>
      <fpage>127</fpage>
      <lpage>135</lpage>
      <abstract xml:lang="en">
        <p>We propose new method in this paper for local RGSep reasoning. Our method support a hiding rule for hiding the local sharing of resources from the outside world. These rules allow us to write local rely/guarantee conditions and improve the reusability of veryfied program modules.</p>
      </abstract>
      <kwd-group xml:lang="en">
        <kwd>multiprocessor programming</kwd>
        <kwd>verification</kwd>
        <kwd>Hoare logic</kwd>
        <kwd>rely-guarantee/sep</kwd>
        <kwd>RGSEP</kwd>
      </kwd-group>
    </article-meta>
  </front>
</article>
