https://hdl.handle.net/20.500.12809/57 2026-04-15T05:55:50Z 2026-04-15T05:55:50Z Ekici, Burak Viswanathan, Arjun Zohar, Yoni Tinelli, Cesare Barrett, Clark Stanford University https://hdl.handle.net/20.500.12809/11068 2025-05-29T11:30:19Z 2023-01-01T00:00:00Z

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.

2023-01-01T00:00:00Z Doğru, Alperen Can Kaymaz, İbrahim Kandemir, Miray Batikan Seydibeyoğlu, Mehmet Özgür https://hdl.handle.net/20.500.12809/11044 2023-10-26T13:00:05Z 2023-01-01T00:00:00Z

Investigations of the Friction and Wear Resistance of the Natural Fiber-Reinforced Polyamide Composites Doğru, Alperen; Can Kaymaz, İbrahim; Kandemir, Miray Batikan; Seydibeyoğlu, Mehmet Özgür The search for natural and biobased materials to create a sustainable future has led many scientists to conduct research on natural-fiber-reinforced composites. Natural fibers have been used for thousands of years, but in the recent decades, they have been used in polymer composites as a reinforcement and/or filler. Natural fibers provide abundant resource in various countries through many forms. The use of natural fiber for structural composites is important in creating important new uses. Biobased materials are becoming more prominent in various applications including automotive parts and many other machinery. For the mechanical parts, friction and wear has been one of the most important topics for long-term performance of these products. In this book chapter, summary of natural fibers and their applications in polyamide composites has been well documented. The use of these composites has been investigated in terms of friction and wear properties. The wear and friction topics are commonly less studied in academic area, but they have a very significant importance for the industry. It is expected that this chapter will highlight the industrial use of these materials for long-term uses.

2023-01-01T00:00:00Z Taşçıkaraoğlu, Akın Noorzad, Najmuddin Catalao, Joao P. S https://hdl.handle.net/20.500.12809/11041 2023-10-25T12:49:05Z 2023-01-01T00:00:00Z

Economic Operation of a Multi-Energy System Considering the Impacts of Micro-Mobility Taşçıkaraoğlu, Akın; Noorzad, Najmuddin; Catalao, Joao P. S The increasing and uncontrolled demand for energy has led to the emergence of a multi-energy system (MES), which is a promising and efficient way of providing multiple energy services to end-users, such as electricity, heating and cooling. The determination of the optimal MES configuration involves a comprehensive assessment of the entire system, including its various components, load demands, and energy prices. This study focuses on an MES that comprises renewable energy sources (RESs), heat pumps (HPs), combined heat and power units (CHPs), community energy storage (CES), micro-mobility such as electric scooters (e-scooters), and multi-energy demands. To optimize the economic operation of the considered MES, several factors need to be taken into account, especially for considering the impacts of micro-mobility. The target of the study is to maximize the efficiency of the system and minimize the operation costs when the load demands are met. The study also evaluates the optimal operation of the MES, taking the time-of-use (TOU) and non-TOU electricity tariff into account and considering the relevant constraints throughout the operation horizon. Additionally, the economic and charging impacts of e-scooters are evaluated on the system. The proposed optimization algorithm is conducted for different case studies and based on the findings, the simulation results clearly demonstrate the effectiveness of the system.

2023-01-01T00:00:00Z Gül, Murat Bayık, Çağlar Abdikan, Saygın https://hdl.handle.net/20.500.12809/11023 2023-10-17T08:48:29Z 2023-01-01T00:00:00Z

Mass movement evaluation in deformed clastic rock with InSAR technique Gül, Murat; Bayık, Çağlar; Abdikan, Saygın This study uses multitemporal InSAR images to assess different types of mass movements occurring in the Seydikemer (Mugla, SW Turkiye) district. A major highway connecting the Fethiye district and Antalya province and numerous small settlements of various sizes are found in the study area. In terms of summer tourism, they are Turkiye's most well-known locations. Since the 1960s, at least according to official records, mass movements in this area have been known to negatively impact human life. Some areas have even been declared disaster zones for this reason. However, the movement's size, type, and susceptibility to landslides have all been studied in the last 10-15 years. With satellite images and field studies, distinctive lobate-shaped movements were classified as inactive and active. During fieldwork, characteristic features such as rough topography and bending trees were easily observed and indicated extremely slow and large-scale movement. In this study, it was found that movement less than 7-8 mm/year could be classified as 'extremely slow' mass movement like a 'creep', and moving up to 43 mm/year was evaluated as 'very slow' movement and 'earth slide' on a rigid surface. The examined moving masses with lobate geometry are activated by natural factors such as valley slope direction, stream bed flow direction, erosion of the toe of the river valleys, earthquakes, excessive precipitation, or human activities such as road opening. This study is aimed to evaluating different types of mass movements developing in the Seydikemer (Mugla, Turkiye) district by using multitemporal InSAR. It has been determined that moving masses with lobate geometry are activated because of natural factors such as valley slope direction, stream bed flow direction, erosion of the toe of the river valleys, earthquakes, excessive precipitation, or human activities such as road opening, which can be classified as earthflow if they do not encounter an obstacle

2023-01-01T00:00:00Z