4 citations · 13 across the 10 of their papers we have counts for
10 papers
A Logical Programming Language as an Instrument for Specifying and Verifying Dynamic Memory
René Haberland
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, altere…
Using Prolog for Transforming XML Documents
René Haberland
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 XS…
Narrowing Down XML Template Expansion and Schema Validation
René Haberland
This work examines how much template instantiation can narrow down schema validation for XML-documents. First, instantiation and validation are formalised. Properties towards their…
Review of Recent Heap Specification and Verification Techniques
René Haberland
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, m…
A Stricter Heap Separating Points-To Logic
René Haberland, Kirill Krinkin
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. V…
Unification of Template-Expansion and XML-Validation
René Haberland
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 co…
Transformation of XML Documents with Prolog
René Haberland, Igor L. Bratchikov
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…
Dynamically Allocated Memory Verification in Object-Oriented Programs using Prolog
René Haberland, Sergey Ivanovskiy
A Prolog-based framework for fully automated verification currently under development for heap-based object-oriented data is introduced. Dynamically allocated issues are discussed,…
Abstract Predicate Entailment over Points-To Heaplets is Syntax Recognition
René Haberland, Kirill Krinkin, Sergey Ivanovskiy
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 c…
A Non-repetitive Logic for Verification of Dynamic Memory with Explicit Heap Conjunction and Disjunction
René Haberland, Kirill Krinkin
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 t…