Mechanically Proved Practical Local Null Safety

Null pointer dereferencing is a well-known bug in object-oriented programs. It can be avoided by adding special validity rules to a language in which programs are written. Are the rules sufficient to ensure absence of such exceptions? This work focuses on null safety for intra-procedural context whe...

Full description

Bibliographic Details
Published in:	Труды Института системного программирования РАН
Main Author:	A. V. Kogtenkov
Format:	Article
Language:	English
Published:	Russian Academy of Sciences, Ivannikov Institute for System Programming 2018-10-01
Subjects:	безопасность пустых указателей статический анализ eiffel формальные методы крупношаговая операционная семантика теорема о сохранении эквивалентность операционных семантик
Online Access:	https://ispranproceedings.elpub.ru/jour/article/view/168

Similar Items

Null safety benchmarks for object initialization
by: A. V. Kogtenkov
Published: (2018-10-01)

Static Verification Tools for C Programs and Linux Device Drivers: A Survey
by: M. U. Mandrykin, et al.
Published: (2018-10-01)

Component-based verification of operating systems
by: V. V. Kuliamin, et al.
Published: (2019-02-01)

Conformance testing of Extensible Authentication Protocol implementations
by: A. V. Nikeshin, et al.
Published: (2019-02-01)

Deductive Verification of Telecommunication Systems Written in C
by: I. S. Anureev
Published: (2012-01-01)

Intelligent Design of Class Structure Model based on Ontological Data Analysis
by: A. N. Kovartsev, et al.
Published: (2018-10-01)

Applying High-Level Function Loop Invariants for Machine Code Deductive Verification
by: Pavel Andreevitch Putro
Published: (2019-09-01)

Platform for interprocedural static analysis of binary code
by: H. K. Aslanyan
Published: (2018-12-01)

On the problem of representation of the formal model of security policy for operating systems
by: P. N. Devyanin
Published: (2018-10-01)

ADV_SPM - Formal security policy models in practice
by: A. V. Khoroshilov, et al.
Published: (2018-10-01)

Buffer Overflow Detection via Static Analysis: Expectations vs. Reality
by: I. A. Dudina
Published: (2018-10-01)

An approach of reachability determination for static analysis defects with help of dynamic symbolic execution
by: A. Y. Gerasimov, et al.
Published: (2018-10-01)

An approach to the C string analysis for buffer overflow detection
by: I. A. Dudina, et al.
Published: (2018-12-01)

Combining ACSL Specifications and Machine Code
by: P. A. Putro
Published: (2018-10-01)

Model-based testing of Internet Mail Protocols
by: N. V. Pakulin, et al.
Published: (2018-10-01)

Input data generation for reaching specific function in program by iterative dynamic analysis
by: A. Y. Gerasimov, et al.
Published: (2018-10-01)

Vulnerabilities Detection via Static Taint Analysis
by: Nikita Vladimirovitch Chimtchik, et al.
Published: (2019-09-01)

Using different views java-programs for static analysis
by: E. A. Karpulevitch
Published: (2018-10-01)

Supporting Java programming in the Svace static analyzer
by: A. P. Merkulov, et al.
Published: (2018-10-01)

Modeling operational semantics of machine instructions
by: V. A. Padaryan, et al.
Published: (2018-10-01)

Using static analysis for finding security vulnerabilities and critical errors in source code
by: Arutyun Avetisyan, et al.
Published: (2018-10-01)

Survey on static program analysis results refinement approaches
by: A. Y. Gerasimov
Published: (2018-10-01)

TLS clients testing
by: A. V. Nikeshin, et al.
Published: (2018-10-01)

Methods and software tools for combined binary code analysis
by: V. A. Padaryan, et al.
Published: (2018-10-01)

Analysis of program changes nature and searching for unpatched code fragments
by: Mariam Seropovna Arutunian, et al.
Published: (2019-04-01)

Test Suite development for verification of TLS security protocol
by: A. V. Nikeshin, et al.
Published: (2018-10-01)

Automation of conformance testing for communication protocols
by: Nikolay Pakulin, et al.
Published: (2018-10-01)

Static analyzer Svace for finding of defects in program source code
by: V. P. Ivannikov, et al.
Published: (2018-10-01)

Interprocedural taint analysis for LLVM-bitcode
by: V. K. Koshelev, et al.
Published: (2018-10-01)

Computing Transition Priorities for Live Petri Nets
by: Kirill Gennadievitch Serebrennikov
Published: (2019-10-01)

Formalization of Error Criteria for static symbolic execution
by: V. K. Koshelev
Published: (2018-10-01)

The refactoring approach used in Klocwork Insight toolkit
by: N. L. Lugovskoy
Published: (2018-10-01)

Refactoring on the whole project
by: S. V. Syromyatnikov, et al.
Published: (2018-10-01)

Adjustable method with predicate abstraction for detection of race conditions in operating systems
by: P. S. Andrianov, et al.
Published: (2018-10-01)

Verification and analysis of variable operating systems
by: V. V. Kuliamin, et al.
Published: (2018-10-01)

Automatic C Program Verification Based on Mixed Axiomatic Semantics
by: I. V. Maryasov, et al.
Published: (2013-01-01)

Using unreachable code analysis in static analysis tool for finding defects in source code
by: R. R. Mulyukov, et al.
Published: (2018-10-01)

Evolution of the Linux kernel
by: E. M. Novikov
Published: (2018-10-01)

Prosega/CPN: An Extension of CPN Tools for Automata-based Analysis and System Verification
by: J. C. Carrasquel, et al.
Published: (2018-10-01)

A static approach to estimation of execution time of components in AADL models
by: A. M. Troitskiy, et al.
Published: (2018-10-01)