
R. Berghammer, H. Hitoshi, W. Guttmann, P. Höfner:
Relational Characterisations of Paths. In Journal of Logic and Algebraic Methods in Programming, Elsevier, 2020. (accepted)
arXiv: CoRR abs/1801.04026
abstract  bibtex
Abstract:
Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to pointwise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in relation algebras. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in firstorder logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms. All results of this paper are formally verified using Isabelle/HOL.
@article{Hoefner20203,
Author = {Berghammer, R. and Hitoshi, H. and Guttmann, W. and H{\"o}fner, P.},
Title = {Relational Characterisations of Paths},
Journal = {Journal of Logic and Algebraic Methods in Programming},
Year = {2020},
Publisher = {Elsevier},
}

R.J. van Glabbeek, P. Höfner:
Progress, Justness and Fairness. In ACM Computing Surveys 52(4):69:169:38, ACM, 2019.
arXiv: CoRR abs/1810.07414  doi: 10.1145/3329125
abstract  pdf  bibtex
Abstract:
Fairness assumptions are a valuable tool when reasoning about systems. In this paper, we classify several fairness properties found in the literature and argue that most of them are too restrictive for many applications. As an alternative we introduce the concept of justness.
@article{Hoefner20192,
Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Progress, Justness and Fairness},
Journal = {ACM Computing Surveys},
Number = {4},
Volume = {52},
Pages = {69:169:38},
Year = {2019},
Publisher = {ACM},
Doi = {10.1145/3329125}
}

R. Berghammer, N. Danilenko, P. Höfner, I. Stucke:
Cardinality of Relations with Applications. In Discrete Mathematics 339(12):30893115, Elsevier, 2016.
doi: 10.1016/j.disc.2016.06.019
abstract  pdf  bibtex
Abstract:
Based on Y. Kawahara’s characterisation of the cardinality of relations we derive some fundamental properties of cardinalities concerning vectors, points and mappingrelated relations. As applications of these results we verify some properties of linear orders and graphs in a calculational manner. These include the cardinalities of rooted trees and some estimates concerning graph parameters. We also calculationally prove the result of D. Kőnig that in bipartite graphs the matching number equals the vertex cover number.
@article{Hoefner20169,
Author = {Berghammer, R. and Danilenko, N. and H{\"o}fner, P. and Stucke, I.},
Title = {Cardinality of Relations with Applications},
Journal = {Discrete Mathematics},
Number = {12},
Volume = {339},
Pages = {30893115},
Year = {2016},
Publisher = {Elsevier},
Doi = {10.1016/j.disc.2016.06.019}
}

T. Bourke, R.J. van Glabbeek, P. Höfner:
Mechanizing a Process Algebra for Network Protocols. In Journal of Automated Reasoning 56(3):309341, Springer, 2016.
doi: 10.1007/s1081701593589
abstract  pdf  bibtex
Abstract:
This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.
@article{Hoefner20166,
Author = {Bourke, T. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Mechanizing a Process Algebra for Network Protocols},
Journal = {Journal of Automated Reasoning},
Number = {3},
Volume = {56},
Pages = {309341},
Year = {2016},
Publisher = {Springer},
Doi = {10.1007/s1081701593589}
}

R.J. van Glabbeek, P. Höfner, M. Portmann, W.L. Tan:
Modelling and Verifying the AODV Routing Protocol. In Distributed Computing 29(4):279315, Springer, 2016.
arXiv: CoRR abs/1512.08867  doi: 10.1007/s0044601502627
abstract  pdf  bibtex
Abstract:
This paper presents a formal specification of the Ad hoc OnDemand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which has been tailored for the modelling of Mobile Ad Hoc Networks and Wireless Mesh Network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol properties by providing detailed proofs of loop freedom and route correctness.
@article{Hoefner20163,
Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Portmann, M. and Tan, W.L.},
Title = {Modelling and Verifying the {AODV} Routing Protocol},
Journal = {Distributed Computing},
Number = {4},
Volume = {29},
Pages = {279315},
Year = {2016},
Publisher = {Springer},
Doi = {10.1007/s0044601502627}
}

P. Höfner, B. Möller:
Extended Feature Algebra. In Journal of Logic and Algebraic Methods in Programming 85(5):952971, Part 2, Elsevier, 2016.
doi: 10.1016/j.jlamp.2015.12.002
abstract  pdf  bibtex
Abstract:
Feature Algebra was introduced as an abstract framework for featureoriented software development. One goal is to provide a common, clearly defined basis for the key ideas of featureorientation. The algebra captures major aspects of featureorientation, such as the hierarchical structure of features and feature composition. However, as we will show, it is not able to model aspects at the level of code, i.e., situations where code fragments of different features have to be merged. In other words, it does not reflect details of concrete implementations.
In this paper we first present concrete models for the original axioms of Feature Algebra which represent the main concepts of featureoriented programs. This shows that the abstract Feature Algebra can be interpreted in different ways. We then use these models to show that the axioms of Feature Algebra do not properly reflect all aspects of featureorientation from the level of directory structures down to the level of actual code. This gives motivation to extend the abstract algebra, which is the second main contribution of the paper. We modify the axioms and introduce the concept of an Extended Feature Algebra. As third contribution, we introduce more operators to cover concepts like overriding in the abstract setting.
@article{Hoefner20162,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Extended Feature Algebra},
Journal = {Journal of Logic and Algebraic Methods in Programming},
Number = {5},
Volume = {85},
Pages = {952971},
Year = {2016},
Publisher = {Elsevier},
Doi = {10.1016/j.jlamp.2015.12.002}
}

R. Berghammer, P. Höfner, I. Stucke:
Cardinality of Relations and Relational Approximation Algorithms. In Journal of Logic and Algebraic Methods in Programming 85(2):269286, Elsevier, 2016.
doi: 10.1016/j.jlamp.2015.12.001
abstract  pdf  bibtex
Abstract:
First, we discuss three specific classes of relations, which allow to model the essential constituents of graphs, such as vertices and (directed or undirected) edges. Based on Kawahara’s characterisation of the cardinality of relations we then derive fundamental properties on their cardinalities. As main applications of these results, we formally verify four relational programs, which implement approximation algorithms by using the assertionbased method and relationalgebraic calculations.
@article{Hoefner20161,
Author = {Berghammer, R. and H{\"o}fner, P. and Stucke, I.},
Title = {Cardinality of Relations and Relational Approximation Algorithms},
Journal = {Journal of Logic and Algebraic Methods in Programming},
Number = {2},
Volume = {85},
Pages = {269286},
Year = {2016},
Publisher = {Elsevier},
Doi = {10.1016/j.jlamp.2015.12.001}
}

R.J. van Glabbeek, P. Höfner:
CCS: It's not Fair!—Fair Schedulers cannot be implemented in CCSlike languages even under progress and certain fairness assumptions. In Acta Informatica 52(23):175205, Springer, 2015.
arXiv: CoRR abs/1505.05964  doi: 10.1007/s0023601502216
abstract  pdf  bibtex
Abstract:
In the process algebra community it is sometimes suggested that, on some level of abstraction, any distributed system can be modelled in standard processalgebraic specification formalisms like CCS. This sentiment is strengthened by results testifying that CCS, like many similar formalisms, is Turing powerful and provides a mechanism for interaction. This paper counters that sentiment by presenting a simple fair scheduler—one that in suitable variations occurs in many distributed systems—of which no implementation can be expressed in CCS, unless CCS is enriched with a fairness assumption.
Since Dekker's and Peterson's mutual exclusion protocols implement fair schedulers, it follows that these protocols cannot be rendered correctly in CCS without imposing a fairness assumption. Peterson expressed this algorithm correctly in pseudocode without resorting to a fairness assumption, so it furthermore follows that CCS lacks the expressive power to accurately capture such pseudocode.
@article{Hoefner20152,
Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {CCS: It's not Fair!Fair Schedulers cannot be implemented in CCSlike languages even under progress and certain fairness assumptions},
Journal = {Acta Informatica},
Number = {23},
Volume = {52},
Pages = {175205},
Year = {2015},
Publisher = {Springer},
Doi = {10.1007/s0023601502216}
}

D. Batory, P. Höfner, D. Köppl, B. Möller, A. Zelend:
Structured Document Algebra in Action. In Software, Services and Systems  Essays Dedicated to Martin Wirsing on the Occasion of His Emeritation 8950:291311, Springer, 2015.
doi: 10.1007/9783319155456_19
abstract  pdf  bibtex
Abstract:
A Structured Document Algebra (SDA) defines modules with variation points and how such modules compose. The basic operations are module addition and replacement. Repeated addition can create nested module structures. SDA also allows the decomposition of mod ules into smaller parts. In this paper we show how SDA modules can be used to deal algebraically with Software Product Lines (SPLs). In particular, we treat some fundamental concepts of SPLs, such as refine ment and refactoring. This leads to mathematically precise formalization of fundamental concepts used in SPLs, which can be used for improved FeatureOriented Software Development (FOSD) tooling.
@article{Hoefner20151,
Author = {Batory, D. and H{\"o}fner, P. and K{\"o}ppl, D. and M{\"o}ller, B. and Zelend, A.},
Title = {Structured Document Algebra in Action},
Journal = { Software, Services and Systems  Essays Dedicated to Martin Wirsing on the Occasion of His Emeritation},
Volume = {8950},
Pages = {291311},
Year = {2015},
Publisher = {Springer},
Doi = {10.1007/9783319155456_19}
}

P. Höfner, A. McIver:
Hopscotch—Reaching the Target Hop by Hop. In Journal of Logic and Algebraic Methods in Programming 83(2):212224, Elsevier, 2014.
doi: 10.1016/j.jlap.2014.02.009
abstract  pdf  bibtex
Abstract:
Concrete and abstract relation algebras have widespread applications in computer science. One of the most famous is graph theory. Classical relations, however, only reason about connectivity, not about the length of a path between nodes. Generalisations of relation algebra, such as the minplus algebra, use numbers allowing the treatment of weighted graphs. In this way one can for example determine the length of shortest paths (e.g. Dijkstra's algorithm). In this paper we treat matrices that carry even more information, such as the \"next hop\" on a path towards a destination. In this way we can use algebra not only for determining the length of paths, but also the concrete path. We show how paths can be reconstructed from these matrices, hop by hop. We further sketch an application for message passing in wireless networks.
@article{Hoefner20142,
Author = {H{\"o}fner, P. and McIver, A.},
Title = {HopscotchReaching the Target Hop by Hop},
Journal = {Journal of Logic and Algebraic Methods in Programming},
Number = {2},
Volume = {83},
Pages = {212224},
Year = {2014},
Publisher = {Elsevier},
Doi = {10.1016/j.jlap.2014.02.009}
}

P. Höfner, B. Möller:
Dijkstra, Floyd and Warshall meet Kleene. In Formal Aspects of Computing 24(46):459476, Springer, 2012.
doi: 10.1007/s0016501202454
abstract  pdf  bibtex
Abstract:
Around 1960, Dijkstra, Floyd and Warshall published papers on algorithms for solving singlesource and allsources shortest path problems, respectively. These algorithms, nowadays named after their inventors, are well known and well established. This paper sheds an algebraic light on these algorithms. We combine the shortest path problems with Kleene algebra, also known as Conway's regular algebra. This view yields a purely algebraic version of Dijkstra's shortest path algorithm and the one by Floyd/Warshall. Moreover, the algebraic abstraction yields applications of these algorithms to structures different from graphs and pinpoints the mathematical requirements on the underlying cost algebra that ensure their correctness.
@article{Hoefner20124,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {{Dijkstra}, {Floyd} and {Warshall} meet {Kleene}},
Journal = {Formal Aspects of Computing},
Number = {46},
Volume = {24},
Pages = {459476},
Year = {2012},
Publisher = {Springer},
Doi = {10.1007/s0016501202454}
}

P. Höfner, R.J. van Glabbeek, I.J. Hayes:
Morgan: a suitable case for treatment (Preface). In Formal Aspects of Computing 24(46):417422, Springer, 2012. (Festschrift in Honour of Carroll Morgan)
doi: 10.1007/s0016501202570
abstract  pdf  bibtex
Abstract:
The achievements of Professor Charles Carroll Morgan as a scientific expert and a computer scientist are discussed. Carroll, as a computer programmer at Ascomp, worked in 'Laws of Programming' after joining the Programming Research Group. He is also credited to describe large and complex static structures by combining building blocks known as schemas and proposing the notion of Dynamicschemas, which are in line with the building blocks used for static properties, and developed a corresponding calculus. Carroll's book 'Programming from Specifications' is seen as the reference for the refinement calculus and provides a thorough treatment of elementary program constructs which were later incorporated as elements. In 2000 Carroll joined his Alma Mater UNSW as adjunct professor where he worked on operational interpretation of the quantitative μcalculus qMμ as a turnbased game between two players.
@article{Hoefner20123,
Author = {H{\"o}fner, P. and van Glabbeek, R.J. and Hayes, I.J.},
Title = {Morgan: a suitable case for treatment (Preface)},
Journal = {Formal Aspects of Computing},
Number = {46},
Volume = {24},
Pages = {417422},
Year = {2012},
Publisher = {Springer},
Doi = {10.1007/s0016501202570}
}

P. Höfner, B. Möller:
Fixing Zeno Gaps. In Theoretical Computer Science 412(28):33033322, Elsevier, 2011.
doi: j.tcs.2011.03.018
abstract  pdf  bibtex
Abstract:
In computer science fixpoints play a crucial role. Most often least and greatest fixpoints are sufficient. However there are situations where other ones are needed. In this paper we study, on an algebraic base, a special fixpoint of the function f(x) = a⋅x that describes infinite iteration of an element a. We show that the greatest fixpoint is too imprecise. Special problems arise if the iterated element contains the possibility of stepping on the spot (e.g. skip in a programming language) or if it allows Zeno behaviour. We present a construction for a fixpoint that captures these phenomena in a precise way. The theory is presented and motivated using an example from hybrid system analysis.
@article{Hoefner20116,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Fixing Zeno Gaps},
Journal = {Theoretical Computer Science},
Number = {28},
Volume = {412},
Pages = {33033322},
Year = {2011},
Publisher = {Elsevier},
Doi = {j.tcs.2011.03.018}
}

P. Höfner, R. Khedri, B. Möller:
Supplementing Product Families with Behaviour. In International Journal of Software and Informatics 5(12):245266, Part II, Institute of Software, Chinese Academy of Sciences, 2011.
abstract  pdf  bibtex
Abstract:
A common approach to dealing with software requirements volatility is to define product families instead of single products. In earlier papers we have developed an algebra of such families that, roughly, consists in a more abstract view of FODAlike and/or trees of features. A product family is represented by an algebraic term over the feature names that can be manipulated using equational laws such as associativity or distributivity. Initially, only \"syntactic\" models of the algebra were considered, giving more or less just the names of the features used in the various products of a family and certain interrelations such as mandatory occurrence and implication between or mutual exclusion of features, without attaching any kind of \"meaning\" to the features. While this is interesting and useful for determining the variety and number of possible members of such a family, it is wholly insufficient when it comes to talking about the correctness of families in a semantic sense. In the present paper we define a class of \"semantic\" models of the general abstract product family algebra that allow treating very relevant additional questions. In these models, the features of a family are requirements scenarios formalised as pairs of relational specifications of a proposed system and its environment. However, the paper is just intended as a proof of feasibility; we are convinced that the approach can also be employed for different semantic models such as general denotational or streambased semantics.
@article{Hoefner20113,
Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
Title = {Supplementing Product Families with Behaviour},
Journal = {International Journal of Software and Informatics},
Number = {12},
Volume = {5},
Pages = {245266},
Year = {2011},
Publisher = {Institute of Software, Chinese Academy of Sciences},
}

H.H. Dang, P. Höfner, B. Möller:
Algebraic Separation Logic. In Journal of Logic and Algebraic Programming 80(6):221247, Elsevier, 2011.
doi: 10.1016/j.jlap.2011.04.003
abstract  pdf  bibtex
Abstract:
We present an algebraic approach to separation logic. In particular, we give an algebraic characterisation for assertions of separation logic, discuss different classes of assertions and prove abstract laws fully algebraically. After that, we use our algebraic framework to give a relational semantics of the commands of a simple programming language associated with separation logic. On this basis we prove the frame rule in an abstract and concise way, parametric in the operator of separating conjunction, of which two particular variants are discussed. In this we also show how to algebraically formulate the requirement that a command preserves certain variables. The algebraic view does not only yield new insights on separation logic but also shortens proofs due to a point free representation. It is largely firstorder and hence enables the use of offtheshelf automated theorem provers for verifying properties at an abstract level.
@article{Hoefner20112,
Author = {Dang, H.H. and H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Algebraic Separation Logic},
Journal = {Journal of Logic and Algebraic Programming},
Number = {6},
Volume = {80},
Pages = {221247},
Year = {2011},
Publisher = {Elsevier},
Doi = {10.1016/j.jlap.2011.04.003}
}

P. Höfner, R. Khedri, B. Möller:
An Algebra of Product Families. In Software & Systems Modeling 10(2):161182, 2011.
doi: 10.1007/s1027000901272
abstract  pdf  bibtex
Abstract:
Experience from recent years has shown that it is often advantageous not to build a single product but rather a family of similar products that share at least one common functionality while having wellidentified variabilities. Such product families are built from elementary features that reach from hardware parts to software artefacts such as requirements, architectural elements or patterns, components, middleware, or code. We use the well established mathematical structure of idempotent semirings as the basis for a product family algebra that allows a formal treatment of the above notions. A particular application of the algebra concerns the multiview reconciliation problem that arises when complex systems are modelled. We use algebraic integration constraints linking features in one view to features in the same or a different view and show in several examples the suitability of this approach for a wide class of integration constraint formulations. Our approach is illustrated with a Haskell prototype implementation of one particular model of product family algebra.
@article{Hoefner20111,
Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
Title = {An Algebra of Product Families},
Journal = {Software & Systems Modeling},
Number = {2},
Volume = {10},
Pages = {161182},
Year = {2011},
Doi = {10.1007/s1027000901272}
}

P. Höfner, G. Struth:
Algebraic Notions of Nontermination: Omega and Divergence in Idempotent Semirings. In Journal of Logic and Algebraic Programming 79(8):794811, Springer, 2010.
doi: 10.1016/j.jlap.2010.07.016
abstract  pdf  bibtex
Abstract:
Two notions of nontermination are studied and compared in the setting of idempotent semirings: Cohen's omega operator and a divergence operator. They are determined for various computational models, and conditions for their existence and their coincidence are given. It turns out that divergence yields a simple and natural way of modelling infinite behaviours of programs and discrete systems, whereas the omega operator shows some anomalies.
@article{Hoefner20101,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Algebraic Notions of Nontermination: Omega and Divergence in Idempotent Semirings},
Journal = {Journal of Logic and Algebraic Programming},
Number = {8},
Volume = {79},
Pages = {794811},
Year = {2010},
Publisher = {Springer},
Doi = {10.1016/j.jlap.2010.07.016}
}

P. Höfner, G. Struth, G. Sutcliffe:
Automated Verification of Refinement Laws. In Annals of Mathematics and Artificial Intelligence 55(12):3562, Springer, 2009.
doi: 10.1007/s1047200991518
abstract  pdf  bibtex
Abstract:
Demonic refinement algebras are variants of Kleene algebras. Introduced by von Wright as a lightweight variant of the refinement calculus, their intended semantics are positively disjunctive predicate transformers, and their calculus is entirely within firstorder equational logic. So, for the first time, offtheshelf automated theorem proving (ATP) becomes available for refinement proofs. We used ATP to verify a toolkit of basic refinement laws. Based on this toolkit, we then verified two classical complex refinement laws for action systems by ATP: a data refinement law and Back's atomicity refinement law. We also present a refinement law for infinite loops that has been discovered through automated analysis. Our proof experiments not only demonstrate that refinement can effectively be automated, they also compare eleven different ATP systems and suggest that program verification with variants of Kleene algebras yields interesting theorem proving benchmarks. Finally, we apply hypothesis learning techniques that seem indispensable for automating more complex proofs.
@article{Hoefner20092,
Author = {H{\"o}fner, P. and Struth, G. and Sutcliffe, G.},
Title = {Automated Verification of Refinement Laws},
Journal = {Annals of Mathematics and Artificial Intelligence},
Number = {12},
Volume = {55},
Pages = {3562},
Year = {2009},
Publisher = {Springer},
Doi = {10.1007/s1047200991518}
}

P. Höfner, B. Möller:
An Algebra of Hybrid Systems. In Journal of Logic and Algebraic Programming 78(2):7497, Springer, 2009.
doi: 10.1016/j.jlap.2008.08.005
abstract  pdf  bibtex
Abstract:
Hybrid systems are heterogeneous systems characterised by the interaction of discrete and continuous dynamics. We present a trajectorybased algebraic model for describing hybrid systems; the trajectories used are closely related to streams. The algebra is based on left quantales and left semirings and provides a new application for these algebraic structures. We show that hybrid automata, which are probably the standard tool for describing hybrid systems, can conveniently be embedded into our algebra. Moreover we point out some important advantages of the algebraic approach. In particular, we show how to handle Zeno effects, which are excluded by most other authors. The development of the theory is illustrated by a running example and a larger case study.
@article{Hoefner20091,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {An Algebra of Hybrid Systems},
Journal = {Journal of Logic and Algebraic Programming},
Number = {2},
Volume = {78},
Pages = {7497},
Year = {2009},
Publisher = {Springer},
Doi = {10.1016/j.jlap.2008.08.005}
}

P. Höfner, B. Möller:
Algebraic Neighbourhood Logic. In Journal of Logic and Algebraic Programming 76(1):3559, Springer, 2008.
doi: 10.1016/j.jlap.2007.10.004
abstract  pdf  bibtex
Abstract:
We present an algebraic embedding of Neighbourhood Logic (NL) into the framework of semirings which yields various simplifications. For example, some of the NL axioms can be dropped, since they are theorems in our framework, and Galois connections produce properties for free. A further simplification is achieved, since the semiring methods used are easy and fairly standard. Moreover, this embedding allows us to reuse knowledge from Neighbourhood Logic in other areas of Computer Science. Since in its original axiomatisation the logic cannot handle intervals of infinite length and therefore not fully model and specify reactive and hybrid systems, using lazy semirings we introduce an extension of NL to intervals of finite and infinite length. Furthermore, we discuss connections between the (extended) logic and other application areas, like Allen's thirteen relations between intervals, the branching time temporal logic CTL* and hybrid systems.
@article{Hoefner20083,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Algebraic Neighbourhood Logic},
Journal = {Journal of Logic and Algebraic Programming},
Number = {1},
Volume = {76},
Pages = {3559},
Year = {2008},
Publisher = {Springer},
Doi = {10.1016/j.jlap.2007.10.004}
}

P. Höfner, G. Struth:
Can Refinement be Automated?. In Electronic Notes in Theoretical Computer Science 201:197222, Elsevier, 2008.
doi: 10.1016/j.entcs.2008.02.021
abstract  pdf  bibtex
Abstract:
We automatically verify Back's atomicity refinement law and a classical data refinement law for action systems. Our novel approach mechanises a refinement calculus based on Kleene algebras in an off the shelf resolution and paramodulation theorem prover and a counterexample checker with heuristics for hypothesis learning. The proofs are supported by a toolkit of meaningful refinement laws that has also been verified and that, for the first time, allows the refinement of programs and software systems, and the verification of further complex refinement laws, by automated deduction. This suggests that a substantial proportion of refinement could indeed be automated.
@article{Hoefner20082,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Can Refinement be Automated?},
Journal = {Electronic Notes in Theoretical Computer Science},
Volume = {201},
Pages = {197222},
Year = {2008},
Publisher = {Elsevier},
Doi = {10.1016/j.entcs.2008.02.021}
}

P. Höfner, F. Lautenbacher:
Algebraic Structure of Web Services. In Electronic Notes in Theoretical Computer Science 200(3):171187, Elsevier, 2008.
doi: 10.1016/j.entcs.2008.04.099
abstract  pdf  bibtex
Abstract:
Web Services and ServiceOriented Architecture in general are promising concepts to overcome difficulties such as heterogeneity, scalability, etc. In this paper we present an algebraic structure of Web Services which assist users in Web Service composition and formal description of their services. Using relation algebra, tests and iteration offer the possibility of an automatic composition of Web Services based on a specified goal.
@article{Hoefner20081,
Author = {H{\"o}fner, P. and Lautenbacher, F.},
Title = {Algebraic Structure of Web Services},
Journal = {Electronic Notes in Theoretical Computer Science},
Number = {3},
Volume = {200},
Pages = {171187},
Year = {2008},
Publisher = {Elsevier},
Doi = {10.1016/j.entcs.2008.04.099}
}

P. Höfner:
Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic. In Electronic Notes in Theoretical Computer Science 191:4972, Elsevier, 2007.
doi: 10.1016/j.entcs.2006.09.040
abstract  pdf  bibtex
Abstract:
In 1996 Zhou and Hansen proposed a firstorder interval logic called Neighbourhood Logic (NL) for specifying liveness and fairness of computing systems and defining notions of real analysis in terms of expanding modalities. After that, Roy and Zhou developed a sound and relatively complete Duration Calculus as an extension of NL. We present an embedding of NL into an idempotent semiring of intervals. This embedding allows us to extend NL from single intervals to sets of intervals as well as to extend the approach to arbitrary idempotent semirings. We show that most of the required properties follow directly from Galois connections, hence we get many properties for free. As one important result we obtain that some of the axioms which were postulated for NL can be dropped since they are theorems in our generalisation. Furthermore, we discuss other interval operations like Allen's 13 relations between intervals and their relationship to semiring neighbours. Then we present some possible interpretations for neighbours beyond interval settings. Here we discuss for example reachability in graphs and applications to hybrid systems. At the end of the paper we add finite and infinite iteration to NL and extend idempotent semirings to Kleene algebras and ω algebras. These extensions are useful for formulating properties of repetitive procedures like loops.
@article{Hoefner20071,
Author = {H{\"o}fner, P.},
Title = {Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic},
Journal = {Electronic Notes in Theoretical Computer Science},
Volume = {191},
Pages = {4972},
Year = {2007},
Publisher = {Elsevier},
Doi = {10.1016/j.entcs.2006.09.040}
}

J. Drury, P. Höfner, W. Wang:
Formal Models of the OSPF Routing Protocol. In A. Fehnker, H. Garaval (eds.), Models for Formal Analysis of Real Systems (MARS 2020). Electronic Proceedings in Theoretical Computer Science 316, pp. 72120, Open Publishing Association, 2020.
doi: 10.4204/EPTCS.316.4
abstract  pdf  bibtex
Abstract:
We present three formal models of the OSPF routing protocol. The first two are formalised in the timed process algebra TAWN, which is not only tailored for routing protocols, but also specifies protocols in pseudocode that is easily readable. The difference between the two models lies in the level of detail (level of abstraction). From the more abstract model we then generate the third model. It is based on networks of timed automata and can be executed in the model checker Uppaal.
@InProceedings{Hoefner20202,
Author = {Drury, J. and H{\"o}fner, P. and Wang, W.},
Title = {Formal Models of the {OSPF} Routing Protocol},
BookTitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
Editor = {Fehnker, A. and Garaval, H.},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {316},
Pages = {72120},
Year = {2020},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.316.4}
}

R. Barry, R.J. van Glabbeek, P. Höfner:
Formalising the Optimised Link State Routing Protocol. In A. Fehnker, H. Garaval (eds.), Models for Formal Analysis of Real Systems (MARS 2020). Electronic Proceedings in Theoretical Computer Science 316, pp. 4071, Open Publishing Association, 2020.
doi: 10.4204/EPTCS.316.3
abstract  pdf  bibtex
Abstract:
Routing protocol specifications are traditionally written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. Formal methods techniques, such as process algebras, avoid these problems, thus leading to more precise and verifiable descriptions of protocols. In this paper we use the timed process algebra TAWN for modelling the Optimised Link State Routing protocol (OLSR) version 2.
@InProceedings{Hoefner20201,
Author = {Barry, R. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Formalising the Optimised Link State Routing Protocol},
BookTitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
Editor = {Fehnker, A. and Garaval, H.},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {316},
Pages = {4071},
Year = {2020},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.316.3}
}

R.J. van Glabbeek, P. Höfner, M. Markl:
A Process Algebra for Link Layer Protocols. In L. Caires (ed.), Programming Languages and Systems (ESOP 2019). Lecture Notes in Computer Science 11423, pp. 668693, Springer, 2019.
arXiv: CoRR abs/1907.13329  doi: 10.1007/9783030171841_24
abstract  pdf  bibtex
Abstract:
We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling frame collisions. We also formalise suitable liveness properties for link layer protocols specified in this framework. To show applicability we model and analyse two versions of the CarrierSense Multiple Access with Collision Avoidance (CSMA/CA) protocol. Our analysis confirms the hidden station problem for the version without virtual carrier sensing. However, we show that the version with virtual carrier sensing not only overcomes this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.
@InProceedings{Hoefner20193,
Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Markl, M.},
Title = {A Process Algebra for Link Layer Protocols},
BookTitle = {Programming Languages and Systems (ESOP 2019)},
Editor = {Caires, L.},
Series = {Lecture Notes in Computer Science},
Volume = {11423},
Pages = {668693},
Year = {2019},
Publisher = {Springer},
Doi = {10.1007/9783030171841_24}
}

C. Bannister, P. Höfner:
False Failure: Creating Failure Models for Separation Logic. In J. Desharnais, W. Guttmann, S. Joosten (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 2018). Lecture Notes in Computer Science 11194, pp. 263279, Springer, 2018.
doi: 10.1007/9783030021498_16
abstract  pdf  bibtex
Abstract:
Separation logic, an extension of FloydHoare logic, finds countless applications in areas of program verification, but does not allow forward reasoning in the setting of total or generalised correctness. To support forward reasoning, separation logic needs to be equiped with a failure element. We present several ways on how to add such an element. We show that none of the `obvious' extensions preserve all the algebraic properties desired. We develop more complicated models, satisfying the desired properties, and discuss their use for forward reasoning.
@InProceedings{Hoefner20184,
Author = {Bannister, C. and H{\"o}fner, P.},
Title = {False Failure: Creating Failure Models for Separation Logic},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2018)},
Editor = {Desharnais, J. and Guttmann, W. and Joosten, S.},
Series = {Lecture Notes in Computer Science},
Volume = {11194},
Pages = {263279},
Year = {2018},
Publisher = {Springer},
Doi = {10.1007/9783030021498_16}
}

R.J. van Glabbeek, P. Höfner, D. van der Wal:
Analysing AWNspecifications using mCRL2 (extended abstract). In C.A. Furia, K. Winter (eds.), Integrated Formal Methods (iFM 2018). Lecture Notes in Computer Science 11023, pp. 398418, Springer, 2018.
doi: 10.1007/9783319989389_23
abstract  pdf  bibtex
Abstract:
We develop and implement a translation from the process Algebra for Wireless Networks (AWN) into the milli Common Representation Language (mCRL2). As a consequence of the translation, the sophisticated toolset of mCRL2 is now available for AWNspecifications. We show that the translation respects strong bisimilarity; hence all safety properties can be automatically checked using the toolset. To show usability of our translation we report on a case study.
@InProceedings{Hoefner20183,
Author = {van Glabbeek, R.J. and H{\"o}fner, P. and van der Wal, D.},
Title = {Analysing {AWN}specifications using {mCRL2} (extended abstract)},
BookTitle = {Integrated Formal Methods (iFM 2018)},
Editor = {Furia, C.A. and Winter, K.},
Series = {Lecture Notes in Computer Science},
Volume = {11023},
Pages = {398418},
Year = {2018},
Publisher = {Springer},
Doi = {10.1007/9783319989389_23}
}

C. Bannister, P. Höfner, G. Klein:
Backwards and Forwards with Separation Logic. In J. Avigad, A. Mahboubi (eds.), Interactive Theorem Proving (ITP 2018). Lecture Notes in Computer Science 10895, pp. 6887, Springer, 2018.
doi: 10.1007/9783319948218_5
abstract  pdf  bibtex
Abstract:
The use of Hoare logic in combination with weakest preconditions and strongest postconditions is a standard tool for program verification, known as backward and forward reasoning. In this paper we extend these techniques to allow backward and forward reasoning for separation logic. While the former is derived directly from the standard operators of separation logic, the latter uses a new one. We implement our framework in the interactive proof assistant Isabelle/HOL, and enable automation with several interactive proof tactics.
@InProceedings{Hoefner20182,
Author = {Bannister, C. and H{\"o}fner, P. and Klein, G.},
Title = {Backwards and Forwards with Separation Logic},
BookTitle = {Interactive Theorem Proving (ITP 2018)},
Editor = {Avigad, J. and Mahboubi, A.},
Series = {Lecture Notes in Computer Science},
Volume = {10895},
Pages = {6887},
Year = {2018},
Publisher = {Springer},
Doi = {10.1007/9783319948218_5}
}

V. Dyseryn, R.J. van Glabbeek, P. Höfner:
Analysing Mutual Exclusion using Process Algebra with Signals. In K. Peters, T. Tini (eds.), Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS 2017). Electronic Proceedings in Theoretical Computer Science 255, pp. 1834, Open Publishing Association, 2017.
doi: 10.4204/EPTCS.255.2
abstract  pdf  bibtex
Abstract:
In contrast to common belief, the Calculus of Communicating Systems (CCS) and similar process algebras lack the expressive power to accurately capture mutual exclusion protocols without enriching the language with fairness assumptions. Adding a fairness assumption to implement a mutual exclusion protocol seems counterintuitive. We employ a signalling operator, which can be combined with CCS, or other process calculi, and show that this minimal extension is expressive enough to model mutual exclusion: we confirm the correctness of Peterson's mutual exclusion algorithm for two processes, as well as Lamport's bakery algorithm, under reasonable assumptions on the underlying memory model. The correctness of Peterson's algorithm for more than two processes requires stronger, less realistic assumptions on the underlying memory model.
@InProceedings{Hoefner20176,
Author = {Dyseryn, V. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Analysing Mutual Exclusion using Process Algebra with Signals},
BookTitle = {Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS 2017)},
Editor = {Peters, K. and Tini, T.},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {255},
Pages = {1834},
Year = {2017},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.255.2}
}

R.J. van Glabbeek, P. Höfner:
Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack. In Models for Formal Analysis of Real Systems (MARS 2017). Electronic Proceedings in Theoretical Computer Science 244, pp. 1452, Open Publishing Association, 2017.
doi: 10.4204/EPTCS.244.2
abstract  pdf  bibtex
Abstract:
We present a formal model for a fragmentation and a reassembly protocol running on top of the standardised CAN bus, which is widely used in automotive and aerospace applications. Although the CAN bus comes with an inbuilt mechanism for prioritisation, we argue that this is not sufficient and provide another protocol to overcome this shortcoming.
@InProceedings{Hoefner20173,
Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Split, Send, Reassemble: A Formal Specification of a {CAN} Bus Protocol Stack},
BookTitle = {Models for Formal Analysis of Real Systems (MARS 2017)},
Editor = {},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {244},
Pages = {1452},
Year = {2017},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.244.2}
}

E. Bres, R.J. van Glabbeek, P. Höfner:
A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract). In Programming Languages and Systems (ESOP 2016). Lecture Notes in Computer Science 9632, pp. 95122, Springer, 2016.
doi: 10.1007/9783662494981_5
abstract  pdf  bibtex
Abstract:
This paper proposes a timed process algebra for wireless networks, an extension of the Algebra for Wireless Networks. It combines treatments of local broadcast, conditional unicast and data structures, which are essential features for the modelling of network protocols. In this framework we model and analyse the Ad hoc OnDemand Distance Vector routing protocol, and show that, contrary to claims in the literature, it fails to be loop free. We also present boundary conditions for a fix ensuring that the resulting protocol is indeed loop free.
@InProceedings{Hoefner20167,
Author = {Bres, E. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract)},
BookTitle = {Programming Languages and Systems (ESOP 2016)},
Editor = {},
Series = {Lecture Notes in Computer Science},
Volume = {9632},
Pages = {95122},
Year = {2016},
Publisher = {Springer},
Doi = {10.1007/9783662494981_5}
}

P. Höfner:
Using Process Algebra to Design Better Protocol (extended abstract); invited. In Forum "MathforIndustry" 2015  The Role and Importance of Mathematics in Innovation (FMI 2015). MI Lecture Notes 65, Kyushu University, 2015.
pdf  bibtex
Abstract:
@InProceedings{Hoefner20158,
Author = {H{\"o}fner, P.},
Title = {Using Process Algebra to Design Better Protocol (extended abstract); invited},
BookTitle = {Forum "MathforIndustry" 2015  The Role and Importance of Mathematics in Innovation (FMI 2015)},
Editor = {},
Series = {MI Lecture Notes},
Volume = {65},
Pages = {},
Year = {2015},
Publisher = {Kyushu University},
Doi = {}
}

R. Berghammer, P. Höfner, I. Stucke:
ToolBased Verification of a Relational Vertex Coloring Program. In W. Kahl, J.N. Oliveira, M. Winter (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 2015). Lecture Notes in Computer Science 9348, pp. 275292, Springer, 2015.
doi: 10.1007/9783319247045_17
abstract  pdf  bibtex
Abstract:
We present different approaches of using a special purpose computer algebra system and theorem provers in software verification. To this end, we first develop a purely algebraic whileprogram for computing a vertex coloring of an undirected (loopfree) graph. For showing its correctness, we then combine the wellknown assertionbased verification method with relationalgebraic calculations. Based on this, we show how automatically to test loopinvariants by means of the RelView tool and also compare the usage of three different theorem provers in respect to the verification of the proof obligations: the automated theorem prover Prover9 and the two proof assistants Coq and Isabelle/HOL. As a result, we illustrate that algebraic abstraction yields verification tasks that can easily be verified with offtheshelf theorem provers, but also reveal some shortcomings and difficulties with theorem provers that are nowadays available.
@InProceedings{Hoefner20156,
Author = {Berghammer, R. and H{\"o}fner, P. and Stucke, I.},
Title = {ToolBased Verification of a Relational Vertex Coloring Program},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2015)},
Editor = {Kahl, W. and Oliveira, J.N. and Winter, M.},
Series = {Lecture Notes in Computer Science},
Volume = {9348},
Pages = {275292},
Year = {2015},
Publisher = {Springer},
Doi = {10.1007/9783319247045_17}
}

M. Kamali, P. Höfner, M. Kamali, L. Petre:
Formal Analysis of Proactive, Distributed Routing. In R. Calinescu, B. Rumpe (eds.), Software Engineering and Formal Methods (SEFM 2015). Lecture Notes in Computer Science 9276, pp. 175189, Springer, 2015.
doi: 10.1007/9783319229690_13
abstract  pdf  bibtex
Abstract:
As (network) software is such an omnipresent component of contemporary missioncritical systems, formal analysis is required to provide the necessary certification or at least assurance for these systems. In this paper we focus on modelling and analysing the Optimised Link State Routing (OLSR) protocol, a distributed, proactive routing protocol. It is recognised as one of the standard adhoc routing protocols for Wireless Mesh Networks (WMN). WMNs are instrumental in critical systems, such as emergency response networks and smart electrical grids. We use the model checker Uppaal for analysing safety properties of OLSR as well as to point out a case of OLSR malfunctioning.
@InProceedings{Hoefner20155,
Author = {Kamali, M. and H{\"o}fner, P. and Kamali, M. and Petre, L.},
Title = {Formal Analysis of Proactive, Distributed Routing},
BookTitle = {Software Engineering and Formal Methods (SEFM 2015)},
Editor = {Calinescu, R. and Rumpe, B.},
Series = {Lecture Notes in Computer Science},
Volume = {9276},
Pages = {175189},
Year = {2015},
Publisher = {Springer},
Doi = {10.1007/9783319229690_13}
}

T. Bourke, R.J. van Glabbeek, P. Höfner:
A Mechanized Proof of Loop Freedom of the (Untimed) {AODV} Routing Protocol. In F. Cassez, J.F. Raskin (eds.), Automated Technology for Verification and Analysis (ATVA 2014). Lecture Notes in Computer Science 8837, pp. 4763, Springer, 2014.
arXiv: CoRR abs/1505.05646  doi: 10.1007/9783319119366_5
abstract  pdf  bibtex
Abstract:
The Ad hoc Ondemand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (WMN) to know where to forward data packets. Such a protocol is `loop free' if it never leads to routing decisions that forward packets in circles. This paper describes the mechanization of an existing penandpaper proof of loop freedom of AODV in the interactive theorem prover Isabelle/HOL. The mechanization relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several improvements of AODV and show that Isabelle/HOL can reestablish most proof obligations automatically and identify exactly the steps that are no longer valid.
@InProceedings{Hoefner20145,
Author = {Bourke, T. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {A Mechanized Proof of Loop Freedom of the (Untimed) {AODV} Routing Protocol},
BookTitle = {Automated Technology for Verification and Analysis (ATVA 2014)},
Editor = {Cassez, F. and Raskin, J.F.},
Series = {Lecture Notes in Computer Science},
Volume = {8837},
Pages = {4763},
Year = {2014},
Publisher = {Springer},
Doi = {10.1007/9783319119366_5}
}

T. Bourke, R.J. van Glabbeek, P. Höfner:
Showing Invariance Compositionally for a Process Algebra of Network Protocols. In G. Klein, R. Gamboa (eds.), Interactive Theorem Proving (ITP 2014). Lecture Notes in Computer Science 8558, pp. 144159, Springer, 2014.
arXiv: CoRR abs/1407.3519  doi: 10.1007/9783319089706_10
abstract  pdf  bibtex
Abstract:
This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, for example nodes of a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). We propose a novel compositional technique for lifting properties from local states (individual nodes) to global states (networks of nodes).
@InProceedings{Hoefner20143,
Author = {Bourke, T. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Showing Invariance Compositionally for a Process Algebra of Network Protocols},
BookTitle = {Interactive Theorem Proving (ITP 2014)},
Editor = {Klein, G. and Gamboa, R.},
Series = {Lecture Notes in Computer Science},
Volume = {8558},
Pages = {144159},
Year = {2014},
Publisher = {Springer},
Doi = {10.1007/9783319089706_10}
}

R. Berghammer, P. Höfner, I. Stucke:
Automated Verification of Relational WhilePrograms. In P. Höfner, P. Jipsen, W. Kahl, M.E. Müller (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 2014). Lecture Notes in Computer Science 8428, pp. 173190, Springer, 2014.
doi: 10.1007/9783319062518_11
abstract  pdf  bibtex
Abstract:
Software verification is essential for safetycritical systems. In this paper, we illustrate that some verification tasks can be done fully automatically. We show how to automatically verify imperative programs for relationbased discrete structures by combining relation algebra and the wellknown assertionbased verification method with automated theorem proving. We present two examples in detail: a relational program for determining the reflexivetransitive closure and a topological sorting algorithm. We also treat the automatic verification of the equivalence of commonlogical and relationalgebraic specifications.
@InProceedings{Hoefner20141,
Author = {Berghammer, R. and H{\"o}fner, P. and Stucke, I.},
Title = {Automated Verification of Relational WhilePrograms},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2014)},
Editor = {H{\"o}fner, P. and Jipsen, P. and Kahl, W. and M{\"u}ller, M.E.},
Series = {Lecture Notes in Computer Science},
Volume = {8428},
Pages = {173190},
Year = {2014},
Publisher = {Springer},
Doi = {10.1007/9783319062518_11}
}

D. Batory, P. Höfner, B. Möller, A. Zelend:
Features, Modularity, and Variation Points. In Workshop on FeatureOriented Software Development (FOSD 2013). pp. 916, ACM, 2013.
doi: 10.1145/2528265.2528269
abstract  pdf  bibtex
Abstract:
A feature interaction algebra (FIA) is an abstract model of features, feature interactions, and their compositions. A structured document algebra (SDA) defines modules with variation points and how such modules compose. We present both FIA and SDA in this paper, and homomorphisms that relate FIA expressions to SDA expressions. This leads to mathematically precise formalizations of fundamental concepts used in software product lines, which can be used for improved FOSD tooling and teaching material.
@InProceedings{Hoefner20136,
Author = {Batory, D. and H{\"o}fner, P. and M{\"o}ller, B. and Zelend, A.},
Title = {Features, Modularity, and Variation Points},
BookTitle = {Workshop on FeatureOriented Software Development (FOSD 2013)},
Editor = {},
Series = {},
Volume = {0},
Pages = {916},
Year = {2013},
Publisher = {ACM},
Doi = {10.1145/2528265.2528269}
}

R.J. van Glabbeek, P. Höfner, M. Portmann, W.L. Tan:
Sequence Numbers Do Not Guarantee Loop Freedom —AODV Can Yield Routing Loops—. In Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 2013). pp. 91100, ACM, 2013.
arXiv: CoRR abs/1512.08891  doi: 10.1145/2507924.2507943
abstract  pdf  bibtex
Abstract:
In the area of mobile adhoc networks and wireless mesh networks, sequence numbers are often used in routing protocols to avoid routing loops. It is commonly stated in protocol specifications that sequence numbers are sufficient to guarantee loop freedom if they are monotonically increased over time. A classical example for the use of sequence numbers is the popular Ad hoc OnDemand Distance Vector (AODV) routing protocol. The loop freedom of AODV is not only a common belief, it has been claimed in the abstract of its RFC and at least two proofs have been proposed. AODVbased protocols such as AODVv2 (DYMO) and HWMP also claim loop freedom due to the same use of sequence numbers.
In this paper we show that AODV is not a priori loop free; by this we counter the proposed proofs in the literature. In fact, loop freedom hinges on nonevident assumptions to be made when resolving ambiguities occurring in the RFC. Thus, monotonically increasing sequence numbers, by themselves, do not guarantee loop freedom.
@InProceedings{Hoefner20135,
Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Portmann, M. and Tan, W.L.},
Title = {Sequence Numbers Do Not Guarantee Loop Freedom AODV Can Yield Routing Loops},
BookTitle = {Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 2013)},
Editor = {},
Series = {},
Volume = {0},
Pages = {91100},
Year = {2013},
Publisher = {ACM},
Doi = {10.1145/2507924.2507943}
}

A. Fehnker, P. Höfner, M. Kamali, V. Mehta:
Topologybased Mobility Models for Wireless Networks. In L. Alvisi, D. Giannakopoulou (eds.), Quantitative Evaluation of Systems (QEST 2013). Lecture Notes in Computer Science 8054, pp. 368383, Springer, 2013.
doi: 10.1007/9783642401961_32
abstract  pdf  bibtex
Abstract:
The performance and reliability of wireless network protocols heavily depend on the network and its environment. In wireless networks node mobility can affect the overall performance up to a point where, e.g. route discovery and route establishment fail. As a consequence any formal technique for performance analysis of wireless network protocols should take node mobility into account. In this paper we propose a topologybased mobility model, that abstracts from physical behaviour, and models mobility as probabilistic changes in the topology. We demonstrate how this model can be instantiated to cover the main aspects of the random walk and the random waypoint mobility model. The model is not a standalone model, but intended to be used in combination with protocol models. We illustrate this by two application examples: first we show a brief analysis of the Adhoc On demand Distance Vector (AODV) routing protocol, and second we combine the mobility model with the Lightweight Medium Access Control (LMAC).
@InProceedings{Hoefner20133,
Author = {Fehnker, A. and H{\"o}fner, P. and Kamali, M. and Mehta, V.},
Title = {Topologybased Mobility Models for Wireless Networks},
BookTitle = {Quantitative Evaluation of Systems (QEST 2013)},
Editor = {Alvisi, L. and Giannakopoulou, D.},
Series = {Lecture Notes in Computer Science},
Volume = {8054},
Pages = {368383},
Year = {2013},
Publisher = {Springer},
Doi = {10.1007/9783642401961_32}
}

P. Höfner, M. Kamali:
Quantitative Analysis of AODV and its Variants on Dynamic Topologies using Statistical Model Checking. In V. Braberman, L. Fribourg (eds.), Formal Modelling and Analysis of Timed Systems (FORMATS 2013). Lecture Notes in Computer Science 8053, pp. 121136, Springer, 2013.
doi: 10.1007/9783642402296_9
abstract  pdf  bibtex
Abstract:
Wireless Mesh Networks (WMNs) are selforganising adhoc networks that support broadband communication. Due to changes in the topology, route discovery and maintenance play a crucial role in the reliability and the performance of such networks. Formal analysis of WMNs using exhaustive model checking techniques is often not feasible: network size (up to hundreds of nodes) and topology changes yield state space explosion. Statistical Model Checking, however, can overcome this problem and allows a quantitative analysis.
In this paper we illustrate this by a careful analysis of the Ad hoc On demand Distance Vector (AODV) protocol. We show that some optional features of AODV are not useful, and that AODV shows unexpected behaviour, yielding a high probability of route discovery failure.
@InProceedings{Hoefner20134,
Author = {H{\"o}fner, P. and Kamali, M.},
Title = {Quantitative Analysis of {AODV} and its Variants on Dynamic Topologies using Statistical Model Checking},
BookTitle = {Formal Modelling and Analysis of Timed Systems (FORMATS 2013)},
Editor = {Braberman, V. and Fribourg, L.},
Series = {Lecture Notes in Computer Science},
Volume = {8053},
Pages = {121136},
Year = {2013},
Publisher = {Springer},
Doi = {10.1007/9783642402296_9}
}

P. Höfner, A. McIver:
Statistical Model Checking of Wireless Mesh Routing Protocols. In G. Brat, N. Rungta, A. Venet (eds.), NASA Formal Methods Symposium (NFM 2013). Lecture Notes in Computer Science 7871, pp. 322336, Springer, 2013.
doi: 10.1007/9783642380884_22
abstract  pdf  bibtex
Abstract:
Several case studies indicate that model checking is limited in the analysis of mesh networks: state space explosion restricts applicability to at most 10 node networks, and quantitative reasoning, often sufficient for network evaluation, is not possible. Both deficiencies can be overcome to some extent by the use of statistical model checkers, such as SMCUppaal. In this paper we illustrate this by a quantitative analysis of two wellknown routing protocols for wireless mesh networks, namely AODV and DYMO. Moreover, we push the limits and show that this technology is capable of analysing networks of up to 100 nodes.
@InProceedings{Hoefner20132,
Author = {H{\"o}fner, P. and McIver, A.},
Title = {Statistical Model Checking of Wireless Mesh Routing Protocols},
BookTitle = {NASA Formal Methods Symposium (NFM 2013)},
Editor = {Brat, G. and Rungta, N. and Venet, A.},
Series = {Lecture Notes in Computer Science},
Volume = {7871},
Pages = {322336},
Year = {2013},
Publisher = {Springer},
Doi = {10.1007/9783642380884_22}
}

S. Edenhofer, P. Höfner:
Towards a Rigorous Analysis of AODVv2 (DYMO). In N. Foster, A. Gurney (eds.), Rigorous Protocol Engineering (WRiPE 2012). IEEE, 2012.
doi: 10.1109/ICNP.2012.6459942
abstract  pdf  bibtex
Abstract:
Dynamic MANET Ondemand (AODVv2) routing, formerly known as DYMO, is a routing protocol especially designed for wireless, multi hop networks. AODVv2 determines routes in a network in an ondemand fashion.
In this paper we present a formal model of AODVv2, using the process algebra AWN. The benefit of this is twofold: (a) the given specification is definitely free of ambiguities; (b) a formal and rigorous analysis of the routing protocol is now feasible. To underpin the latter point we also present a first analysis of the AODVv2 routing protocol. On the one hand we show that some of the problems discovered in the AODV routing protocol, the predecessor of AODVv2, have been addressed and solved. On the other hand we show that other limitations still exist; an example is the establishment of nonoptimal routes. Even worse, we locate shortcomings in the AODVv2 routing protocol that do not occur in AODV. This yields the conclusion that AODVv2 is not necessarily better than AODV.
@InProceedings{Hoefner20125,
Author = {Edenhofer, S. and H{\"o}fner, P.},
Title = {Towards a Rigorous Analysis of {AODVv2} ({DYMO})},
BookTitle = {Rigorous Protocol Engineering (WRiPE 2012)},
Editor = {Foster, N. and Gurney, A.},
Series = {},
Volume = {0},
Pages = {},
Year = {2012},
Publisher = {IEEE},
Doi = {10.1109/ICNP.2012.6459942}
}

P. Höfner, R.J. van Glabbeek, W.L. Tan, M. Portmann, A. McIver, A. Fehnker:
A Rigorous Analysis of AODV and its Variants. In Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 2012). pp. 203212, ACM, 2012. (nominated for best paper award)
arXiv: CoRR abs/1512.08873  doi: 10.1145/2387238.2387274
abstract  pdf  bibtex
Abstract:
In this paper we present a rigorous analysis of the Ad hoc OnDemand Distance Vector (AODV) routing protocol using a formal specification in AWN (Algebra for Wireless Net works), a process algebra which has been specifically tailored for the modelling of Mobile Ad Hoc Networks and Wireless Mesh Network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol correctness properties by providing a detailed proof of loop freedom. In contrast to evaluations using simulation or other formal methods such as model checking, our proof is generic and holds for any possible network scenario in terms of network topology, node mobility, traffic pattern, etc. A key contribution of this paper is the demonstration of how the reasoning and proofs can relatively easily be adapted to protocol variants.
@InProceedings{Hoefner20127,
Author = {H{\"o}fner, P. and van Glabbeek, R.J. and Tan, W.L. and Portmann, M. and McIver, A. and Fehnker, A.},
Title = {A Rigorous Analysis of {AODV} and its Variants},
BookTitle = {Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 2012)},
Editor = {},
Series = {},
Volume = {0},
Pages = {203212},
Year = {2012},
Publisher = {ACM},
Doi = {10.1145/2387238.2387274}
}

P. Höfner, B. Möller, A. Zelend:
Foundations of Coloring Algebra with Consequences for Featureoriented Programming. In W. Kahl, T. Griffin (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 2012). Lecture Notes in Computer Science 7560, pp. 3349, Springer, 2012.
doi: 10.1007/9783642333149_3
abstract  pdf  bibtex
Abstract:
In 2011, simple and concise axioms for feature compositions, interactions and products have been proposed by Batory et al. They were mainly inspired by Kästner's Colored IDE (CIDE) as well as by experience in feature oriented programming over the last decades. However, so far only axioms were proposed; consequences of these axioms such as variability in models have not been studied. In this paper we discuss the proposed axioms from a theoretical point of view, which yields a much better understanding of the proposed algebra and therefore of feature oriented programming. For example, we show that the axioms characterising feature composition are isomorphic to settheoretic models.
@InProceedings{Hoefner20126,
Author = {H{\"o}fner, P. and M{\"o}ller, B. and Zelend, A.},
Title = {Foundations of Coloring Algebra with Consequences for Featureoriented Programming},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2012)},
Editor = {Kahl, W. and Griffin, T.},
Series = {Lecture Notes in Computer Science},
Volume = {7560},
Pages = {3349},
Year = {2012},
Publisher = {Springer},
Doi = {10.1007/9783642333149_3}
}

A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, W.L. Tan:
A Process Algebra for Wireless Mesh Networks. In H. Seidl (ed.), Programming Languages and Systems (ESOP'12) (ESOP 2012). Lecture Notes in Computer Science 7211, pp. 295315, Springer, 2012.
doi: 10.1007/9783642288692_15
abstract  pdf  bibtex
Abstract:
We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Adhoc OnDemand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.
@InProceedings{Hoefner20122,
Author = {Fehnker, A. and van Glabbeek, R.J. and H{\"o}fner, P. and McIver, A. and Portmann, M. and Tan, W.L.},
Title = {A Process Algebra for Wireless Mesh Networks},
BookTitle = {Programming Languages and Systems (ESOP'12) (ESOP 2012)},
Editor = {Seidl, H.},
Series = {Lecture Notes in Computer Science},
Volume = {7211},
Pages = {295315},
Year = {2012},
Publisher = {Springer},
Doi = {10.1007/9783642288692_15}
}

A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, W.L. Tan:
Automated Analysis of AODV using UPPAAL. In C. Flanagan, B. König (eds.), Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012). Lecture Notes in Computer Science 7214, pp. 173187, Springer, 2012.
arXiv: CoRR abs/1512.07352  doi: 10.1007/9783642287565_13
abstract  pdf  bibtex
Abstract:
This paper describes an automated, formal and rigorous analysis of the Ad hoc OnDemand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks.
We give a brief overview of a model of AODV implemented in the UPPAAL model checker. It is derived from a processalgebraic model which reflects precisely the intention of AODV and accurately captures the protocol specification. Furthermore, we describe experiments carried out to explore AODV's behaviour in all network topologies up to 5 nodes. We were able to automatically locate problematic and undesirable behaviours. This is in particular useful to discover protocol limitations and to develop improved variants. This use of model checking as a diagnostic tool complements other formalmethodsbased protocol modelling and verification techniques, such as process algebra.
@InProceedings{Hoefner20121,
Author = {Fehnker, A. and van Glabbeek, R.J. and H{\"o}fner, P. and McIver, A. and Portmann, M. and Tan, W.L.},
Title = {Automated Analysis of AODV using UPPAAL},
BookTitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)},
Editor = {Flanagan, C. and K{\"o}nig, B.},
Series = {Lecture Notes in Computer Science},
Volume = {7214},
Pages = {173187},
Year = {2012},
Publisher = {Springer},
Doi = {10.1007/9783642287565_13}
}

D. Batory, P. Höfner, J. Kim:
Feature Interactions, Products, and Composition. In Generative Programming and Component Engineering (GPCE 2011). pp. 1322, ACM, 2011.
doi: 10.1145/2047862.2047867
abstract  pdf  bibtex
Abstract:
The relationship between feature modules and feature interactions is not wellunderstood. To explain classic examples of feature interaction, we show that features are not only composed sequentially, but also by crossproduct and interaction operations that heretofore were implicit in the literature. Using the Colored IDE (CIDE) tool as our starting point, we (a) present a formal model of these operations, (b) show how it connects and explains previously unrelated results in Feature Oriented Software Development (FOSD), and (c) describe a tool, based on our formalism, that demonstrates how changes in composed documents can be backpropagated to their original feature module definitions, thereby improving FOSD tooling.
@InProceedings{Hoefner20118,
Author = {Batory, D. and H{\"o}fner, P. and Kim, J.},
Title = {Feature Interactions, Products, and Composition},
BookTitle = {Generative Programming and Component Engineering (GPCE 2011)},
Editor = {},
Series = {},
Volume = {0},
Pages = {1322},
Year = {2011},
Publisher = {ACM},
Doi = {10.1145/2047862.2047867}
}

A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, W.L. Tan:
Modelling and Analysis of AODV in UPPAAL. In Rigorous Protocol Engineering (WRiPE'11) (WRiPE 2011). 2011.
abstract  pdf  bibtex
Abstract:
This paper describes work in progress towards an automated formal and rigorous analysis of the Ad hoc OnDemand Distance Vector (AODV) routing protocol, a popular protocol used in ad hoc wireless networks.
We give a brief overview of a model of AODV implemented in the UPPAAL model checker, and describe experiments carried out to explore AODV's behaviour in two network topologies. We were able to locate automatically and confirm some known problematic and undesirable behaviours. We believe this use of model checking as a diagnostic tool complements other formal methods based protocol modelling and verification techniques, such as process algebras. Model checking is in particular useful for the discovery of protocol limitations and in the development of improved variations.
@InProceedings{Hoefner20117,
Author = {Fehnker, A. and van Glabbeek, R.J. and H{\"o}fner, P. and McIver, A. and Portmann, M. and Tan, W.L.},
Title = {Modelling and Analysis of {AODV} in {UPPAAL}},
BookTitle = {Rigorous Protocol Engineering (WRiPE'11) (WRiPE 2011)},
Editor = {},
Series = {},
Volume = {0},
Pages = {},
Year = {2011},
Publisher = {},
Doi = {}
}

P. Höfner, A. McIver:
Towards an Algebra of Routing Tables. In H. de Swart (ed.), Relational and Algebraic Methods in Computer Science (RAMiCS 2011). Lecture Notes in Computer Science 6663, pp. 212229, Springer, 2011.
doi: 10.1007/9783642210709_17
abstract  pdf  bibtex
Abstract:
We use wellknown algebraic concepts like semirings and matrices to model and argue about Wireless Mesh Networks. These networks are used in a wide range of application areas, including public safety and transportation. Formal reasoning therefore seems to be necessary to guarantee safety and security. In this paper, we model a simplified algebraic version of the AODV protocol and provide some basic properties. For example we show that each node knows a route to the originator of a message (if there is one).
@InProceedings{Hoefner20115,
Author = {H{\"o}fner, P. and McIver, A.},
Title = {Towards an Algebra of Routing Tables},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2011)},
Editor = {de Swart, H.},
Series = {Lecture Notes in Computer Science},
Volume = {6663},
Pages = {212229},
Year = {2011},
Publisher = {Springer},
Doi = {10.1007/9783642210709_17}
}

H.H. Dang, P. Höfner:
Variable Side Conditions and Greatest Relations in Algebraic Separation Logic. In H. de Swart (ed.), Relational and Algebraic Methods in Computer Science (RAMiCS 2011). Lecture Notes in Computer Science 6663, pp. 125140, Springer, 2011.
doi: 10.1007/9783642210709_11
abstract  pdf  bibtex
Abstract:
When reasoning within separation logic, it is often necessary to provide side conditions for inference rules. These side conditions usually contain information about variables and their use, and are given within a metalanguage, i.e., the side conditions cannot be encoded in separation logic itself. In this paper we discuss different possibilities how side conditions of variables—occurring e.g. in the ordinary or the hypothetical frame rule—can be characterised using algebraic separation logic. We also study greatest relations; a concept used in the soundness proof of the hypothetical frame rule. We provide one and only one level of abstraction for the logic, the side conditions and the greatest relations.
@InProceedings{Hoefner20114,
Author = {Dang, H.H. and H{\"o}fner, P.},
Title = {Variable Side Conditions and Greatest Relations in Algebraic Separation Logic},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2011)},
Editor = {de Swart, H.},
Series = {Lecture Notes in Computer Science},
Volume = {6663},
Pages = {125140},
Year = {2011},
Publisher = {Springer},
Doi = {10.1007/9783642210709_11}
}

H.H. Dang, P. Höfner:
Automated Higherorder Reasoning about Quantales. In B. Konev, R.A. Schmidt, S. Schulz (eds.), Workshop on Practical Aspects of Automated Reasoning (PAAR'10) (PAAR 2010"pages: "4051). EasyChair Proceedings in Computing 9, EasyChair, 2010.
abstract  pdf  bibtex
Abstract:
Originally developed as an algebraic characterisation for quantum mechanics, the al gebraic structure of quantales nowadays finds widespread applications ranging from (non commutative) logics to hybrid systems. We present an approach to bring reasoning about quantales into the realm of (fully) automated theorem proving. This will yield automation in various (new) fields of applications in the future. To achieve this goal and to receive a general approach (independent of any particular theorem prover), we use the TPTP Prob lem Library for higherorder logic. In particular, we give an encoding of quantales in the typed higherorder form (THF) and present some theorems about quantales which can be proved fully automatically. We further present prospective applications for our approach and discuss practical experiences using THF.
@InProceedings{Hoefner20102,
Author = {Dang, H.H. and H{\"o}fner, P.},
Title = {Automated Higherorder Reasoning about Quantales},
BookTitle = {Workshop on Practical Aspects of Automated Reasoning (PAAR'10) (PAAR 2010"pages: "4051)},
Editor = {Konev, B. and Schmidt, R.A. and Schulz, S.},
Series = {EasyChair Proceedings in Computing},
Volume = {9},
Pages = {},
Year = {2010},
Publisher = {EasyChair},
Doi = {}
}

P. Höfner, B. Möller:
An Extension of Feature Algebra [Extended Abstract]. In S. Apel, W.R. Cook, K. Czarnecki, C. Kästner, N. Loughran, O. Nierstrasz (eds.), Workshop on FeatureOriented Software Development (FOSD'09). pp. 7580, ACM, 2009.
doi: 10.1145/1629716.1629731
abstract  pdf  bibtex
Abstract:
Feature algebra was introduced as an abstract framework for feature oriented software development. One goal is to pro vide a common, clearly defined basis for the key ideas of feature orientation. We first present concrete models for the original axioms of feature algebra which represent the main features of feature oriented programs. However, these mod els show that the axioms of the feature algebra do not reflect some aspects of feature orientation properly. Hence we modify the axioms and introduce the concept of an extended feature algebra. Since the extension is also a generalisation, the original algebra can be retrieved by a single additional axiom. Last but not least we introduce more operators to cover concepts like overriding in the abstract setting.
@InProceedings{Hoefner20094,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {An Extension of Feature Algebra [Extended Abstract]},
BookTitle = {Workshop on FeatureOriented Software Development (FOSD'09)},
Editor = {Apel, S. and Cook, W.R. and Czarnecki, K. and K{\"a}stner, C. and Loughran, N. and Nierstrasz, O.},
Series = {},
Volume = {0},
Pages = {7580},
Year = {2009},
Publisher = {ACM},
Doi = {10.1145/1629716.1629731}
}

H.H. Dang, P. Höfner, B. Möller:
Towards Algebraic Separation Logic. In R. Berghammer, A.M Jaoua, B. Möller (eds.), Relations and Kleene Algebra in Computer Science (RelmiCS/AKA'09). Lecture Notes in Computer Science 5827, pp. 5972, Springer, 2009.
doi: 10.1007/9783642046391_5
abstract  pdf  bibtex
Abstract:
We present an algebraic approach to separation logic. In particular, we give algebraic characterisations for all constructs of separation logic. The algebraic view does not only yield new insights on separation logic but also shortens proofs and enables the use of automated theorem provers for verifying properties at a more abstract level.
@InProceedings{Hoefner20093,
Author = {Dang, H.H. and H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Towards Algebraic Separation Logic},
BookTitle = {Relations and Kleene Algebra in Computer Science (RelmiCS/AKA'09)},
Editor = {Berghammer, R. and Jaoua, A.M and M{\"o}ller, B.},
Series = {Lecture Notes in Computer Science},
Volume = {5827},
Pages = {5972},
Year = {2009},
Publisher = {Springer},
Doi = {10.1007/9783642046391_5}
}

P. Höfner, R. Khedri, B. Möller:
Algebraic View Reconciliation. In A. Cerone, S. Gruner (eds.), Software Engineering and Formal Methods (SEFM'08). pp. 8594, IEEE, 2008.
doi: 10.1109/SEFM.2008.36
abstract  pdf  bibtex
Abstract:
Embedded systems such as automotive systems are very complex to specify. Since it is difficult to capture all their requirements or their design in one single model, approaches working with several system views are adopted. The main problem there is to keep these views coherent; the issue is known as view reconciliation. This paper proposes an algebraic solution. It uses sets of integration constraints that link (families of) system features in one view to other (families of) features in the same or a different view. Both, families and constraints, are formalised using a feature algebra. Besides presenting a constraint relation and its mathematical properties, the paper shows in several examples the suitability of this approach for a wide class of integration constraint formulations.
@InProceedings{Hoefner20087,
Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
Title = {Algebraic View Reconciliation},
BookTitle = {Software Engineering and Formal Methods (SEFM'08)},
Editor = {Cerone, A. and Gruner, S.},
Series = {},
Volume = {0},
Pages = {8594},
Year = {2008},
Publisher = {IEEE},
Doi = {10.1109/SEFM.2008.36}
}

P. Höfner, G. Struth:
On Automating the Calculus of Relations. In A. Armando, P. Baumgartner, G. Dowek (eds.), Automated Reasoning. Lecture Notes in Artificial Intelligence 5195, pp. 5066, Springer, 2008.
doi: 10.1007/9783540710707_5
abstract  pdf  bibtex
Abstract:
Relation algebras provide abstract equational axioms for the calculus of binary relations. They name an established area of mathematics and have found numerous applications in computing. We prove more than hundred theorems of relation algebras with offtheshelf automated theorem provers. They form a basic calculus from which more advanced applications can be explored. We also present two automation experiments from the formal methods literature. Our results further demonstrate the feasibility of automated deduction with complex algebraic structures. They also open a new perspective for automated deduction in relational formal methods.
@InProceedings{Hoefner20086,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {On Automating the Calculus of Relations},
BookTitle = {Automated Reasoning},
Editor = {Armando, A. and Baumgartner, P. and Dowek, G.},
Series = {Lecture Notes in Artificial Intelligence},
Volume = {5195},
Pages = {5066},
Year = {2008},
Publisher = {Springer},
Doi = {10.1007/9783540710707_5}
}

P. Höfner:
Automated Reasoning for Hybrid Systems — Two Case Studies —. In R. Berghammer, B. Möller, G. Struth (eds.), Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08). Lecture Notes in Computer Science 4988, pp. 191205, Springer, 2008.
doi: 10.1007/9783540789130_15
abstract  pdf  bibtex
Abstract:
At an abstract level hybrid systems are related to variants of Kleene algebra. Since it has recently been shown that Kleene algebras and their variants, like omega algebras, provide a reasonable base for automated reasoning, the aim of the present paper is to show that automated algebraic reasoning for hybrid system is feasible. We mainly focus on applications. In particular, we present case studies and proof experiments to show how concrete properties of hybrid systems, like safety and liveness, can be algebraically characterised and how offtheshelf automated theorem provers can be used to verify them.
@InProceedings{Hoefner20085,
Author = {H{\"o}fner, P.},
Title = {Automated Reasoning for Hybrid Systems  Two Case Studies },
BookTitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08)},
Editor = {Berghammer, R. and M{\"o}ller, B. and Struth, G.},
Series = {Lecture Notes in Computer Science},
Volume = {4988},
Pages = {191205},
Year = {2008},
Publisher = {Springer},
Doi = {10.1007/9783540789130_15}
}

P. Höfner, G. Struth:
Nontermination in Idempotent Semirings. In R. Berghammer, B. Möller, G. Struth (eds.), Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08). Lecture Notes in Computer Science 4988, pp. 206220, Springer, 2008.
doi: 10.1007/9783540789130_16
abstract  pdf  bibtex
Abstract:
We study and compare two notions of nontermination on idempotent semirings: infinite iteration and divergence. We determine them in various models and develop conditions for their coincidence. It turns out that divergence yields a simple and natural way of modelling infinite behaviour, whereas infinite iteration shows some anomalies.
@InProceedings{Hoefner20084,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Nontermination in Idempotent Semirings},
BookTitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08)},
Editor = {Berghammer, R. and M{\"o}ller, B. and Struth, G.},
Series = {Lecture Notes in Computer Science},
Volume = {4988},
Pages = {206220},
Year = {2008},
Publisher = {Springer},
Doi = {10.1007/9783540789130_16}
}

P. Höfner, G. Struth:
Automated Reasoning in Kleene Algebra. In F. Pfenning (ed.), Automated Deduction (CADE21). Lecture Notes in Artificial Intelligence 4603, pp. 279294, Springer, 2007.
doi: 10.1007/9783540735953_19
abstract  pdf  bibtex
Abstract:
It has often been claimed that model checking, special purpose automated deduction or interactive theorem proving are needed for formal program development. We demonstrate that offtheshelf automated proof and counterexample search is an interesting alternative if combined with the right domain model. We implement variants of Kleene algebras axiomatically in Prover9/Mace4 and perform proof experiments about Hoare, dynamic, temporal logics, concurrency control and termination analysis. They confirm that a simple automated analysis of some important program properties is possible. Particular benefits of this approach include \"soft\" model checking in a firstorder setting, crosstheory reasoning between standard formalisms and full automation of some (co)inductive arguments. Kleene algebras might therefore provide lightweight formal methods with heavyweight automation.
@InProceedings{Hoefner20072,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Automated Reasoning in Kleene Algebra},
BookTitle = {Automated Deduction (CADE21)},
Editor = {Pfenning, F.},
Series = {Lecture Notes in Artificial Intelligence},
Volume = {4603},
Pages = {279294},
Year = {2007},
Publisher = {Springer},
Doi = {10.1007/9783540735953_19}
}

P. Höfner, B. Möller:
Lazy Semiring Neighbours and Some Applications. In R.A. Schmidt (ed.), Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06). Lecture Notes in Computer Science 4136, pp. 207221, Springer, 2006.
doi: 10.1007/11828563_14
abstract  pdf  bibtex
Abstract:
We extend an earlier algebraic approach to Neighbourhood Logic (NL) from domain semirings to lazy semirings yielding lazy semiring neighbours. Furthermore we show three important applications for these. The first one extends NL to intervals with infinite length. The second one applies lazy semiring neighbours in an algebraic semantics of the branching time temporal logic CTL*. The third one sets up a connection between hybrid systems and lazy semiring neighbours.
@InProceedings{Hoefner20069,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Lazy Semiring Neighbours and Some Applications},
BookTitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06)},
Editor = {Schmidt, R.A.},
Series = {Lecture Notes in Computer Science},
Volume = {4136},
Pages = {207221},
Year = {2006},
Publisher = {Springer},
Doi = {10.1007/11828563_14}
}

P. Höfner, B. Möller, K. Solin:
Omega Algebra, Demonic Refinement Algebra and Commands. In R.A. Schmidt (ed.), Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06). Lecture Notes in Computer Science 4136, pp. 222234, Springer, 2006.
doi: 10.1007/11828563_15
abstract  pdf  bibtex
Abstract:
Weak omega algebra and demonic refinement algebra are two ways of describing systems with finite and infinite iteration. We show that these independently introduced kinds of algebras can actually be defined in terms of each other. By defining modal operators on the underlying weak semiring, that result directly gives a demonic refinement algebra of commands. This yields models in which extensionality does not hold. Since in predicatetransformer models extensionality always holds, this means that the axioms of demonic refinement algebra do not characterise predicatetransformer models uniquely. The omega and the demonic refinement algebra of commands both utilise the convergence operator that is analogous to the halting predicate of modal μcalculus. We show that the convergence operator can be defined explicitly in terms of infinite iteration and domain if and only if domain coinduction for infinite iteration holds.
@InProceedings{Hoefner20068,
Author = {H{\"o}fner, P. and M{\"o}ller, B. and Solin, K.},
Title = {Omega Algebra, Demonic Refinement Algebra and Commands},
BookTitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06)},
Editor = {Schmidt, R.A.},
Series = {Lecture Notes in Computer Science},
Volume = {4136},
Pages = {222234},
Year = {2006},
Publisher = {Springer},
Doi = {10.1007/11828563_15}
}

P. Höfner, R. Khedri, B. Möller:
Feature Algebra. In J. Misra, T. Nipkow, E. Sekerinski (eds.), Formal Methods (FM'06). Lecture Notes in Computer Science 4085, pp. 300315, Springer, 2006.
doi: 10.1007/11813040_21
abstract  pdf  bibtex
Abstract:
Based on experience from the hardware industry, product families have entered the software development process as well, since software developers often prefer not to build a single product but rather a family of similar products that share at least one common functionality while having wellidentified variabilities. Such shared commonalities, also called features, reach from common hardware parts to software artefacts such as requirements, architectural properties, components, middleware, or code. We use idempotent semirings as the basis for a feature algebra that allows a formal treatment of the above notions as well as calculations with them. In particular models of feature algebra the elements are sets of products, i.e. product families. We extend the algebra to cover product lines, refinement, product development and product classification. Finally we briefly describe a prototype implementation of one particular model.
@InProceedings{Hoefner20065,
Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
Title = {Feature Algebra},
BookTitle = {Formal Methods (FM'06)},
Editor = {Misra, J. and Nipkow, T. and Sekerinski, E.},
Series = {Lecture Notes in Computer Science},
Volume = {4085},
Pages = {300315},
Year = {2006},
Publisher = {Springer},
Doi = {10.1007/11813040_21}
}

B. Möller, P. Höfner, G. Struth:
Quantales and Temporal Logics. In M. Johnson, V. Vene (eds.), Algebraic Methodology and Software Technology (AMAST'06). Lecture Notes in Computer Science 4019, pp. 263277, Springer, 2006.
doi: 10.1007/11784180_21
abstract  pdf  bibtex
Abstract:
We propose an algebraic semantics for the temporal logic CTL* and simplify it for its sublogics CTL and LTL. We abstractly represent state and path formulas over transition systems in Boolean left quantales. These are complete lattices with a multiplication that preserves arbitrary joins in its left argument and is isotone in its right argument. Over these quantales, the semantics of CTL* formulas can be encoded via finite and infinite iteration operators; the CTL and LTL operators can be related to domain operators. This yields interesting new connections between representations as known from the modal μcalculus and Kleene/ωalgebra.
@InProceedings{Hoefner20064,
Author = {M{\"o}ller, B. and H{\"o}fner, P. and Struth, G.},
Title = {Quantales and Temporal Logics},
BookTitle = {Algebraic Methodology and Software Technology (AMAST'06)},
Editor = {Johnson, M. and Vene, V.},
Series = {Lecture Notes in Computer Science},
Volume = {4019},
Pages = {263277},
Year = {2006},
Publisher = {Springer},
Doi = {10.1007/11784180_21}
}

P. Höfner, B. Möller:
Towards an Algebra of Hybrid Systems. In W. MacCaull, M. Winter, I. Düntsch (eds.), Relational Methods in Computer Science (RelMiCS8/AKA3). Lecture Notes in Computer Science 3929, pp. 121133, Springer, 2006.
doi: 10.1007/11734673_10
abstract  pdf  bibtex
Abstract:
We present a trajectorybased model for describing hybrid systems. For this we use left quantales and left semirings, thus providing a new application for these algebraic structures. Furthermore, we sketch a connection between game theory and hybrid systems.
@InProceedings{Hoefner20062,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Towards an Algebra of Hybrid Systems},
BookTitle = {Relational Methods in Computer Science (RelMiCS8/AKA3)},
Editor = {MacCaull, W. and Winter, M. and D{\"u}ntsch, I.},
Series = {Lecture Notes in Computer Science},
Volume = {3929},
Pages = {121133},
Year = {2006},
Publisher = {Springer},
Doi = {10.1007/11734673_10}
}

A. Huhn, P. Höfner, W. Kießling:
Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System. In M. Winter, A. Rauber, S. Christodoulakis, A Min Tjoa (eds.), Research and Advanced Technology for Digital Libraries (ECDL'05). Lecture Notes in Computer Science 3652, pp. 498499, Springer, 2005.
doi: 10.1007/11551362_53
abstract  pdf  bibtex
Abstract:
Advanced personalization techniques are required to cope with novel challenges posed by attributerich digital libraries. At the heart of our deeply personalized alerting system is one extensible preference model that serves all purposes in conjunction with our search technology Preference XPath and XMLbased semantic annotations of digital library objects. In this paper we focus on the impact of automatic query expansion by ontologies. First results indicate that use of ontologies improves the quality of the result set and generates further results of higher quality.
@InProceedings{Hoefner20053,
Author = {Huhn, A. and H{\"o}fner, P. and Kie{\ss}ling, W.},
Title = {Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System},
BookTitle = {Research and Advanced Technology for Digital Libraries (ECDL'05)},
Editor = {Winter, M. and Rauber, A. and Christodoulakis, S. and Tjoa, A Min},
Series = {Lecture Notes in Computer Science},
Volume = {3652},
Pages = {498499},
Year = {2005},
Publisher = {Springer},
Doi = {10.1007/11551362_53}
}

P. Höfner, B. Möller:
A New Correctness Proof for Prim's Algorithm. Technical Report 201902, Institute of Computer Science, University of Augsburg. 2019. direct link.
abstract  pdf  bibtex
Abstract:
We present a new correctness proof for Prim's algorithm. The standard proof establishes the invariant that each iteration constructs a subtree of some minimal spanning tree, and heavily relies on the existence of a spanning tree of the overall graph, as well as an `edge exchange' property, which includes reasoning about graph cycles. We establish a stronger property showing that the algorithm builds a minimal spanning tree in each step, w.r.t. the vertices already covered. As a consequence, the proof neither uses the existence of a minimal spanning tree of the entire graph, nor the classical exchange property.
@Techreport{Hoefner20195,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {A New Correctness Proof for Prim's Algorithm},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201902},
Year = {2019},
Url = {opus.bibliothek.uniaugsburg.de/opus4/57262}
}

E. Bres, R.J. van Glabbeek, P. Höfner:
A Timed Process Algebra for Wireless Networks with an Application in Routing. Technical Report 9145, NICTA. 2016. url: www.nicta.com.au/pub?doc=9145.
arXiv: CoRR abs/1606.03663
abstract  pdf  bibtex
Abstract:
This paper proposes a timed process algebra for wireless networks, an extension of the Algebra for Wireless Networks. It combines treatments of local broadcast, conditional unicast and data structures, which are essential features for the modelling of network protocols. In this framework we model and analyse the Ad hoc OnDemand Distance Vector routing protocol, and show that, contrary to claims in the literature, it fails to be loop free. We also present boundary conditions for a fix ensuring that the resulting protocol is indeed loop free.
@Techreport{Hoefner20168,
Author = {Bres, E. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {A Timed Process Algebra for Wireless Networks with an Application in Routing},
Institution = {NICTA},
Number = {9145},
Year = {2016},
Url = {www.nicta.com.au/pub?doc=9145}
}

R.J. van Glabbeek, P. Höfner:
Progress, Fairness and Justness in Process Algebra. Technical Report 8501, NICTA. 2015. url: www.nicta.com.au/pub?doc=8501.
arXiv: CoRR abs/1501.03268
abstract  pdf  bibtex
Abstract:
To prove liveness properties of concurrent systems, it is often necessary to postulate progress, fairness and justness properties. This paper investigates how the necessary progress, fairness and justness assumptions can be added to or incorporated in a standard processalgebraic specification formalism. We propose a formalisation that can be applied to a wide range of process algebras. The presented formalism is used to reason about route discovery and packet delivery in the setting of wireless networks.
@Techreport{Hoefner20153,
Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Progress, Fairness and Justness in Process Algebra},
Institution = {NICTA},
Number = {8501},
Year = {2015},
Url = {www.nicta.com.au/pub?doc=8501}
}

D. Batory, P. Höfner, B. Möller, A. Zelend:
Features, Modularity, and Variation Points. Technical Report TR2147, University of Texas at Austin. 2013. direct link.
abstract  pdf  bibtex
Abstract:
A feature interaction algebra (FIA) is an abstract model of features, feature interactions, and their compositions. A structured document algebra (SDA) defines modules with variation points and how such modules compose. We present both FIA and SDA in this paper, and homomorphisms that relate FIA expressions to SDA expressions. Doing so separates fundamental concepts of Software Product Lines (SPLs) that have previously been conflated and misunderstood. Our work also justifies observations and relationships that have been used in prior work on featurebased SPLs.
@Techreport{Hoefner20137,
Author = {Batory, D. and H{\"o}fner, P. and M{\"o}ller, B. and Zelend, A.},
Title = {Features, Modularity, and Variation Points},
Institution = {University of Texas at Austin},
Number = {TR2147},
Year = {2013},
Url = {apps.cs.utexas.edu/tech_reports/reports/tr/TR2147.pdf}
}

A. Fehnker, R.J. van Glabbeek, P. Höfner, M. Portmann, A. McIver, W.L. Tan:
A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV. Technical Report 5513, NICTA. 2013. url: www.nicta.com.au/pub?doc=5513.
arXiv: CoRR abs/1312.7645
abstract  pdf  bibtex
Abstract:
We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Adhoc OnDemand Distance Vector (AODV) routing protocol. We give a complete specification of this widelyused protocol, where only timing aspects are omitted. The process algebra allows us to state and (dis)prove crucial properties of mesh network routing protocols such as loop freedom and packet delivery.
Based on the unambiguous specification, we locate some problems and limitations of AODV that could easily yield performance problems. Two examples are the nonoptimal routes established by AODV and the fact that some routes are not found at all. These problems are then analysed and improvements are suggested. Since the improvements are formalised in the same process algebra, proofs of loop freedom etc. become simple.
@Techreport{Hoefner20131,
Author = {Fehnker, A. and van Glabbeek, R.J. and H{\"o}fner, P. and Portmann, M. and McIver, A. and Tan, W.L.},
Title = {A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing {AODV}},
Institution = {NICTA},
Number = {5513},
Year = {2013},
Url = {www.nicta.com.au/pub?doc=5513}
}

P. Höfner, B. Möller, A. Zelend:
Foundations of Coloring Algebra with Consequences for FeatureOriented Programming. Technical Report 201206, Institute of Computer Science, University of Augsburg. 2012. direct link.
abstract  pdf  bibtex
Abstract:
In 2011, simple and concise axioms for feature compositions, interactions and products have been proposed by Batory et al. They were mainly inspired by Kästner's Colored IDE (CIDE) as well as by experience in feature oriented programming over the last decades. However, so far only axioms were proposed; consequences of these axioms such as variability in models have not been studied. In this paper we discuss the proposed axioms from a theoretical point of view, which yields a much better understanding of the proposed algebra and therefore of feature oriented programming. For example, we show that the axioms characterising feature composition are isomorphic to settheoretic models.
@Techreport{Hoefner201212,
Author = {H{\"o}fner, P. and M{\"o}ller, B. and Zelend, A.},
Title = {Foundations of Coloring Algebra with Consequences for FeatureOriented Programming},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201206},
Year = {2012},
Url = {www.informatik.uniaugsburg.de/en/chairs/dbis/pmi/publications/all_pmi_techreports/tr201206_hoe_moe_zel.html}
}

P. Höfner, S. Mentl, B. Möller, W. Scholz:
Requirements in Feature Algebra. Technical Report 201012, Institute of Computer Science, University of Augsburg. 2010. direct link.
abstract  bibtex
Abstract:
Feature Algebra is intended to capture the commonalities of feature oriented software development (FOSD) such as introductions, refinements and quantification. It abstracts from differences of minor importance and focusses on most of the main aspects of FOSD. However, so far requirements have not been integrated into Feature Algebra. They arise within different aspects of feature orientation, like feature interaction, feature dependence, mutual exclusion and required features. In this paper we present a possibility how to integrate requirements into Feature Algebra.
@Techreport{Hoefner20109,
Author = {H{\"o}fner, P. and Mentl, S. and M{\"o}ller, B. and Scholz, W.},
Title = {Requirements in Feature Algebra},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201012},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201012_hoe_men_moe_scholz/}
}

P. Höfner, R. Khedri, B. Möller:
Supplementing Product Families with Behaviour. Technical Report 201013, Institute of Computer Science, University of Augsburg. 2010. direct link.
abstract  pdf  bibtex
Abstract:
A common approach to dealing with software requirements volatility is to define product families instead of single products. In earlier papers we have developed an algebra of such families that, roughly, consists in a more abstract view of andor trees of features as used in FeatureOriented Domain Analysis. A product family is represented by an algebraic term over the feature names; it can be manipulated using equational laws such as associativity or distributivity. Initially, only 'syntactic' models of the algebra were considered, giving more or less just the names of the features used in the various products of a family and certain interrelations such as mandatory occurrence and implication between or mutual exclusion of features, without attaching any kind of \"meaning\" to the features. While this is interesting and useful for determining the variety and number of possible members of such a family, it is wholly insufficient when it comes to talking about the correctness of families in a semantic manner. In the present paper we define a class of \"semantic\" models of the general abstract product family algebra that allows treating very relevant additional questions. In these models, the features of a family are requirements scenarios formalised as pairs of relational specifications of a proposed system and its environment. However, the paper is just intended as a proof of feasibility; we are convinced that the approach can also be employed for different semantic models such as general denotational or streambased semantics.
@Techreport{Hoefner20108,
Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
Title = {Supplementing Product Families with Behaviour},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201013},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201013_hoe_khe_moe/}
}

P. Höfner, B. Möller:
Fixing Zeno Gaps. Technical Report 201011, Institute of Computer Science, University of Augsburg. 2010. direct link.
abstract  pdf  bibtex
Abstract:
In computer science fixpoints play a crucial role. Most often least and greatest fixpoints are sufficient. However there are situations where other ones are needed. In this paper we study, on an algebraic base, a special fixpoint of the function f(x) = a⋅x that describes infinite iteration of an element a. We show that the greatest fixpoint is too imprecise. Special problems arise if the iterated element contains the possibility of stepping on the spot (e.g. skip in a programming language) or if it allows Zeno behaviour. We present a construction for a fixpoint that captures these phenomena in a precise way. The theory is presented and motivated using an example from hybrid system analysis.
@Techreport{Hoefner20107,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Fixing Zeno Gaps},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201011},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201011_hoe_moe/}
}

P. Höfner, M.E. Müller, S. Zeissler:
ATPPortal: A Userfriendly Webbased Interface for Automated Theorem Provers and for Automatically Generated Proofs. Technical Report 201010, Institute of Computer Science, University of Augsburg. 2010. direct link.
abstract  pdf  bibtex
Abstract:
This report describes the design, the implementation and the usage of a system for managing different systems for automated theorem proving and automatically generated proofs. In particular, we focus on a userfriendly webbased interface and a structure for collecting and cataloguing proofs in a uniform way. The second point hopefully helps to understand the structure of automatically generated proofs and builds a starting point for new insights for strategies for proof planning.
@Techreport{Hoefner20106,
Author = {H{\"o}fner, P. and M{\"u}ller, M.E. and Zeissler, S.},
Title = {{ATPPortal}: A Userfriendly Webbased Interface for Automated Theorem Provers and for Automatically Generated Proofs},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201010},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201010_hoe_mue_zei/}
}

P. Höfner, B. Möller:
An Extension of Feature Algebra. Technical Report 201009, Institute of Computer Science, University of Augsburg. 2010. direct link.
abstract  pdf  bibtex
Abstract:
Feature algebra was introduced as an abstract framework for feature oriented software development. One goal is to provide a common, clearly defined basis for the key ideas of feature orientation. So far, feature algebra captures major aspects of feature orientation, like the hierarchical structure of features and feature composition. However, as we will show, it is not able to model aspects at the level of code, i.e., situations where code fragments of different features have to be merged. With other words, it does not reflect details of concret implementations. In the paper we first present concrete models for the original axioms of feature algebra which represent the main concepts of feature oriented programs. This shows that the abstract feature algebra can be interpreted in different ways. We then use these models to show that the axioms of feature algebra do not reflect all aspects of feature orientation properly. This gives the motivation to extend the abstract algebra — which is the second main contribution of the paper. We modify the axioms and introduce the concept of an extended feature algebra. The original algebra can be retrieved by a single additional axiom. As third contribution we introduce more operators to coveer concepts like overriding in the abstract setting.
@Techreport{Hoefner20105,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {An Extension of Feature Algebra},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201009},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201009_hoe_moe/}
}

H.H. Dang, P. Höfner, B. Möller:
Algebraic Separation Logic. Technical Report 201006, Institute of Computer Science, University of Augsburg. 2010. direct link.
abstract  pdf  bibtex
Abstract:
We present an algebraic approach to separation logic. In particular, we give an algebraic characterisation for assertions of separation logic, discuss different classes of assertions and prove abstract laws fully algebraically. After that, we use our algebraic framework to give a relational semantics of the commands of the simple programming language associated with separation logic. On this basis we prove the frame rule in an abstract and concise way. We also propose a more general version of separating conjunction which leads to a frame rule that is easier to prove. In particular, we show how to algebraically formulate the requirement that a command does not change certain variables; this is also expressed more conveniently using the generalised separating conjunction. The algebraic view does not only yield new insights on separation logic but also shortens proofs due to a point free representation. It is largely firstorder and hence enables the use of offtheshelf automated theorem provers for verifying properties at a more abstract level.
@Techreport{Hoefner20104,
Author = {Dang, H.H. and H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Algebraic Separation Logic},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201006},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201006_dan_hoe_moe/}
}

H.H. Dang, P. Höfner:
Automated HigherOrder Reasoning in Quantales. Technical Report 201003, Institute of Computer Science, University of Augsburg. 2010. direct link.
abstract  pdf  bibtex
Abstract:
Originally developed as an algebraic characterisation for quantum mechanics, the algebraic structure of quantales nowadays finds widespread applications ranging from (noncommutative) logics to hybrid systems. We present an approach to bring reasoning in quantales into the realm of (fully) automated theorem proving. Hence the paper paves the way for automatisation in various (new) fields of applications. To achieve this goal and to receive a general approach (independent of any particular theorem prover), we use the TPTP Problem Library for higherorder logic. In particular, we give an encoding of quantales in the typed higherorder form (THF) and present some theorems about quantales which can be proved fully automatically. We further present prospective applications for our approach and discuss practical experiences using THF.
@Techreport{Hoefner20103,
Author = {Dang, H.H. and H{\"o}fner, P.},
Title = {Automated HigherOrder Reasoning in Quantales},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201003},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201003_dan_hoe/}
}

H.H. Dang, P. Höfner, B. Möller:
Towards Algebraic Separation Logic. Technical Report 200912, Institute of Computer Science, University of Augsburg. 2009. direct link.
abstract  pdf  bibtex
Abstract:
We present an algebraic approach to separation logic. In particular, we give algebraic characterisations for all constructs of separation logic like assertions and commands. The algebraic view does not only yield new insights on separation logic but also shortens proofs and enables the use of automated theorem provers for verifying properties at a more abstract level.
@Techreport{Hoefner20096,
Author = {Dang, H.H. and H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Towards Algebraic Separation Logic},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200912},
Year = {2009},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200912_dan_hoe_moe/}
}

P. Höfner, G. Struth:
On Automating the Calculus of Relations. Technical Report CS0805, Department of Computer Science, University of Sheffield. 2008.
abstract  pdf  bibtex
Abstract:
Relation algebras provide abstract equational axioms for the calculus of binary relations. They name an established area of mathematics with various applications in computer science. We prove more than hundred theorems of relation algebras with offtheshelf automated theorem provers. This yields a basic calculus from which more advance applications can be explored. Here, we present two examples from the formal methods literature. Our experiments not only further underline the feasibility of automated deduction in complex algebraic structures and provide theorem proving benchmarks, they also pave the way for lifting established formal methods such as B or Z to a new level of automation.
@Techreport{Hoefner200810,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {On Automating the Calculus of Relations},
Institution = {Department of Computer Science, University of Sheffield},
Number = {CS0805},
Year = {2008},
Url = {}
}

P. Höfner, R. Khedri, B. Möller:
Algebraic View Reconciliation. Technical Report 200713, Institute of Computer Science, University of Augsburg. 2007. direct link.
abstract  bibtex
Abstract:
Embedded systems such as automotive systems are very complex to specify. Since it is difficult to capture all their requirements or their design in one single model, approaches working with several system views are adopted. The main problem there is to keep these views coherent; the issue is known as view reconciliation. This paper proposes an algebraic solution. It uses sets of integration constraints that link (families of) system features in one view to other (families of) features in the same or a different view. Both families and constraints are formalized using a feature algebra. Besides presenting a constraint relation and its mathematical properties, the paper shows in several examples the suitability of this approach for a wide class of integration constraint formulations
@Techreport{Hoefner20078,
Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
Title = {Algebraic View Reconciliation},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200713},
Year = {2007},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200713_hoe_khe_moe/}
}

P. Höfner, F. Lautenbacher:
Algebraic Structure of Web Services. Technical Report 200712, Institute of Computer Science, University of Augsburg. 2007. direct link.
abstract  pdf  bibtex
Abstract:
The ServiceOriented Architecture is gaining more and more attention and one way of realising it is the usage of Web Services. But which Web Services need to be invoked to reach a goal and which parameters are necessary at the beginning or are returned at the end? In this report we present an algebraic structure of Web Services in order to formally describe the Web Services and assist the users in Web Service composition. Hence, we apply relation algebra, tests, Kleene star and modal operators to characterise Web Services and Web Service Composition.
@Techreport{Hoefner20077,
Author = {H{\"o}fner, P. and Lautenbacher, F.},
Title = {Algebraic Structure of Web Services},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200712},
Year = {2007},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200712_hoe_lau/}
}

P. Höfner, B. Möller:
An Algebra of Hybrid Systems. Technical Report 200708, Institute of Computer Science, University of Augsburg. 2007. direct link.
abstract  pdf  bibtex
Abstract:
Hybrid systems are heterogeneous systems characterised by the interaction of discrete and continuous dynamics. We present a trajectorybased algebraic model for describing hybrid systems; the trajectories used are closely related to streams. The algebra is based on left quantales and left semirings and provides a new application for these algebraic structures. We show that hybrid automata, which are probably the standard tool for describing hybrid systems, can conveniently be embedded into our algebra. Moreover we point out some important advantages of the algebraic approach. In particular, we show how to handle Zeno effects, which are excluded by most other authors. The development of the theory is illustrated by a running example and a larger case study.
@Techreport{Hoefner20075,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {An Algebra of Hybrid Systems},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200708},
Year = {2007},
Url = {www.informatik.uniaugsburg.de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200708_hoe_moe/}
}

P. Höfner, G. Struth:
Can Refinement be Automated?. Technical Report CS0708, Department of Computer Science, University of Sheffield. 2007. direct link.
abstract  pdf  bibtex
Abstract:
Relation algebras provide abstract equational axioms for the calculus of binary relations. They name an established area of mathematics with various applications in computer science. We prove more than hundred theorems of relation algebras with offtheshelf automated theorem provers. This yields a basic calculus from which more advance applications can be explored. Here, we present two examples from the formal methods literature. Our experiments not only further underline the feasibility of automated deduction in complex algebraic structures and provide theorem proving benchmarks, they also pave the way for lifting established formal methods such as B or Z to a new level of automation.
@Techreport{Hoefner20074,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Can Refinement be Automated?},
Institution = {Department of Computer Science, University of Sheffield},
Number = {CS0708},
Year = {2007},
Url = {www.dcs.shef.ac.uk/intranet/research/public/resmes/CS0708.pdf}
}

P. Höfner, G. Struth:
Automated Reasoning in Kleene Algebra. Technical Report CS0704, Department of Computer Science, University of Sheffield. 2007.
abstract  pdf  bibtex
Abstract:
It has often been claimed that model checking, special purpose automated deduction or interactive theorem proving are needed for formal program development. We demonstrate that offtheshelf automated proof and counterexample search is an interesting alternative if combined with the right domain model. We implement variants of Kleene algebras axiomatically in Prover9/Mace4 and perform proof experiments about Hoare, dynamic, temporal logics, concurrency control and termination analysis. They confirm that a simple automated analysis of some important program properties is possible. Particular benefits of this approach include \"soft\" model checking in a firstorder setting, crosstheory reasoning between standard formalisms and full automation of some (co)inductive arguments. Kleene algebras might therefore provide lightweight formal methods with heavyweight automation.
@Techreport{Hoefner20073,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Automated Reasoning in Kleene Algebra},
Institution = {Department of Computer Science, University of Sheffield},
Number = {CS0704},
Year = {2007},
Url = {}
}

P. Höfner, G. Struth:
Algebraic Notions of NonTermination. Technical Report CS0612, Department of Computer Science, University of Sheffield. 2006. direct link.
abstract  pdf  bibtex
Abstract:
We study and compare two notions of nontermination on idempotent semirings: infinite iteration and divergence. We determine them in various models and develop conditions for their coincidence. It turns out that divergence yields a simple and natural way of modelling infinite behaviour, whereas infinite iteration shows some anomalies.
@Techreport{Hoefner200611,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Algebraic Notions of NonTermination},
Institution = {Department of Computer Science, University of Sheffield},
Number = {CS0612},
Year = {2006},
Url = {www.dcs.shef.ac.uk/intranet/research/public/resmes/CS0612.pdf}
}

P. Höfner, B. Möller, K. Solin:
Omega Algebra, Demonic Refinement Algebra and Commands. Technical Report 200611, Institute of Computer Science, University of Augsburg. 2006. direct link.
abstract  pdf  bibtex
Abstract:
Weak omega algebra and demonic refinement algebra are two ways of describing systems with finite and infinite iteration. We show that these independently introduced kinds of algebras can actually be defined in terms of each other. By defining modal operators on the underlying weak semiring, that result directly gives a demonic refinement algebra of commands. This yields models in which extensionality does not hold. Since in predicatetransformer models extensionality always holds, this means that the axioms of demonic refinement algebra do not characterise predicatetransformer models uniquely. The omega and the demonic refinement algebra of commands both utilise the convergence operator that is analogous to the halting predicate of modal μcalculus. We show that the convergence operator can be defined explicitly in terms of infinite iteration and domain if and only if domain coinduction for infinite iteration holds.
@Techreport{Hoefner20067,
Author = {H{\"o}fner, P. and M{\"o}ller, B. and Solin, K.},
Title = {Omega Algebra, Demonic Refinement Algebra and Commands},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200611},
Year = {2006},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200611_hoe_moe_sol/}
}

P. Höfner, B. Möller:
Lazy Semiring Neighbours and some Applications. Technical Report 200609, Institute of Computer Science, University of Augsburg. 2006. direct link.
abstract  pdf  bibtex
Abstract:
We extend an earlier algebraic approach to Neighbourhood Logic (NL) from domain semirings to lazy semirings yielding lazy semiring neighbours. Furthermore we show three important applications for these. The first one extends NL to intervals with infinite length. The second one applies lazy semiring neighbours in an algebraic semantics of the branching time temporal logic CTL*. The third one sets up a connection between hybrid systems and lazy semiring neighbours.
@Techreport{Hoefner20066,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Lazy Semiring Neighbours and some Applications},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200609},
Year = {2006},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr20069_hoe_moe/}
}

B. Möller, P. Höfner, G. Struth:
Quantales and Temporal Logics. Technical Report 200606, Institute of Computer Science, University of Augsburg. 2006. direct link.
abstract  pdf  bibtex
Abstract:
We propose an algebraic semantics for the temporal logic CTL* and simplify it for its sublogics CTL and LTL. We abstractly represent state and path formulas over transition systems in Boolean left quantales. These are complete lattices with a multiplication that preserves arbitrary joins in its left argument and is isotone in its right argument. Over these quantales, the semantics of CTL* formulas can be encoded via finite and infinite iteration operators; the CTL and LTL operators can be related to domain operators. This yields interesting new connections between representations as known from the modal μcalculus and Kleene/ωalgebra.
@Techreport{Hoefner20063,
Author = {M{\"o}ller, B. and H{\"o}fner, P. and Struth, G.},
Title = {Quantales and Temporal Logics},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200606},
Year = {2006},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr20066_moe_hoe_str/}
}

P. Höfner, R. Khedri, B. Möller:
Feature Algebra. Technical Report 200604, Institute of Computer Science, University of Augsburg. 2006. direct link.
abstract  pdf  bibtex
Abstract:
Based on experience from the hardware industry, product families have entered the software development process as well, since software developers often prefer not to build a single product but rather a family of similar products that share at least one common functionality while having wellidentified variabilities. Such shared commonalities, also called features, reach from common hardware parts to software artefacts such as requirements, architectural properties, components, middleware, or code. We use idempotent semirings as the basis for a feature algebra that allows a formal treatment of the above notions as well as calculations with them. In particular models of feature algebra the elements are sets of products, i.e. product families. We extend the algebra to cover product lines, refinement, product development and product classification. Finally we briefly describe a prototype implementation of one particular model.
@Techreport{Hoefner20061,
Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
Title = {Feature Algebra},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200604},
Year = {2006},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr20064_hoe_khe_moe/}
}

P. Höfner:
Semiring Neighbours. Technical Report 200519, Institute of Computer Science, University of Augsburg. 2005. direct link.
abstract  pdf  bibtex
Abstract:
In 1996 Zhou and Hansen proposed a firstorder interval logic called Neighbourhood Logic (NL) for specifying liveness and fairness of computing systems and also defining notions of real analysis in terms of expanding modalities. After that, Roy and Zhou presented a sound and relatively complete Duration Calculus as an extension of NL. We present an embedding of NL into an idempotent semiring of intervals. This embedding allows us to extend NL from single intervals to sets of intervals as well as to extend the approach to arbitrary idempotent semirings. We show that most of the required properties follow directly from Galois connections, hence we get the properties for free. As one important result we get that some of the axioms which were postulated for NL can be dropped since they are theorems in our generalisation. Furthermore, we present some possible interpretations for neighbours beyond intervals. Here we discuss for example reachability in graphs and applications to hybrid systems. At the end of the paper we add finite and infinite iteration to NL and extend idempotent semirigs to Kleene algebras and omega algebras. These extensions are useful for formulating repetitive properties and procedures like loops.
@Techreport{Hoefner20055,
Author = {H{\"o}fner, P.},
Title = {Semiring Neighbours},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200519},
Year = {2005},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200519_hoe/}
}

A. Huhn, P. Höfner, W. Kießling:
Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System. Technical Report 200507, Institute of Computer Science, University of Augsburg. 2005. direct link.
abstract  pdf  bibtex
Abstract:
Advanced personalization techniques are required to cope with novel challenges posed by attributerich digital libraries. At the heart of our deeply personalized alerting system is one extensible preference model that serves all purposes. In this paper we focus on ontology and quality assessment in con junction with our search technology Preference XPath and XMLbased seman tic annotations of digital library multimedia objects. We evaluate the impacts of automatic query expansion by ontologies by embedding our alerting system P News as a black box or a glass box in a test lab. It changes configuration pa rameters on its own, feeds test cases to PNews, compares the results of differ ent configurations, and stores the result set for further evaluations. The most important indications of this work in progress are: The use of ontologies im proves the quality of the result set, generates further results of higher quality, and implies the use of knowledge to reduce a loss of focus.
@Techreport{Hoefner20052,
Author = {Huhn, A. and H{\"o}fner, P. and Kie{\ss}ling, W.},
Title = {Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200507},
Year = {2005},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/db/publications/all_db_techreports/tr20057_huh_hoe_kie/}
}

P. Höfner:
From Sequential Algebra to Kleene Algebra: Interval Modalities and Duration Calculus. Technical Report 200505, Institute of Computer Science, University of Augsburg. 2005. direct link.
abstract  pdf  bibtex
Abstract:
The duration calculus (DC) is a formal, algebraic system for specification and design of real time systems, where real numbers are used to model time and (Boolean valued) functions to formulate requirements. Since its introduction in 1991 by Chaochen, Hoare and Ravn it has been applied to many case studies and has been extended into several directions. E.g., there is an extension for specifying liveness and safety requirements. This report presents the duration calculus on the basis of Kleene algebra. Doing this we will analyse the DC in a new view.
@Techreport{Hoefner20051,
Author = {H{\"o}fner, P.},
Title = {From Sequential Algebra to Kleene Algebra: Interval Modalities and Duration Calculus},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200505},
Year = {2005},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr20055_hoe/}
}