В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

Compiler Development

983 membersпожаловаться на группу
2020 November 12

M

MaxGraey in Compiler Development
Peter Sovietov
Пережиток прошлого. Спасибо, исправил.
👍
источник
16:18пожаловаться#1

YY

Yuriy Yarosh in Compiler Development
А как нынче обстоят дела с верификациями конкурентностей на темпоральной логике ?

Просто посмотрел в F* и в TLA+2 и как-то не густо...
Может есть какие-то проекты или паперы интересные глянуть ?
Спасибо.
источник
16:35пожаловаться#2

LW

Lev Walkin in Compiler Development
На темпоральной логике, да, TLA+ и примерно всё. Если уйти чуть больше в практику и симуляции, есть SPIN/Promela.
источник
16:43пожаловаться#3

AG

Alex Gryzlov in Compiler Development
https://en.wikipedia.org/wiki/List_of_model_checking_tools
Wikipedia
List of model checking tools
Wikimedia list article
источник
16:49пожаловаться#4

AG

Alex Gryzlov in Compiler Development
они там практически все на темпоральной логике
источник
16:49пожаловаться#5

AG

Alex Gryzlov in Compiler Development
вот например довольно свежий обзор https://arxiv.org/abs/1803.10324
источник
16:52пожаловаться#6

AT

Alexander Tchitchigi... in Compiler Development
Yuriy Yarosh
А как нынче обстоят дела с верификациями конкурентностей на темпоральной логике ?

Просто посмотрел в F* и в TLA+2 и как-то не густо...
Может есть какие-то проекты или паперы интересные глянуть ?
Спасибо.
F* не имеет отношения к темпоральной логике только...
А в чём именно вопрос?
источник
16:53пожаловаться#7

YY

Yuriy Yarosh in Compiler Development
Alexander Tchitchigin
F* не имеет отношения к темпоральной логике только...
А в чём именно вопрос?
Ну просто в F* как-то не обнаружил средств для верификации конкурентных процессов... может чего пропустил,
источник
17:00пожаловаться#8

YY

Yuriy Yarosh in Compiler Development
Lev Walkin
На темпоральной логике, да, TLA+ и примерно всё. Если уйти чуть больше в практику и симуляции, есть SPIN/Promela.
Спасибо - гляну.
источник
17:00пожаловаться#9

YY

Yuriy Yarosh in Compiler Development
Alex Gryzlov
они там практически все на темпоральной логике
Да, это понятно...
Гляну обзор.
источник
17:00пожаловаться#10

AT

Alexander Tchitchigi... in Compiler Development
Yuriy Yarosh
Ну просто в F* как-то не обнаружил средств для верификации конкурентных процессов... может чего пропустил,
Скорее всего, нет, не пропустили. Потому что F* не имеет отношения к темпоральной логике. А нацелен на функциональную корректность.
источник
17:01пожаловаться#11

AT

Anton Trunov in Compiler Development
Можно погрузить темпоралку в прувер...
источник
17:10пожаловаться#12

AG

Alex Gryzlov in Compiler Development
верификация конкурентных процессов разделяется на модель-теоретические и пруф-теоретические методы
источник
17:10пожаловаться#13

AT

Anton Trunov in Compiler Development
Но да, кроме как темпоралки для Coq я как-то не встречал ничего.
источник
17:10пожаловаться#14

AG

Alex Gryzlov in Compiler Development
первое это модел чекинг, второе - сессионные типы и (конкурентная) сепарационная логика
источник
17:11пожаловаться#15

AG

Alex Gryzlov in Compiler Development
между ними конечно есть перекрестное опыление, например работы миллера и ко по пруф-теории модел чекинга (в частности http://slimmer.gforge.inria.fr/bedwyr/)
источник
17:12пожаловаться#16

AG

Alex Gryzlov in Compiler Development
но вообще с этими вопросами лучше в @practical_fm
источник
17:14пожаловаться#17

M

MrSmith in Compiler Development
http://groups.csail.mit.edu/commit/
источник
18:33пожаловаться#18

E

EgorBo in Compiler Development
https://twitter.com/gvanrossum/status/1326932991566700549 хех
Twitter
Guido van Rossum
I decided that retirement was boring and have joined the Developer Division at Microsoft. To do what? Too many options to say! But it’ll make using Python better for sure (and not just on Windows :-). There’s lots of open source here. Watch this space.
источник
21:53пожаловаться#19

TS

Timur Safin in Compiler Development
EgorBo
https://twitter.com/gvanrossum/status/1326932991566700549 хех
Twitter
Guido van Rossum
I decided that retirement was boring and have joined the Developer Division at Microsoft. To do what? Too many options to say! But it’ll make using Python better for sure (and not just on Windows :-). There’s lots of open source here. Watch this space.
подозрительно, что Андерс первым его поздравил - наверное, он его и переманил?
источник
22:02пожаловаться#20