scholarly journals VERIFICATION OF A PREDICATE HEAPSORT PROGRAM USING INVERSE TRANSFORMATIONS

2020 ◽  
Author(s):  
Vladimir Ivanovich Shelekhov ◽  
Keyword(s):  
Programming Language ◽  
Array Element ◽  
Deductive Verification ◽  
Arbitrary Type

Deductive verification of the classical J.Williams heapsort algorithm for objects of an arbitrary type was conducted. In order to simplify verification, non-trivial transformations, replacing pointer arithmetic operators by an array element constructs, were applied. The program was translated to the predicate programming language. Deductive verification of the program in the tools Why3 and Coq appears to be complicated and time consuming.

scholarly journals TRANSFORMATION, SPECIFICATION, AND VERIFICATION OF THE PROGRAM CALCULATING THE ELEMENTS NUMBER OF A SET PRESENTED BY A BIT VECTOR

2020 ◽  
Author(s):  
Erdem Garmayevich Tumurov ◽  
◽  
Vladimir Ivanovich Shelekhov ◽  
Keyword(s):  
Programming Language ◽  
Program Model ◽  
Linux Kernel ◽  
Deductive Verification ◽  
Specification And Verification ◽  
Bit Vector

Transformations eliminating pointers in the memweight function in OS Linux kernel library is described. Next, the function is translated to the predicate programming language P. For the obtained predicate program, deductive verification in the Why3 tool was performed. In order to simplify verification, the program model of calculating program inner state was constructed.

scholarly journals Deductive Verification of Floating-Point Java Programs in KeY

2021 ◽  
pp. 242-261
Author(s):  
Rosa Abbasi ◽  
Jonas Schiffl ◽  
Eva Darulova ◽  
Mattias Ulbrich ◽  
Wolfgang Ahrendt
Keyword(s):  
Programming Language ◽  
Floating Point ◽  
Deductive Verification ◽  
Java Programming ◽  
Special Values ◽  
Floating Point Arithmetic ◽  
Smt Solvers ◽  
Java Programs ◽  
Transcendental Functions ◽  
Point Arithmetic

AbstractDeductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due to rounding as well as the presence of the special values infinity and ‘Not a Number’ (NaN). In this paper, we present the first floating-point support in a deductive verification tool for the Java programming language. Our support in the KeY verifier handles arithmetic via floating-point decision procedures inside SMT solvers and transcendental functions via axiomatization. We evaluate this integration on new benchmarks, and show that this approach is powerful enough to prove the absence of floating-point special values—often a prerequisite for further reasoning about numerical computations—as well as certain functional properties for realistic benchmarks.

scholarly journals Scalability and precision by combining expressive type systems and deductive verification

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-29
Author(s):  
Florian Lanzinger ◽  
Alexander Weigl ◽  
Mattias Ulbrich ◽  
Werner Dietl
Keyword(s):  
Programming Language ◽  
Program Verification ◽  
Type Systems ◽  
The Other ◽  
Deductive Verification ◽  
Java Programming ◽  
Verification Tool ◽  
Novel Approach ◽  
Typical Type

Type systems and modern type checkers can be used very successfully to obtain formal correctness guarantees with little specification overhead. However, type systems in practical scenarios have to trade precision for decidability and scalability. Tools for deductive verification, on the other hand, can prove general properties in more cases than a typical type checker can, but they do not scale well. We present a method to complement the scalability of expressive type systems with the precision of deductive program verification approaches. This is achieved by translating the type uses whose correctness the type checker cannot prove into assertions in a specification language, which can be dealt with by a deductive verification tool. Type uses whose correctness the type checker can prove are instead turned into assumptions to aid the verification tool in finding a proof.Our novel approach is introduced both conceptually for a simple imperative language, and practically by a concrete implementation for the Java programming language. The usefulness and power of our approach has been evaluated by discharging known false positives from a real-world program and by a small case study.

Towards verification of scientific and engineering programs. The CPPS project

2020 ◽  
pp. 91-106
Author(s):  
Дмитрий Алексеевич Кондратьев ◽  
Алексей Владимирович Промский
Keyword(s):  
Parallel Programming ◽  
Program Verification ◽  
Array Element ◽  
Programming System ◽  
Deductive Verification ◽  
Engineering Applications ◽  
Engineering Programs ◽  
Domain Specific ◽  
Axiomatic Semantics ◽  
Engineering Mathematics

В настоящее время, когда теоретические основы верификации программ хорошо изучены, исследователи концентрируют свои усилия на предметно-ориентированных методах для различных классов программ. Инструменты, которые они выбирают, варьируются от проверки моделей для сетевых протоколов до исчислений указателей для фрагментов ядра операционной системы. Однако, похоже, что области научных и инженерных программ все еще уделяется недостаточно внимания. Мы хотели бы внести свой вклад в заполнение этого пробела с помощью разработки системы CPPS. Целью этого проекта является создание системы параллельного программирования для Sisal-программ. Дедуктивная верификация Sisal-программ является одной из важных подцелей. Так как язык Cloud-Sisal построен на основе циклических выражений, их аксиоматическая семантика является базой логики Хоара для языка Sisal. Циклические выражения языка Cloud-Sisal, выражения конструирования массивов и выражения замещения элементов массивов позволяют реализовать эффективно исполняемые программы вычислительной или инженерной математики. Таким образом, мы полагаем, что наша аксиоматическая семантика для этих типов выражений может представлять интересный результат. Природа таких программ позволяет достичь не только эффективного исполнения, но и упростить верификацию. Действительно, программы вычислительной математики часто основаны на итерациях над структурами данных. Символический метод верификации финитных итераций является в этой ситуации очень полезным, так как он элиминирует те проблемные инварианты цикла, которые всегда мешают формальной верификации. Все предыдущие исследования этого метода были теоретическими, CPPS представляет собой первую попытку использования его на практике. Nowadays, when formal fundamentals of program verification are well studied, researchers concentrate their efforts on domain-specific methods for various classes of programs. However, it seems that the field of scientific and engineering applications still lacks attention. We would like to contribute to filling this gap through the development of the Cloud Parallel Programming System (CPPS). The goal of this project is to create a parallel programming system for Sisal programs. Deductive verification of Sisal programs is one the of important subgoals. Since the Cloud Sisal language is built on the basis of loop expressions, their axiomatic semantics is the basis of Hoare’s logic for the Sisal language. The Cloud Sisal loop expressions, array construction expressions and array element replacement expressions enable efficiently executable computational or engineering mathematics programs. Thus, we believe that our axiomatic semantics for these types of expressions may present an interesting result.

Programming Language for Severely Retarded Children

1978 ◽  
Vol 9 (4) ◽  
pp. 213-219
Author(s):  
Carol McCall Davis
Keyword(s):  
Programming Language ◽  
Mentally Retarded ◽  
Mentally Retarded Children

This article describes methods of language programming for profoundly mentally retarded children that are based on linguistic principles. Examples of program contents are drawn from research reports and include cuing procedures, as well as progress from receptive through imitative behaviors, labeling responses, and grammatical sequencing.

PENGELOLAAN DATA ANGGOTA BERBASIS WEBSITE DI YAMAHA VIXION CLUB CABANG BANDUNG

2020 ◽  
Vol 2 (2) ◽  
pp. 113-127
Author(s):  
Nova Indrayana Yusman
Keyword(s):  
Data Management ◽  
Organizational Structure ◽  
Human Resource Development ◽  
Human Resource ◽  
Programming Language ◽  
The Internet ◽  
Web Based ◽  
Management Software ◽  
The City ◽  
Data Management Software

Yamaha Vixion Club Bandung (YVCB) was formed on July 7, 2007 in the city of Bandung, as a place of friendship between Yamaha Vixion motorcyclists. In its organizational structure, YVCB has a Human Resource Development (HRD) division. Until now, there are more than 800 Yamaha Vixion Club Bandung members. This software is made to facilitate the work of the Yamaha Vixion Club Bandung HRD Division in processing member data. Created using Microsoft Webmatrix as an editor with the PHP programming language. The database uses MySQL with PHPMyAdmin as the software. The method used in making this software is prototyping so that between developers and customers can understand each other what the customer wants. The purpose of making web-based member data management software is that in terms of managing member data it can be done anytime and anywhere by just accessing the internet. In the use of the program, the author chose to use PHP, because PHP is the best and easiest to use in website programming language. Based on the last paragraph, the author intends to make aplication based computerized attendance so that become effective and efficient in terms of time.

SMART and TOPSIS Method For Determining The Priority Of Screen Printing

SinkrOn ◽  
2020 ◽  
Vol 4 (2) ◽  
pp. 151
Author(s):  
Rinaldi Setiawan ◽  
Arini Arini ◽  
Luh Kesuma Wardhani
Keyword(s):  
Decision Support ◽  
Programming Language ◽  
Screen Printing ◽  
Small And Medium Enterprises ◽  
Topsis Method ◽  
Product Selection ◽  
Final Value ◽  
Combination Of Methods ◽  
Medium Enterprises ◽  
Research Criteria

The number of micro, small and medium enterprises (MSMEs) in the field of screen printing and convection that use websites in marketing is one of them CV. Ini Sablon. but in the production process there are obstacles in working on orders that come to be done first in accordance with predetermined criteria, namely deadlines, number of orders, design, profit, and availability of goods. The use of Decision Support System (DSS) aims to provide recommendations to owners of screen printing companies. This study uses the SMART method to weight the criteria and the TOPSIS method for product selection. This system is built using the PHP programming language and MySQL database. The results of the study were a screen printing production priority website with the best final value of 0.62 and the worst final value of 0.35 with the level of accuracy between manual and system calculations reaching 100%. In this study the criteria cannot be updated, it is expected that further research criteria can be updated and use a combination of methods that have not been done.

Sign in / Sign up

Export Citation Format

Share Document