Простий
пошук
Розширений
пошук
Покажчики
Професійний
пошук
Рубрикатор
НБУВ
Розподілений
пошук

Бази даних

Наукова періодика України - результати пошуку

Книжкові видання та компакт-диски
Журнали та продовжувані видання
Автореферати дисертацій
Реферативна база даних
Наукова періодика України
Тематичний навігатор
Авторитетний файл імен осіб
Mozilla Firefox Для швидкої роботи та реалізації всіх функціональних можливостей пошукової системи використовуйте браузер
"Mozilla Firefox"
Вид пошуку
Повнотекстовий пошук
 Знайдено в інших БД:Реферативна база даних (1)
Список видань за алфавітом назв:
A  B  C  D  E  F  G  H  I  J  L  M  N  O  P  R  S  T  U  V  W  
А  Б  В  Г  Ґ  Д  Е  Є  Ж  З  И  І  К  Л  М  Н  О  П  Р  С  Т  У  Ф  Х  Ц  Ч  Ш  Щ  Э  Ю  Я  

Авторський покажчик    Покажчик назв публікацій


Пошуковий запит: (<.>AT=Melnyk Static Analysis of Source$<.>)
Загальна кількість знайдених документів : 1
1.

Melnyk V. 
Static Analysis of Source Code Modeled for Java-Programs Containing Applications with Android Security [Електронний ресурс] / V. Melnyk, K. Melnyk, O. Zhyharevych // Proсeedings of the National Aviation University. - 2015. - № 2. - С. 46-53. - Режим доступу: http://nbuv.gov.ua/UJRN/Vnau_2015_2_9
Здійснено поєднання методів статичного аналізу з моделлю дедуктивної перевірки й використанням рішень теорії статичної моделі (ТСМ) для створення основи, яка, враховуючи аспект аналізу вихідного коду, автоматично створюється за допомогою аналізатора, котрий виводить кінцеву інформацію про цей аспект. Аналізатор генерується шляхом перекладу програми для збору семантики з метою викладення формул в першому наближенні на основі кількох представлених теорій. Оскільки програма здійснює імпорт пакетів і використовує класові методи цих пакетів, вона імпортує семантику викликів API в наближенні першого порядку. Аналізатор, використовуючи ці наближення як моделі та їх формули першого порядку, залучає поведінку специфікації (його негативність) описаної програми. Рішення SMT-LIB формул розглядається як комбінована формула для того, щоб їх "обмежувати" та "розв'язувати". Форма "розв'язку" може використовуватися для ідентифікації логічних помилок (безпеки) Java-програм на базі Android. Властивості безпеки Android представлено як обмежувальні аналітичні цілі, щоб показати важливість цих обмежень.
Попередній перегляд:   Завантажити - 289.411 Kb    Зміст випуску    Реферативна БД     Цитування
 
Відділ наукової організації електронних інформаційних ресурсів
Пам`ятка користувача

Всі права захищені © Національна бібліотека України імені В. І. Вернадського