Дедуктивный метод анализа логических гонок с использованием сепарационной логики

В работе предложен дедуктивный метод анализа логических гонок на основе метода Rely-Guarantee и сепарационной логики. В отличие от схожих методов, предложенный ме- тод позволяет проводить анализ параллельных программ на общей памяти, в которых неко- торые потоки имеют совместно используемые области памяти, скрытые от других потоков; не специфицировать состояния всей системы после каждого шага, что способствует прове- дению анализа логических гонок с меньшим числом ложных отчетов