arXiv subjects

René Haberland

Publications and source records attributed to René Haberland.

10 recordsLinked to original sources

arXiv2022

Review of Recent Heap Specification and Verification Techniques

The article provides an overview of the existing methods of dynamic memory verification; a comparative analysis is carried out; the applicability for solving problems of control, monitoring, and verification of dynamic memory is evaluated. This article is divided into eight sections. The first section introduces formal verification, followed by a section that discusses dynamic memory management problems. The third section discusses Hoare's calculus resumed by heap transformations to the stack. The fifth and sixth sections introduce the concept of dynamic memory shape analysis and the rotation of pointers. The seventh is on separation logic. The last section discusses possible areas of further research, particularly the recognition at recording level of various instances of objects; automation of proofs; "hot" code, that is, software code that updates itself when the program runs; expanding intuitiveness, for instance, on proof explanations.

cs.LO↗

arXiv2021

Using Prolog for Transforming XML Documents

Proponents of the programming language Prolog share the opinion Prolog is more appropriate for transforming XML-documents as other well-established techniques and languages like XSLT. In order to clarify this position this work proposes a tuProlog-styled interpreter for parsing XML-documents into Prolog-internal lists and vice versa for serialising lists into XML-documents. Based on this implementation a comparison between XSLT and Prolog follows. First, criteria are researched, such as considered language features of XSLT, usability and expressibility. These criteria are validated. Second, it is assessed when Prolog distinguishes between input and output parameters towards reversible transformation.

cs.PL↗

arXiv2021

Narrowing Down XML Template Expansion and Schema Validation

This work examines how much template instantiation can narrow down schema validation for XML-documents. First, instantiation and validation are formalised. Properties towards their practical meaning are probed, an implementation is developed. Requirements for an unification are elaborated and a comparison is taken out. The semantics are formulated in terms of denotational semantics as well as rule-based referring to the data models chosen. Formalisation makes it clearer instantiation is adequately represented. Both semantics show, that the rules set for both, instantiation and validation, cannot totally be unified. However, reuse of simplified code also simplifies unification. Implementation allows unification of both processes on document-level. The validity of all implementations is guaranteed by a comprehensive test suite. Analysis shows the minimal XML template language has got regular grammar properties, except macros. An explanation was given, why filters and arrows are not best, especially towards a unified language to be variable and extensive. Recommendations for future language design are provided. Instantiation shows a universal gap in applications, for instance, as seen by XSLT. Lack of expressibility of arbitrary functions in a schema is one such example, expressibility of the command language is another basic restriction. Useful unification constraints are found out to be handy, such as typing each slot. In order to obtain most flexibility out of command languages adaptations are required. An alternative to introducing constraints is the effective construction of special NFAs. Comparison criteria are introduced regarding mainly syntax and semantics. Comparisons is done accordingly. Despite its huge syntax definitions XSD was found weaker than RelaxNG or XML template language. As template language the latter is considered universal.

cs.LO↗

arXiv2021

A Logical Programming Language as an Instrument for Specifying and Verifying Dynamic Memory

This work proposes a Prolog-dialect for the found and prioritised problems on expressibility and automation. Given some given C-like program, if dynamic memory is allocated, altered and freed on runtime, then a description of desired dynamic memory is a heap specification. The check of calculated memory state against a given specification is dynamic memory verification. This contribution only considers formal specification and verification in a Hoare calculus. Issues found include: invalid assignment, (temporary) unavailable data in memory cells, excessive memory allocation, (accidental) heap alteration in unexpected regions and others. Excessive memory allocation is nowadays successfully resolved by memory analysers like Valgrind. Essentially, papers in those areas did not bring any big breakthrough. Possible reasons may also include the decrease of tension due to more available memory and parallel threads. However, starting with Apt, problems related to variable modes have not yet been resolved -- neither entirely nor in an acceptable way. Research contributions over the last decades show again and again that heap issues remain and remain complex and still important. A significant contribution was reached in 2016 by Peter O'Hearn, who accepted the Gödel prize for his parallel approach on a spatial heap operation.

cs.LO↗

arXiv2019

A Stricter Heap Separating Points-To Logic

Dynamic memory issues are hard to locate and may cost much of a development project's efforts and was repeatedly reported similarly afterwards independently by different persons. Verification as one formal method may proof a given program's heap matches a specified dynamic behaviour. Dynamic (or heap) memory, is the region within main memory that is manipulated by program statements like alloc, free and pointer manipulation during program execution. Usually, heap memory is allocated for problems where the amount of used memory is unknown prior to execution. Regions within the heap may be related "somehow" with each other, often, but not always, by pointers containing absolute addresses of related heap cells. The data structure described by all valid pointer variables manifests heap graphs. A heap graph is a directed connected simple graph within the dynamic memory which may contain cycles, and where each vertex represents an unique memory address and every edge links two heap vertices. The heap graph must be pointed by at least one variable from the local stack or a chain of other heap graphs which is finally pointed by at least one stacked variable. Heap vertices may not overlap. A heap formula expresses the assertion on dynamic memory and can either be a heaplet, or a recursively defined heap-spatial or logical formula.

cs.LO↗

arXiv2019

Transformation of XML Documents with Prolog

Transforming XML documents with conventional XML languages, like XSL-T, is disadvantageous because there is too lax abstraction on the target language and it is rather difficult to recognize rule-oriented transformations. Prolog as a programming language of declarative paradigm is especially good for implementation of analysis of formal languages. Prolog seems also to be good for term manipulation, complex schema-transformation and text retrieval. In this report an appropriate model for XML documents is proposed, the basic transformation language for Prolog LTL is defined and the expressiveness power compared with XSL-T is demonstrated, the implementations used throughout are multi paradigmatic.

cs.LO↗

arXiv2019

Unification of Template-Expansion and XML-Validation

The processing of XML documents often includes creation and validation. These two operations are typically performed in two different nodes within a computer network that do not correlate with each other. The process of creation is also called instantiation of a template and can be described by filling a template with data from external repositories. Initial access to arbitrary sources can be formulated as an expression of certain command languages like XPath. Filling means copying invariant element nodes to the target document and unfolding variable parts from a given template. Validation is a descision problem returning true if a given XML document satisfies a schema and false otherwise. The main subject is to find a language that unions the template expansion and the validation. [..].

cs.LO↗

arXiv2019

Dynamically Allocated Memory Verification in Object-Oriented Programs using Prolog

A Prolog-based framework for fully automated verification currently under development for heap-based object-oriented data is introduced. Dynamically allocated issues are discussed, recent approaches and criteria are analysed. The architecture and its components are introduced by example. Finally, propositions to further and related work are given.

cs.LO↗

arXiv2019

Abstract Predicate Entailment over Points-To Heaplets is Syntax Recognition

Abstract predicates are considered in this paper as abstraction technique for heap-separated configurations, and as genuine Prolog predicates which are translated straight into a corresponding formal language grammar used as validation scheme for intermediate heap states. The approach presented is rule-based because the abstract predicates are rule-based, the parsing technique can be interpreted as an automated fold/unfold of the corresponding heap graph.

cs.LO↗

arXiv2019

A Non-repetitive Logic for Verification of Dynamic Memory with Explicit Heap Conjunction and Disjunction

In this paper, we review existing points-to Separation Logics for dynamic memory reasoning and we find that different usages of heap separation tend to be an obstacle. Hence, two total and strict spatial heap operations are proposed upon heap graphs, for conjunction and disjunction -- similar to logical conjuncts. Heap conjunction implies that there exists a free heap vertex to connect to or an explicit destination vertex is provided. Essentially, Burstall's properties do not change. By heap we refer to an arbitrary simple directed graph, which is finite and may contain composite vertices representing class objects. Arbitrary heap memory access is restricted, as well as type punning, late class binding and further restrictions. Properties of the new logic are investigated, and as a result group properties are shown. Both expecting and superficial heaps are specifiable. Equivalence transformations may make denotated heaps inconsistent, although those may be detected and patched by the two generic linear canonization steps presented. The properties help to motivate a later full introduction of a set of equivalences over heap for future work. Partial heaps are considered as a useful specification technique that help to reduce incompleteness issues with specifications. Finally, the logic proposed may be considered for extension for the Object Constraint Language.

cs.LO↗