Публикации по теме 'formal-methods'
Масштабируемое глубокое символьное обучение с подкреплением с помощью Imandra: Часть I
Сочетание статистического (например, нейронных сетей) и классического «символического» ИИ давно интересовало исследователей ИИ и позволило получить некоторые очень интересные недавние результаты.
В Aesthetic Integration мы разработали Imandra ™, автоматизированную облачную систему символьных рассуждений, основанную на последних достижениях в формальной проверке. Способность Имандры разлагать бесконечные пространства состояний алгоритмов на конечный набор символических областей..
Введение в проверку моделей с помощью TLA+
В этом месяце я ставлю перед собой задачу завершить серию онлайн-лекций в университете Введение в проверку моделей . Курс ведет Йост-Питер Катоен, один из авторов книги Принципы проверки моделей . Катоен отмечает, что курс больше сосредоточен на теории, чем на применении. Однако, поскольку у меня есть небольшой опыт в этой области, я использую курс и упражнения в качестве предлога для практики использования TLA+ и связанных с ним инструментов, языка алгоритмов Pluscal и TLC Model..
Визуальное программирование: что пошло не так и есть ли возможности для улучшения?
Это ответ на обсуждение в Hacker News после публикации в блоге Medium о почему визуальное программирование не отстой . Давайте прольем свет на некоторые повторяющиеся моменты, поднятые в разделе комментариев.
Замечание №1: Я перепробовал множество языков визуального программирования, и все они отстой.
Мы тебя чувствуем! И мы твердо верим, что существующие инструменты можно улучшить. В последнее десятилетие было проведено большое количество исследований по увязке визуальных..
Тестирование на основе собственности за пять минут.
Среда, 06 марта 2019
В двух словах о тестировании на основе свойств.
В двух словах о тестировании на основе свойств.
Привет! Добро пожаловать в первую часть моей серии статей о ментальных моделях. Щелкните здесь для просмотра других частей.
Допустим, у нас есть функция сортировки с именем mySort ,
Стандартизированное тестирование попросит вас предложить некоторые значения для тестирования,
тогда как Тестирование на основе свойств просит вас объявить схему..
Знакомство с миром Формальные методы/проверка
Если вы, как и я, прошли через такие термины, как «формальные методы» / «верификация программы» / «формальная верификация» во времена бакалавриата информатики, но не знали об интересных исследованиях, проводимых в этой области, то вы можете хотите следовать этому письму, чтобы начать работу с этой конкретной областью информатики и логики.
Это вводная статья по этой теме (которая будет состоять из других частей), а также моя первая работа на Medium!
Я предполагаю, что вы знакомы с..
Десять проектов, связанных с Ethereum, которые вы могли бы предпринять
За полгода в пространстве Ethereum у меня накопилось несколько интересных проектов. Я обычно откладываю их в сторону и вместо этого работаю над существующими материалами, просматривая, добавляя тесты, удаляя ошибки и записывая доказательства. Может быть, мне стоит начать все мои незавершенные проекты, повозиться и в конце концов найти то, что набирает обороты. Может, мне стоит начать с малого. Тогда самый простой способ начать - это как-то выразить идеи. Вот чем я здесь занимаюсь.
Если..
Вопросы по теме 'formal-methods'
Анализ статических значений LLVM для оптимизации
Допустим, у меня есть такая функция:
int foo(int a, int b, int d, int x){
if (c) {a = 1; b = 1; d = a;}
else {a = 2; b = 2; d = 1;}
if (a == b) {x = d;} else {x = 0;}
return x;
}
Эта тривиальная функция всегда возвращает 1. При...
650 просмотров
schedule
14.01.2023
Верна ли эта спецификация TLA +?
Пока что я написал немного кода для своего проекта, но не знаю, правда он или ложь. Вы, ребята, можете увидеть мой код? Во-первых, я должен опубликовать требование для лучшего понимания ..
В информатике взаимное исключение относится к требованию...
331 просмотров
schedule
12.05.2023
Какова связь между инвариантом цикла и самым слабым предусловием
Учитывая инвариант цикла, Википедия перечисляет хороший способ создать самые слабые предварительные условия для цикла (из http://en.wikipedia.org/wiki/Predicate_transformer_semantics ):
wp(while E inv I do S, R) =
I \wedge
\forall y. ((E...
990 просмотров
schedule
16.07.2022
Как определить переводчик выражений?
Я определил 2 почти идентичных языка (foo и bar):
theory SimpTr
imports Main
begin
type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"
datatype foo_exp =
FooBConst bool |
FooIConst int |
FooLet vname foo_exp foo_exp...
59 просмотров
schedule
29.07.2023
Nusmv состояния и переходы
Я хочу сформулировать эту проблему в NuSMv:
Пользователь может находиться в одном из этих трех состояний: U-потребность, U-использование, U-грусть (представляющий собой пользователя, который нуждается в услуге, начинает пользоваться и он/она...
166 просмотров
schedule
11.10.2022
Как представить схемы последовательных операций [Z-нотация]
У меня есть схема работы C, которая состоит из двух последовательных схем операций A и B. A необходимо выполнить до B. Я застрял в том, как представить последовательность активации схемы.
Могу ли я использовать соединение схемы, т.е. C == A ∧ B?...
95 просмотров
schedule
17.06.2022
Как явно указать подпись в Alloy?
Я изучаю язык моделирования Alloy и увидел этот код.
sig Person {
partner: Person
}
fact partnerProperties {
partner = ~partner
no p: Person | p in p.partner
}
Этот код выражает «Отношения человека partner взаимны».
Я могу понять...
62 просмотров
schedule
07.07.2022
Как написать большой и большой клин на Изабель
Я пытаюсь использовать Изабель для автоматического доказательства. Однако у меня возникла проблема с указанием формул в Isabelle. Например, у меня есть такие формулы, как Затем я определяю наборы и использую символы big_wedge и big_vee в...
123 просмотров
schedule
08.02.2023
