Уважаемые коллеги, доброго времени суток! Представляем вам нидерландское научное издание Formal Methods in System Design. Журнал имеет третий квартиль, издаётся в Springer Netherlands, его SJR за 2021 г. равен 0,502, пятилентий импакт-фактор 1,676, печатный ISSN - 0925-9856, электронный - 1572-8102, предметные области - Теоретические компьютерные науки, Программное обеспечение, Аппаратная часть и системная архитектура. Вот так выглядит обложка:
Редактором является Нир Питерман, контактные данные - nir.piterman@gu.se.
Дополнительные публикационные контакты - mangayarkarasi.lakshmiram@springernature.com, Marielle.Klijn@springer.com, journalpermissions@springernature.com, patrick.keefe@springer.com.
Основное внимание в данном журнале уделяется формальным методам проектирования, внедрения и проверки корректности аппаратных (СБИС) и программных систем. Стимул для создания журнала с этой целью исходил как от академических кругов, так и от промышленности. В обеих областях интерес к использованию формальных методов быстро возрос за последние несколько лет. Огромные затраты и время, необходимые для проверки новых конструкций, привели к осознанию необходимости разработки более мощных методов. В настоящее время разрабатывается ряд методов и инструментов для повышения надежности сложных аппаратных и программных систем. В то время как граница между (суб) компонентами системы, которые воплощены в аппаратном обеспечении, прошивке или программном обеспечении, продолжает размываться, соответствующие дисциплины проектирования и формальные методы быстро развиваются. Следовательно, ожидается появление важного (и полезного) набора общеприменимых формальных методов, которые окажут сильное влияние на будущие среды проектирования и методы проектирования.
Адрес издания - https://www.springer.com/journal/10703
Пример статьи, название - Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking. Заголовок (Abstract) - This paper addresses model checking based on SAT solvers and Craig interpolants. We tackle major scalability problems of state-of-the-art interpolation-based approaches, and we achieve two main results: (1) A novel model checking algorithm; (2) A new and flexible way to handle an incremental representation of (over-approximated) forward reachable states. The new model checking algorithm IGR, Interpolation with Guided Refinement, partially takes inspiration from IC3 and interpolation sequences. It bases its robustness and scalability on incremental refinement of state sets, and guided unwinding/simplification of transition relation unrollings. State sets, the central data structure of our algorithm, are incrementally refined, and they represent a valuable information to be shared among related problems, either in concurrent or sequential (multiple-engine or multiple-property) execution schemes. We provide experimental data, showing that IGR extends the capability of a state-of-the-art model checker, with a specific focus on hard-to-prove properties. Keywords: Formal verification; Hardware model checking; Interpolation; SAT solving
