检索结果-内蒙古大学图书馆

Separation Logic Verification of c Programs with an SMT Solver

ELEcTRONIc NOTES IN THEORETIcAL cOMPUTER ScIENcE 2009年 254卷 5-23页

作者： Botincan, Matko Parkinson, Matthew Schulte, Wolfram Univ Zagreb Zagreb Croatia Univ Cambridge Cambridge England Microsoft Res Redmond WA USA

This paper presents a methodology for automated modular verification of c programs against specifications written in separation logic. The distinguishing features of the approach are representation of the c memory model in separation logic by means of rewrite rules suitable for automation and the careful integration of an SMT solver behind the separation logic prover to guide the proof search.

关键词： Separation logic automated verification automated theorem proving c programming language

来源：评论

学校读者我要写书评

暂无评论

VIP: Verifying Real-World c Idioms with Integer-Pointer casts

引用

PROcEEDINGS OF THE AcM ON programming languageS-PAcMPL 2022年第POPL期6卷 1–32页

作者： Lepigre, Rodolphe Sammler, Michael Memarian, Kayvan Krebbers, Robbert Dreyer, Derek Sewell, Peter MPI SWS Saarland Informat Campus Saarbrucken Germany Univ Cambridge Cambridge England Radboud Univ Nijmegen Nijmegen Netherlands

Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level (e.g., bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in c allows, they are performed with the help of integer-pointer casts. Prior work has explored increasingly realistic memory object models for c that account for the desired semantics of integer-pointer casts while also being sound w.r.t. compiler optimisations, culminating in PNVI-ae-udi, the preferred memory object model in ongoing discussions within the ISO WG14 c standards committee. However, its complexity makes it an unappealing target for verification, and no tools currently exist to verify c programs under PNVI-ae-udi. In this paper, we introduce VIP, a newmemory object model aimed at supporting c verification. VIP sidesteps the complexities of PNVI-ae-udi with a simple but effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly. At the same time, we prove VIP compatible with PNVI-ae-udi, thus enabling verification on top of VIP to benefit from PNVI-ae-udi's validation with respect to practice. In particular, we build a verification tool, Refinedc-VIP, for verifying programs under VIP semantics. As the name suggests, Refinedc-VIP extends the recently developed Refinedc tool, which is automated yet also produces foundational proofs in coq. We evaluate Refinedc-VIP on a range of systems-code idioms, and validate VIP's expressiveness via an implementation in the cerberus c semantics.

关键词： c programming language memory model pointer provenance separation logic proof automation Iris coq

来源：评论

学校读者我要写书评

暂无评论

BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs

引用

PROcEEDINGS OF THE AcM ON programming languageS-PAcMPL 2022年第OOPSLA期6卷 1613–1638页

作者： Zhu, Fengmin Sammler, Michael Lepigre, Rodolphe Dreyer, Derek Garg, Deepak MPI SWS Saarland Informat Campus Saarbrucken Germany

Low-level systems code often needs to interact with data, such as page table entries or network packet headers, in which multiple pieces of information are packaged together as bitfield components of a single machine integer and accessed via bitfield manipulations (e.g., shifts and masking). Most existing approaches to verifying such code employ SMT solvers, instantiated with theories for bit vector reasoning: these provide a powerful hammer, but also significantly increase the trusted computing base of the verification toolchain. In this work, we propose an alternative approach to the verification of bitfield-manipulating systems code, which we call BFF. Building on the Refinedc framework, BFF is not only highly automated (as SMT-based approaches are) but also foundationalDi.e., it produces a machine-checked proof of program correctness against a formal semantics for c programs, fully mechanized in coq. Unlike SMT-based approaches, we do not try to solve the general problem of arbitrary bit vector reasoning, but rather observe that real systems code typically accesses bitfields using simple, well-understood programming patterns: the layout of a bit vector is known up front, and its bitfields are accessed in predictable ways through a handful of bitwise operations involving bit masks. correspondingly, we center our approach around the concept of a structured bit vector-i.e., a bit vector with a known bitfield layout-which we use to drive simple and predictable automation. We validate the BFF approach by verifying a range of bitfield-manipulating c functions drawn from real systems code, including page table manipulation code from the Linux kernel and the pKVM hypervisor.

关键词： bitfield manipulation bit vectors c programming language refinement types proof automation coq Iris

来源：评论

学校读者我要写书评

暂无评论

THE AUTOMATED SOLUTION OF 2ND QUANTIZATION EQUATIONS WITH APPLIcATIONS TO THE cOUPLED cLUSTER APPROAcH

引用

THEORETIcA cHIMIcA AcTA 1991年第1期79卷 1-42页

作者： JANSSEN, cL ScHAEFER, HF Center for Computational Quantum Chemistry University of Georgia Athens USA

Theoretical methods in chemistry frequently involve the tedious solution of complex algebraic equations. Then the solutions, sometimes still quite complex, are usually hand-coded by a programmer into an efficient computer language. During this procedure it is all too easy to make an error which will go undetected. A better approach would be to introduce the computer at an even earlier stage in the development of the theory by programming it to first solve the set of equations and then compile the solution into an efficient computer language. In this research a program has been written in the c programming language which can efficiently compute the quasivacuum expectation value of a product of creation and annihilation operators and scalar arrays. The terms in the resulting expressions are then transformed into a canonical form so that all equivalent terms can be combined. Finally, the equations are compiled into a simple representation which can be rapidly interpreted by a Fortran program. This symbol manipulator has been applied to open-shell coupled cluster theory. Two coupled cluster methods using high-spin open-shell references are presented. In one of these methods, the cluster operator contains the unitary group generators, and products thereof, which generate all single and double excitations with respect to the reference. The other uses a simplified cluster operator which generates equations that must be spin-projected. These methods are compared to other descriptions of electron correlation for the cH2 singlet-triplet splitting and the NH2 potential energy surface.

关键词： 2ND QUANTIZATION EQUATIONS cOUPLED cLUSTER APPROAcH ELEcTRONIc STRUcTURE ScHRODINGER EQUATION c programming language

来源：评论

学校读者我要写书评

暂无评论

Discussion on Teaching Innovation of the c language Program of the Noncomputer Specialty

Discussion on Teaching Innovation of the C Language Program ...

引用

4th International conference on computer Science and Education

作者： Wang, Yuanmei Liu, Feng Yangtze Univ Coll Electron & Informat Jinzhou Peoples R China Huazhong Univ Sci & Technol Dept Control Sci & Engn Wuhan Peoples R China

ISBN: (纸本)9781424435197

According to teaching practice, the paper analyzes the problem in teaching of the course of c language programming of noncomputer specialty, declares the method of teaching innovation and discusses the reformation of teaching mode. Practice of teaching innovation has proved that we have achieved better results in training students' ability of thinking and innovation, and improved the teaching goal of the ability of practice.

关键词： c programming language Task Motivation Practice Teaching Teaching Innovation

来源：评论

学校读者我要写书评

暂无评论

ISAAcS - interactive structure analysis of amorphous and crystalline systems

引用

JOURNAL OF APPLIED cRYSTALLOGRAPHY 2010年第1期43卷 181-185页

作者： Le Roux, Sebastien Petkov, Valeri Cent Michigan Univ Dept Phys Mt Pleasant MI 48859 USA

ISAAcS (interactive structure analysis of amorphous and crystalline systems) is a cross-platform program developed to analyze the structural characteristics of three-dimensional structure models built by computer simulations. The models may have any degree of periodicity (i.e. crystallinity) and local symmetry. The following structural information is computed from the models: total and partial radial distribution functions and structure factors for X-ray or neutron scattering, coordination numbers, bond-angle and near atomic neighbor distributions, bond-valence sums, ring statistics, and spherical harmonics invariants. The information may be visualized conveniently and stored for further use.

关键词： Fortran90 c programming language GTK glasses radial distribution functions neutron diffraction/scattering neutron structure factors X-ray diffraction/scattering X-ray structure factors ring statistics spherical harmonics bond valence

来源：评论

学校读者我要写书评

暂无评论

Learning and Practicing Fundamentals of Electrical and computer Engineering through Building and programming a Microcontroller with Multiple Peripherals

Learning and Practicing Fundamentals of Electrical and Compu...

引用

40th Annual Frontiers in Education conference

作者： Song, Jianjian Mu, Xiaoyan Xu, Huihui Yoder, Mark Rose Hulman Inst Technol Terre Haute IN 47803 USA

ISBN: (纸本)9781424462599

A required sophomore course on microcontrollers and computer architecture was designed and offered for the first time in 2009 to expose our electrical engineering (EE) sophomore students to microcontroller-based applications so that they could appreciate and be exposed to fundamentals of electrical and computer engineering (EcE) through hardware and software design and interfacing. The course also helps students to obtain a broad view of various subjects of EcE from circuits, signals, digital logic, microcontrollers, c and assembly language programming to system design, implementation and measurement so that they can make a well informed decision on whether to continue to major in EE. The course builds a foundation for future classes that may require instrumentation or microcontroller-based applications such as those on communications, control, power electronics as well as junior and senior design courses. In addition, the students are required to purchase most of the hardware components for the course so that they can use the components for future projects.

关键词： microcontroller computer architecture sophomore c programming language assembly language

来源：评论

学校读者我要写书评

暂无评论

Tartare: Automatic Generation of c Pointer Statements and Feedback 24

Tartare: Automatic Generation of C Pointer Statements and Fe...

引用

26th Australasian computing Education conference (AcE)

作者： Brieven, Geraldine Baum, Valentin Donnet, Benoit Univ Liege Montefiore Inst Liege Belgium

ISBN: (纸本)9798400716195

This paper addresses the difficulties students face when learning and practicing pointers (i.e., variables storing the memory address of another variable as its value) in a computer programming class. To improve their understanding and practice, we have developed Tartare, an automatic c pointer statement and feedback generator. By creating statements with automatic feedback, students are given the opportunity to practice at will, each time on a different instance. In addition, if the statement must be done remotely and accounts in the final grade, Tartare discourages academic dishonesty since each student faces their own statement to solve. This paper describes the techniques implemented in Tartare, relying on a pattern template-based approach. The statement variety of Tartare is evaluated. Finally, current limitations and further improvements are discussed. We believe our approach for Tartare can be transposed for automatic exercises generation in various other fields.

关键词： c programming language pointers statement generation Tartare

来源：评论

学校读者我要写书评

暂无评论

Signal Analysis Module of Nc Machine Tool Based on c language

Signal Analysis Module of NC Machine Tool Based on C Languag...

引用

International conference on Frontiers of Mechanical Engineering and Materials Engineering (MEME 2012)

作者： cheng, Yao Hu, Youmin Wu, Bo Xuan, Jianping Jia, Guangfei Huazhong Univ Sci & Technol State Key Lab Digital Mfg Equipment & Technol Wuhan 430074 Peoples R China

ISBN: (纸本)9783037854419

In the monitoring of a Nc machine tool (NcMT), signal analysis is one of the most important considerations. In order to process multi-information in a comprehensive way and integrate with Nc systems in a stable way, a signal analysis module (SAM) with various feature parameters programmed in c language is proposed. Experiments are carried out in Huazhong NcMT to verify the validity of the presented SAM. The work described in this paper can be applied to almost all Nc systems and industrial computers with different operating systems (OSs).

关键词： Nc machine tool c programming language Time-frequency domain analysis

来源：评论

学校读者我要写书评

暂无评论

creating Detectors clothes' colors and Presentations for the Visually Impaired

Creating Detectors Clothes' Colors and Presentations for the...

引用

International conference on Science and Technology (TIcST)

作者： Pattanavichai, Santi Pattamavorakun, Suwarin Rajamangala Univ Technol Thanyaburi Fac Sci & Technol Pathum Thani Thailand

ISBN: (纸本)9781467376709

Matching the color of clothing is a challenging task for the visually impaired persons. In this paper, we propose and create the detector which matches color shirt and presentations for impaired vision. The detector is easy to use by using just one button press to manage the operation of the device for display speech output through speaker for the visually impaired persons. The speech output is Thai language only in this detector. The goal of creating a more personal control the color of the image file can be any shade of color on the RGB color with Micro Processor and Micro controller. The image file come from recording by the compact camera and detect by the source code creating by c programming language to filter color and display speech output through speaker from the database on the microprocessor. Finally, the detector for the visually impaired, who can choose the color of clothing that want to put it to work. The prototype is further tested by 20 visually impaired participants in Thomamix Witthaya School for the visually impaired at Phetchaburi Province.

关键词： The Visually Impaired A compact camera RGB color Micro controller Microprocessor c programming language Speaker Detectors clothes' colors

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：