Описание тега formal-verification
Формальная проверка - это акт доказательства или опровержения правильности предполагаемых алгоритмов, лежащих в основе системы, в отношении определенной формальной спецификации или свойства с использованием формальных математических методов.
11
ответов
Существуют ли доказуемые языки реального мира? (Scala?)
Меня учили формальным системам в университете, но я был разочарован тем, что они, казалось, не использовались в реальном слове. Мне нравится идея быть в состоянии знать, что некоторый код (объект, функция, что угодно) работает, не путем тестирования…
31 окт '10 в 20:40
0
ответов
Построение обратимой схемы из грамматики
Я ищу способ автоматически генерировать обратимую схему с учетом грамматики (без контекста). Под спецификацией логической схемы я подразумеваю список вентилей (взятых из универсального набора: И, ИЛИ, НЕ, NAND и т. Д.) Плюс бит (ы), к которым примен…
22 дек '17 в 16:38
1
ответ
Как исследование символического состояния работает в проверке символьной модели
Следующий алгоритм представляет собой грубый эскиз проверки модели с помощью Computational Tree Logic (CTL): Заявлено, что: Задача проверки модели для CTL состоит в том, чтобы проверить для заданной системы переходов TS и формулы CTL Φ, если TS |= Φ…
30 май '18 в 02:55
0
ответов
Моделирование вектора / массива фиксированного размера в Boogie
Я пытаюсь моделировать векторы фиксированной длины в буги. Каждый вектор с разным размером должен быть другого типа. Я попробовал два подхода, но у обоих есть особая проблема. Подход 1: Тип псевдонимов Определите псевдоним типа и некоторые аксиомы, …
26 июл '18 в 08:35
1
ответ
Построить формальную модель UART в NuSMV?
Я изучаю проверку моделей и NuSMV для моего образования. Я могу редактировать и запускать код NuSMV, и у меня есть четкое представление о том, что такое UART и что делает. Моя задача - формально смоделировать UART с NuSMV, но в настоящее время я не …
26 фев '17 в 15:27
1
ответ
Печать внутренних решающих формул в z3
Инструмент доказательства теорем z3 занимает много времени, чтобы решить формулу, с которой, я думаю, она сможет легко справиться. Чтобы лучше понять это и, возможно, оптимизировать мой ввод в z3, я хотел увидеть внутренние ограничения, которые z3 г…
27 окт '12 в 18:09
1
ответ
Знание, когда доказательство в стиле Изара действительно в Изабель
Я работаю над упражнением, пытаясь выучить язык изар. У меня есть следующий скрипт для леммы о списках. lemma "EX ys zs. xs = ys @ zs ∧ (length ys = length zs ∨ length ys = length zs + 1)" proof - show ?thesis by blast (* L *) qed Кажется, Изабель п…
11 янв '19 в 22:56
1
ответ
Дафни: повернутая область проверки массива методом
Это доказательство дает бесконечный цикл в верификаторе Дафниса: // Status: verifier infinite loop // rotates a region of the array by one place forward method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>) requi…
12 янв '16 в 02:47
1
ответ
Почему lean добавляет неявные переменные к леммам из eq?
Следующий код имеет странное поведение variable (toto : Type) check eq.symm --output: eq.symm : ?a toto = ?b toto → ?b toto = ?a toto Я ожидал бы, что проверка не учитывает не относящуюся к делу неявную переменную toto, показывая мне тип eq.symm. Эт…
06 июн '16 в 13:56
0
ответов
Формализуйте следующее требование в логике высказываний, используя подходящие высказывания для компонентных утверждений.
Процесс a или процесс b входит в критическую секцию, но не одновременно. Если это произойдет (то есть они одновременно входят в критическую секцию), будет выполнено прерывание. р = обработать q = процесс б r = критическая секция оператор ∨ = или опе…
06 дек '15 в 15:31
11
ответов
Могут ли функции Haskell быть доказаны / проверены на модели / проверены со свойствами корректности?
Продолжая идеи: есть ли доказуемые языки реального мира? Я не знаю как вы, но мне надоело писать код, который я не могу гарантировать. Задав вышеупомянутый вопрос и получив феноменальный ответ (спасибо всем!), Я решил сузить свой поиск доказуемого, …
02 ноя '10 в 13:12
2
ответа
Формальная проверка сроков
Мне известны различные формальные средства проверки для проверки свойств программ (например, средство проверки модели SPIN). Существуют ли какие-либо общие инструменты / методологии для проверки требований к синхронизации во встроенных системах реал…
20 ноя '12 в 05:43
10
ответов
Имеют ли место формальные методы проверки программ в промышленности?
Я взглянул на Hoare Logic в колледже. То, что мы сделали, было действительно просто. Большую часть того, что я сделал, было доказательство правильности простых программ, состоящих из while петли, if заявления и последовательность инструкций, но не б…
28 июл '09 в 21:20
1
ответ
От включения набора для установления равенства в Lean
Учитывая доказательство включения множества и его обратное, я хотел бы показать, что два множества равны. Например, я знаю, как доказать следующее утверждение и его обратное утверждение: open set universe u variable elem_type : Type u variable A : s…
13 авг '17 в 09:28
1
ответ
Нужна помощь в понимании метода Овики-Гриза
Я (по ошибке) взял курс о проверке параллельных программ, и мы до сих пор рассматривали этот метод, называемый "метод Овики-Гриза". По-видимому, можно доказать различные результаты о программе, связав утверждение с каждым утверждением, и показать, ч…
25 сен '14 в 05:15
0
ответов
Дафни - "Проверка неокончательна" на rise4fun
Я получил сообщение об ошибке "Verification Inconclusive" для алгоритма графа, который я пытаюсь доказать в режиме dafny VS2015. Я пытался использовать версию 2.1.1, новейшую версию, доступную на странице релизов dafny. Здесь был только еще один воп…
28 мар '18 в 10:25
3
ответа
Является ли статический анализ действительно формальной проверкой?
Я читал о формальной проверке, и суть в том, что для работы требуются формальная спецификация и модель. Однако многие источники классифицируют статический анализ как метод формальной проверки, некоторые упоминают абстрактную интерпретацию и упоминаю…
21 фев '16 в 07:22
1
ответ
Причина различий в количестве достижимых состояний
Я проверяю 8-битный сумматор с этим кодом. Когда я печатаю, число достижимых состояний равно 1, если основной модуль пуст, и 2^32, если весь основной модуль включен. Что делает эту разницу в сообщаемом количестве достижимых состояний? Для 4-разрядно…
08 май '17 в 05:52
0
ответов
Уппал: оценка вероятности на примере железнодорожных ворот
Я использую пример Train Gate и хочу запустить свойство проверки Pr[<=100] (<> Train(0).Cross) Сказать, какова вероятность пересечения поезда (0) в 100-кратных единицах . Я добавил часы в безопасное состояние, как показано в прикрепленном файле. Зап…
04 сен '18 в 08:57
1
ответ
Анализ статических значений 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. Компиляция с помощью clan…
08 ноя '12 в 23:13