Описание тега abstract-interpretation
Формальный метод статического вывода свойств программы.
3
ответа
Абстрактная интерпретация в LLVM
Мне нужно использовать абстрактную интерпретацию, чтобы провести некоторый анализ с использованием LLVM. Это возможно? или мне нужно проще использовать инструменты анализа. Если бы я мог сделать это с помощью LLVM, какие классы помогли бы мне сформу…
12 дек '15 в 12:56
2
ответа
В чем разница между анализом потока данных и абстрактной интерпретацией
В чем разница между анализом потока данных и абстрактной интерпретацией и используются ли они для одной и той же цели? Каковы плюсы и минусы этих двух по отношению друг к другу.
28 июн '13 в 18:16
1
ответ
Рассчитать достижимость функции, используя анализ значений frama-c
Вот мой пример: int in; int sum(int n){ int log_input = n; int log_global = in; return 0; } int main(){ int n = Frama_C_interval(-10, 10); in = n; if (n > 0){ sum(n + 4); } return 0; } Я хотел бы найти диапазон входной переменной n при инициализа…
03 фев '16 в 11:25
1
ответ
Автоматическое расширение в анализе значений frama-c
Я ищу метод для расширения циклов без подсказок пользователя. Я объясню на примере: int z; void main(void) { int r = Frama_C_interval(0, MAX_INT); z = 0; for (int y=0; y<r; y++) z++; } При выполнении анализа значения frama-c для этого кода глобал…
26 дек '15 в 16:39
4
ответа
Краткие примеры реализации абстрактной интерпретации
Я беру курс по абстрактной интерпретации, но я не видел примеров того, как теория соотносится с реальным кодом. Я ищу короткие примеры кода, где мне не нужно работать с целым компилятором. Анализ не должен быть полезным, я просто хотел бы увидеть пр…
28 май '10 в 11:24
0
ответов
Вычисление сводки функций с использованием анализа значений Frama-C
Допустим, у нас есть следующий пример кода: int a(int x){ if (x < 0){ return -50; } if (x >= 0 && x <= 3600){ return x - 100; } return x + 100; } int main(){ int q = Frama_C_interval(50, 5000); return a(q); } Запустив инструмент ана…
06 янв '16 в 22:39
2
ответа
Что означает "петли должны быть сложены, чтобы обеспечить завершение"?
В статье о формальных методах (абстрактная интерпретация, если быть точным) я наткнулся на "петли должны быть свернуты до конца". Мне ясно, что означает завершение, но я не знаю, что такое свернутая петля, и как выполнять складывание на петле. Может…
25 авг '11 в 14:47
1
ответ
Правдивая абстрактная мера для стоимости выполнения цели Пролога
Далее я рассматриваю только программы на чистом прологе. Это означает, что я не говорю о побочных эффектах и вызовах ОС, которые оставляют сферу логики, чтобы делать что-то, что не может наблюдаться изнутри Пролога. Существует известная абстрактна…
23 июл '17 в 20:46
2
ответа
Как доказать простые равенства недетерминированных значений в Frama-C + EVA?
Меня немного смущает поведение Frama-C версии 18.0 (Argon). Учитывая следующую программу: #include <assert.h> #include <limits.h> /*@ requires order: min <= max; assigns \result \from min, max; ensures result_bounded: min <= \resul…
16 май '19 в 19:31
1
ответ
Невозможно использовать команды JBMC (Bounded Model Checker) для Java
Я новичок в JBMC(ограниченная модель проверки). У нас есть требование выяснить возможности исключения RunTime, которое может возникнуть в Java-программе, без ее запуска. Мы искали некоторые абстрактные рамки интерпретации и обнаружили, что JBMC помо…
19 июн '19 в 16:15
0
ответов
Что означает "текстовая точка"?
В документе есть такие слова, как "Только объекты, созданные в одной текстовой точке, имеют абстрактные представления". Что означает "текстовая точка"? Я предполагаю, что этот термин является общим термином, а не тематическим.
03 ноя '19 в 01:52
0
ответов
Операторы сужения и расширения в анализе потока данных
Я реализую алгоритм анализа потока данных ( https://en.wikipedia.org/wiki/Data-flow_analysis) для интервального анализа, используя подход рабочего списка. Однако я не понимаю, когда применять операторы расширения и сужения. Насколько я понимаю, опер…
30 ноя '19 в 08:15
0
ответов
Вывод инвариантов с абстрактной интерпретацией - примеры
Я читал о выводе инвариантов посредством абстрактной интерпретации, особенно статью Патрика Кузо и Радии Кузо "Автоматический синтез оптимальных инвариантных утверждений: математические основы". Однако я не могу найти практического примера того, как…
20 авг '20 в 18:33
0
ответов
Применение обратного анализа
Используя абстрактную интерпретацию, знаете ли вы какие-либо (практические или нет) применения обратного анализа? Приложения, которые также не требуют прямого анализа, а только обратного анализа.
12 окт '23 в 08:13