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