Hasil Pencarian  ::  Simpan CSV :: Kembali

"HOL is a theorem prover based on a higher order logic. Its expressive logic makes it suitable for embedding programming logics. Compared to other theorem provers, HOL is attractive because of its familiar and intuitive logic and because it is highly programmable. In this paper we will compare a number of commonly used embedding approaches in HOL and outline their strength and weakness. We will also outline a new alternative called hybrid embedding that combines the strength of other approaches, though some price will have to be paid. "

"Pada pengembangan sistem, dibutuhkan sebuah mekanisme untuk menjamin bahwa sistem tersebut berjalan dengan benar tanpa error atau rsquo;bug rsquo;. Sejauh ini, hal yang biasa dilakukan adalah dengan testing, tetapi hal ini sulit dilakukan untuk mencakup semua kemungkinan. Untuk sistem yang membutuhkan tingkat correctness yang tinggi, seperti misalnya pada hardware , perlu mekanisme yang dapat menjamin kebenaran program untuk semua kemungkinan input. Ada solusi lain yang dapat menjamin kebenaran program untuk semua kemungkinan input, yaitu dengan verifikasi formal. Verifikasi formal dilakukan dengan pemodelan matematika. Salah satu sistem yang membutuhkan tingkat correctness yang tinggi adalah sistem bilangan floating-point. Hal ini terkait dengan pengalaman yang dialami Intel pada tahun 1994. Salah satu bahasa standar dalam membangun sebuah sistem digital atau hardware adalah VHDL. Ada beberapa tools yang bisa dilakukan untuk verifikasi formal, salah satunya adalah HOL theorem prover. Penelitian ini melakukan formalisasi operasi aritmatika VHDL dan konstruksi terkait yang dilakukan dengan menggunakan HOL Theorem Prover. Hasilnya adalah sebuah framework yang berisi formalisasi beberapa algoritma aritmatika dasar VHDL dan konstruksi terkaitnya. Framework ini kemudian dapat digunakan untuk memverifikasi modul VHDL yang memanfaatkan aritmatika VHDL dan konstruksi terkaitnya.

---

In system development, a mechanism is needed to ensure that the system runs correctly without error or rsquo bug rsquo . So far, testing is a common solution, but it rsquo s hard to cover all error possibilities. For systems that require a high level of correctness, such as hardware systems, there is a need for a mechanism that can ensure the correctness of the program for all possible inputs. There is another solution to do the task, i.e. by formal verification. Formal verification is done by mathematical modeling. One system that requires a high level of correctness is the floating point number system. This is related to the experience of Intel in 1994.

One of the standard languages in developing a digital system or a hardware is VHDL. There are several tools that can be used for formal verification, one of which is HOL Theorem Prover. This research conducts a formalization of VHDL arithmetic operation and the related constructions done by using HOL Theorem Prover. The result is a framework which contains the formalization of some basic VHDL arithmetic algorithms and the related constructions. This framework can then be used to verify VHDL modules that utilize the VHDL arithmetic and the related constructs."

"Membangun piranti lunak tidaklah sulit, yang sulit adalah bagaimana membangun piranti lunak sesuai dengan spesifikasi yang ada. Kesalahan sering terjadi ketika pengembang tidak atau kurang memperhatikan spesifikasi pada awal pengembangan dan hanya memperhatikan hasil akhir saja. Kesalahan ini akan terus berlanjut sampai pada tahap piranti tersebut diuji coba. Penemuan kesalahan di akhir proses tentu memakan biaya lebih besar jika dibandingkan pada awal proses. Lingu merupakan bahasa baru untuk aplikasi basis data yang dapat melakukan verifikasi program dengan bantuan theorem prover HOL. Tujuan dari verifikasi program adalah memberikan jaminan bahwa program yang dibuat telah sesuai dengan spesifikasi yang diberikan. Dengan adanya jaminan tersebut, pengembang dapat melanjutkan proses pembuatan piranti lunak hingga tahap terakhir. Saat ini, Lingu hanya memfokuskan diri pada aplikasi basis data. Aplikasi basis data merupakan aplikasi yang dekat dengan kehidupan sehari-hari. SET (Student Entrance Test atau Ujian Penerimaan Mahasiswa) merupakan salah satu aplikasi krusial basis data. Kesalahan dalam SET membawa dampak besar bagi calon mahasiswa, sehingga pembangunan SET tidak boleh sembarangan dan harus memperhatikan spesifikasi-spesifikasi tertentu yang menjadi perhatian penting dalam proses seleksi masuk. Tugas akhir ini bertujuan untuk memberikan wawasan baru dalam membangunpiranti lunak dan memverifikasi program dengan menggunakan Lingu. Studi kasus menggunakan SET. Analisis dilakukan terhadap perbandingan Lingu..."

"

Penelitian ini mencari dosen pakar di Fakultas Ilmu Komputer Universitas Indonesia (Fasilkom UI) dengan menggunakan data abstrak dan metadata tugas akhir mahasiswa Fasilkom UI menggunakan teknik information retrieval. Pencarian pakar dilakukan tanpa query expansion dan dengan query expansion. Metode yang digunakan untuk mencari dosen pakar adalah metode berbasis BM25 serta kombinasi antara word2vec dan doc2vec, yang merupakan word embedding dan document embedding. Teknik yang digunakan untuk mengatasi masalah vocabulary mismatch adalah teknik query expansion dengan pendekatan statistik, semantik, serta hybrid. Kontribusi penelitian ini adalah 2 metode baru untuk pencarian pakar tanpa query expansion, 6 jenis kombinasi relasi ontologi berdasarkan concept hierarchy ACM CCS 2012 untuk mengekspansi kueri, serta 14 jenis kombinasi antara metode query expansion berbasis embedding dan ontologi. Evaluasi dari hasil pencarian pakar dilakukan dengan menghitung binary relevance berdasarkan human judgment. Pada penelitian ini, metode pencarian pakar tanpa query expansion dengan hasil yang paling baik adalah metode BM25-sum dengan nilai AP@5 sebesar 0.648. Pencarian pakar dengan berbagai macam jenis query expansion tidak dapat meningkatkan performa retrieval tanpa query expansion secara signifikan, tetapi pencarian dengan query expansion menggunakan metode berbasis embedding, yaitu w2v-w2v memiliki nilai AP@5 sebesar 0.696, yang lebih tinggi dari skor AP@5 dari BM25-sum tanpa query expansion. Pencarian pakar dengan query expansion berbasis ontologi serta hybrid mampu menghasilkan skor AP@5 setinggi 0.664. Skor tersebut tidak setinggi pencarian dengan query expansion dengan w2v-w2v, namun hasilnya lebih baik dari pencarian tanpa query expansion.

---

This research searches for expert lecturers in the Faculty of Computer Science, Universitas Indonesia (Fasilkom UI) with information retrieval techniques using students’ thesis abstract and metadata. The retrieval process is done without and with query expansion. The methods used to find expert lecturers are BM25-based methods as well as combinations between word2vec and doc2vec, which are word embedding and document embedding. We performed query expansion using statistical, semantic, and hybrid approaches to solve vocabulary mismatch problems. This research’s contributions are 2 new methods to retrieve experts without query expansion, 6 types of ontological relations based on the ACM CCS 2012 concept hierarchy to expand queries, and 14 types of combinations between embedding-based and ontology-based query expansion methods. The expert retrieval result is evaluated by calculating binary relevance based on human judgment. Expert search method without query expansion that produces the best result in this research is the BM25-sum method, with an AP@5 score of 0.648. Even though expert retrieval with various query expansion methods does not increase the performance of retrieval without query expansion significantly, the expert search method with embedding-based query expansion method, i.e. w2v-w2v, achieved an AP@5 score of 0.696, which is higher than that of BM25-sum without query expansion. Ontology-based and hybrid query expansion expert search methods managed to score 0.664 for AP@5. This score is not as high as that of w2v-w2v, but the result is still better than that of retrieval without query expansion.

"