Bilgisayar Mühendisliği Bölümü Koleksiyonu

Formal Verification of Bit-Vector Invertibility Conditions in Coq

2025-05-29T11:30:19Z

Formal Verification of Bit-Vector Invertibility Conditions in Coq Ekici, Burak; Viswanathan, Arjun; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark Stanford University We prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors—used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver cvc5— in the Coq proof assistant. Previous work proved many of these in a completely automatic fashion for arbitrary bit-width; however, some were only proved for bit-widths up to 65, even though they are being used to solve formulas over larger bit-widths. In this paper we describe the process of proving a representative subset of these invertibility conditions in Coq. In particular, we describe the BVList library for bit-vectors in Coq, our extensions to it, and proofs of the invertibility conditions.

İnternet Sıkça Sorulan Sorular ve Wiki Yaklaşımı

2023-10-03T10:09:48Z

İnternet Sıkça Sorulan Sorular ve Wiki Yaklaşımı Bekçibaşı, Uğur; Karaarslan, Enis Bilgiye mümkün oldukça farklı kaynaklardan ve hızlı olarak ulaşmak gerekmektedir. Günümüzde bu bilgiye ulaşmamız için gerekli araştırma ve öğrenme yöntemlerine destek olabilecek en etkili, en kolay ulaşılabilir kaynak; İnternettir. Kullanıcılarının interneti etkin kullanabilmeleri, bilgiye ulaşabilmeleri için tanıştırmaya/yönlendirmeye ihtiyaç duyacakları açıktır. Bu bildiride, bu tür bir kılavuz olarak kullanılabilecek "İnternet sıkça sorulan sorular" bilgi kaynağının oluşturulması hedeflenmiştir. Bilginin sınıflandırıldığı ve kolay erişim için çeşitli yöntemlerin kullanılabildiği dinamik bir arayüz hedeflenmiştir. Bu amaçla 'inet-tr çokça sorulan sorular' bölümünün dinamik bir yapıya dönüştürülüp, ilk ve güncel bilgilere kaynak olmasına yönelik tasarım sunulmuştur. Bu çalışmada başlıca hedeflenenler; sıkça sorulan sorular bölümlerinin arama motorlarındaki bulunabilirliklerini yükseltmek, oluşturulacak bölümlerin amacına uygunluğunu/içeriğini belirlemek, veri girişi için kullanılacak yapılarının ve denetimin dinamikliğinin (wiki altyapısı ile) verimini arttırmak ve sıkça sorulan sorular kaynaklarının güncel kalma şartlarını oluşturmaktır.; Nowadays it is a necessity to access the information quickly from various resources. The Internet is the most effective and easily accessible resource which can provide necessary research and learning opportunities to access the information. It is obvious that the users need introduction/guidance to use the Internet efficiently and access the information. In this study, it is aimed to prepare a "frequently asked questions" resource as such guidance. A dynamic interface design is aimed where the information is classified and various methods are used for easy access. For this reason a design is introduced where the 'inet-tr frequently asked questions' section is tailored with a dynamic architecture to provide recent and updated information. Main objectives of this study are to raise the accessibility rate of frequently asked questions sections, determine the suitability/content of the subsections, to increase the dynamic efficiency of the data input and control structure (wiki infrastructure), set conditions to keep the resources of the frequently asked questions up-to-date.

Is ChatGPT Leading Generative AI What is Beyond Expectations?

2023-10-03T10:07:37Z

Is ChatGPT Leading Generative AI What is Beyond Expectations? Aydın, Ömer; Karaarslan, Enis Generative AI has the potential to change the way we do things. The chatbot is one of the most popular implementation areas. Even though companies like Google and Meta had chatbots, ChatGPT became popular as it was made publicly available. Although ChatGPT is still in the early stages of its development, it attracted the attention of people and capital groups. It has taken the public interest; people from different fields, ages, and education levels started using ChatGPT. There have been many trials with ChatGPT. It is possible to see a lot of news and shares on the Internet. The study aims to shed light on what is happening in the literature and get an insight into the user expectations of ChatGPT and Generative AI. We also give information about the competitors of ChatGPT, such as Google’s Bard AI, Claude, Meta’s Wit.ai and Tencent’s HunyuanAide. We describe technical and structural fundamentals and try to shed light on who will win the race. We also shared information about the GPT4 version of OpenAI's ChatGPT. We share the early stage due diligence and current situation analysis for all these points. We examine preprint papers and published articles. We also included striking posts on the LinkedIn platform and a compilation of various blogs and news. We also made use of ChatGPT in editing the content of these resources of this study. We can get an insight into the people's interests through their questions submitted to ChatGPT. We can also understand the capabilities of GPT3, GPT4 and also predict further enhancements.

DEVOUR: Deleterious Variants on Uncovered Regions in Whole-Exome Sequencing

2023-09-25T07:52:14Z

DEVOUR: Deleterious Variants on Uncovered Regions in Whole-Exome Sequencing Türk, Erdem; Ayaz, Akif; Yüksek, Ayhan; Süzek, Barış Ethem The discovery of low-coverage (i.e. uncovered) regions containing clinically significant variants, especially when they are related to the patient's clinical phenotype, is critical for whole-exome sequencing (WES) based clinical diagnosis. Therefore, it is essential to develop tools to identify the existence of clinically important variants in low-coverage regions. Here, we introduce a desktop application, namely DEVOUR (DEleterious Variants On Uncovered Regions), that analyzes read alignments for WES experiments, identifies genomic regions with no or low-coverage (read depth < 5) and then annotates known variants in the low-coverage regions using clinical variant annotation databases. As a proof of concept, DEVOUR was used to analyze a total of 28 samples from a publicly available Hirschsprung disease-related WES project (NCBI Bioproject: https://www.ncbi.nlm.nih.gov/bioproject/?term=PRJEB19327), revealing the potential existence of 98 disease-associated variants in low-coverage regions. DEVOUR is available from https://github.com/projectDevour/DEVOUR under the MIT license