Verification of sequencel programs using Mizar
Başlık çevirisi mevcut değil.
- Tez No: 540537
- Danışmanlar: Dr. NELSON J. RUSTHON
- Tez Türü: Doktora
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2010
- Dil: İngilizce
- Üniversite: Texas Tech University
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Belirtilmemiş.
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 79
Özet
Özet yok.
Özet (Çeviri)
Purely functional language programs are claimed to lend themselves more easily to their proof of correctness. SequenceL, exclusively designed at Texas Tech University, is a strict functional language. There are some proof-assistants used in verification of functional language programs. In this research, we used one of the available proof assistants called Mizar to prove correctness of SequenceL programs. Mizar is based on Tarski-Grothendieck set theory formulated in a first-order language. The Mizar language is human readable compared to other formal systems. It also has some other desirable features for our purposes. The result of this research is a Mizar file that describes a semantics of SequenceL and the framework in which properties of SequenceL programs can be proved. Some examples such as factorial and Euclidian greatest common divisor are given in the Mizar file. Also, a reasonably sized library of proven statements is provided intended to shorten the proofs of properties of SequenceL programs.
Benzer Tezler
- Hibrit üç yönlü periyodik minimal yüzeyli üç boyutlu grafen yapıların mekaniği ve tasarımı
The mechanics and design of hybrid triply periodic minimal surfaces of three dimensional graphene
OSMAN FURKAN YILMAZ
Yüksek Lisans
Türkçe
2022
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
DOÇ. DR. MESUT KIRCA
- Yüksek gerilim yeraltı kablo sistemlerinde tasarım parametrelerinin elektriksel ve termal performansa etkisinin sonlu elemanlar yöntemi ile incelenmesi
Investigation of the effect of design parameters on electrical and thermal performance in high-voltage underground cable systems with fem
YUNUS BERAT DEMİROL
Yüksek Lisans
Türkçe
2024
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiElektrik Mühendisliği Ana Bilim Dalı
PROF. DR. ÖZCAN KALENDERLİ
- CAM sistemlerinin, CNC takım tezgahlarına uygulanması ve postprocessor hazırlanması
Applications of CAM (Computer aided manufacturing) systems for CNC machining tools and developing of postprocessor
ERDAL GAMSIZ
- Networked computing-based system identification and control of electromechanical systems with industrial IoT
Endüstriyel IoT ile elektromekanik sistemlerin ağ hesaplama tabanlı sistem tanıma ve kontrolü
RAMAZAN KAYA
Yüksek Lisans
İngilizce
2024
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiKontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
DOÇ. DR. ALİ FUAT ERGENÇ
- Kalite çemberleri ve TS-ISO 9000 uygulamaları
Quality circles and TS-ISO 9000 practies
MUSA GÜRSOY
Yüksek Lisans
Türkçe
1994
Endüstri ve Endüstri Mühendisliğiİstanbul Teknik ÜniversitesiPROF.DR. ATAÇ SOYSAL