Framework for evaluating loop invariantdetection games in relation to automateddynamic invariant detectors
Başlık çevirisi mevcut değil.
- Tez No: 726060
- Danışmanlar: DR. GEOFFREY G. XİE, DR. GLENN COOK
- Tez Türü: Yüksek Lisans
- Konular: Savunma ve Savunma Teknolojileri, Defense and Defense Technologies
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2015
- Dil: İngilizce
- Üniversite: The Naval Postgraduate School
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Belirtilmemiş.
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: Belirtilmemiş.
Özet
Özet yok.
Özet (Çeviri)
Software has a huge and negative impact on the economy. Formal verification is an effective method to check whether a piece of software contains certain kinds of errors. Defense Advanced Research Projects Agency (DARPA) started the Crowd Sourced Formal Verification (CSFV) program to propose a new model for formal verification by using five online games. CSFV aims to explore whether an online game player with no formal verification expertise can achieve formal verification more efficiently than through conventional processes. We observe that, currently, no quality criteria exist to measure CSFV gamers' efforts. The study suggests that machine detectability of a solution detected by a gamer indicates poor quality for that solution. The solutions in one of the games, StormBound, were selected for examination. An automated tool was developed to check the machine detectability of the solutions, and 78 percent of the assertions were seen to be machine detectable.
Benzer Tezler
- Mimarlıkta döngüsel tasarım yaklaşımı: Karar verme mekanizmaları için kavramsal bir çerçeve
Advancing circular design in architecture: A framework for decision-making mechanisms
AYŞE CEYLİN CEYDA HÜNDAL
- A game-theoretical approach for analyzing effects of combined control on freeway traffic: Case of integrated ramp metering and variable speed limiting
Oyun teorisi yaklaşımı ile bütünleşik kontrolün otoyol trafiği üzerindeki etkisinin incelenmesi: Bütünleşik katılım denetimi ve değişken hız kısıtı örneği
MUHAMMED ADEMOĞLU
Yüksek Lisans
İngilizce
2024
İstanbul Teknik Üniversitesiİnşaat Mühendisliği Ana Bilim Dalı
Yükleniyor...
- Development of a modular pulmonary resuscitation device for chronic and acute respiratory support
Kronik ve akut solunum desteği için modüler pulmoner resüsitasyon cihazının geliştirilmesi
MUNAM ARSHAD
- Kültürel miras yapılarının sayısallaştırılması ve HBIM modeline dönüşümü
Digitization of cultural heritage buildings and their conversion into HBIM models
HANDAN AŞ ÇEMREK
Yüksek Lisans
Türkçe
2026
Mimar Sinan Güzel Sanatlar ÜniversitesiEnformatik Ana Bilim Dalı
Yükleniyor...
- Seramik sanayide kaynak verimliliği ve temiz üretim
Resource efficiency and cleaner production in the ceramic industry
YAĞMUR ÇELİK SAYDAM
Yüksek Lisans
Türkçe
2025
Bilecik Şeyh Edebali ÜniversitesiKimya Mühendisliği Ana Bilim Dalı
Yükleniyor...