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 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.

On the Formal Specification and Verification of Multi-Agent Systems

1997 ◽  
Vol 06 (01) ◽  
pp. 37-65 ◽  
Author(s):  
Michael Fisher ◽  
Michael Wooldridge
Keyword(s):  
Programming Language ◽  
Formal Specification ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Agent Programming ◽  
Formal Specification And Verification ◽  
Multi Agent ◽  
Specification And Verification

This article describes first steps towards the formal specification and verification of multi-agent systems, through the use of temporal belief logics. The article first describes Concurrent METATEM, a multi-agent programming language, and then develops a logic that may be used to reason about Concurrent METATEM systems. The utility of this logic for specifying and verifying Concurrent METATEM systems is demonstrated through a number of examples. The article concludes with a brief discussion on the wider implications of the work, and in particular on the use of similar logics for reasoning about multi-agent systems in general.

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.

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.

Sign in / Sign up

Export Citation Format

Share Document