Publications - Henrik Barthels

Peer Reviewed Conference Publications

  1. A Compiler for Linear Algebra Operations
    SPLASH '16 Companion, ACM, October 2016.
    Student Research Competition.
    @inproceedings{Barthels2016:280,
        author    = "Henrik Barthels",
        title     = "A Compiler for Linear Algebra Operations",
        booktitle = "SPLASH '16 Companion",
        year      = 2016,
        month     = oct,
        publisher = "ACM",
        note      = "Student Research Competition",
        url       = "http://hpac.rwth-aachen.de/~barthels/publications/ACM_SRC_2016_abstract.pdf"
    }
    In this paper we present a compiler that translates arithmetic expressions containing matrices to efficient sequences of calls to basic linear algebra kernels.
    abstractwebPDFbibtexhide
  2. Juggrnaut – An Abstract JVM
    Jonathan Heinen, Henrik Barthels and Christina Jansen
    International Conference on Formal Verification of Object-Oriented Software, pp. 142-159, 2011.
    @inproceedings{Heinen2011:370,
        author       = "Jonathan Heinen and Henrik Barthels and Christina Jansen",
        title        = "Juggrnaut – An Abstract JVM",
        booktitle    = "International Conference on Formal Verification of Object-Oriented Software",
        year         = 2011,
        pages        = "142--159",
        organization = "Springer",
        url          = "http://hpac.rwth-aachen.de/~barthels/publications/juggrnaut.pdf"
    }
    We introduce a new kind of hypergraphs and hyperedge replacement grammars, where nodes are associated types. We use them to adapt the abstraction framework Juggrnaut presented by us in [7, 8] – for the verification of Java Bytecode programs. The framework is extended to handle additional concepts needed for the analysis of Java Bytecode like null pointers and method stacks as well as local and static variables. We define the abstract transition rules for a significant subset of opcodes and show how to compute the abstract state space. Finally we complete the paper with some experimental results.
    abstractPDFbibtexhide

Thesis

  1. Systematic Generation of Algorithms for Iterative Methods
    Master's Thesis, RWTH Aachen, March 2015.
    @mastersthesis{Barthels2015:240,
        author = "Henrik Barthels",
        title  = "Systematic Generation of Algorithms for Iterative Methods",
        school = "RWTH Aachen",
        year   = 2015,
        type   = "Master's Thesis",
        month  = mar,
        url    = "https://arxiv.org/pdf/1703.00279"
    }
    webPDFbibtexhide

Others

  1. A Compiler for Linear Algebra Operations
    Poster, 2 November 2016.
    ACM Student Research Competition at SPLASH 2016.
    @misc{Barthels2016:948,
        author = "Henrik Barthels",
        title  = "A Compiler for Linear Algebra Operations",
        month  = nov,
        year   = 2016,
        note   = "ACM Student Research Competition at SPLASH 2016",
        type   = "Poster",
        url    = "http://hpac.rwth-aachen.de/~barthels/publications/ACM_SRC_2016_poster.pdf"
    }
    PDFbibtexhide
  2. The Matrix Chain Algorithm to Compile Linear Algebra Expressions
    Two-page abstract, 31 October 2016.
    DSLDI 2016.
    @misc{Barthels2016:600,
        author      = "Henrik Barthels and Paolo Bientinesi",
        title       = "The Matrix Chain Algorithm to Compile Linear Algebra Expressions",
        month       = oct,
        year        = 2016,
        note        = "DSLDI 2016",
        type        = "Two-page abstract",
        institution = "RWTH Aachen",
        url         = "https://arxiv.org/pdf/1611.05660"
    }
    webPDFbibtexhide
  3. Automata-Based Detection of Hypergraph Embeddings
    Bachelor's Thesis, RWTH Aachen, September 2011.
    @misc{Barthels2011:804,
        author = "Henrik Barthels",
        title  = "Automata-Based Detection of Hypergraph Embeddings",
        month  = sep,
        year   = 2011,
        type   = "Bachelor's Thesis, RWTH Aachen",
        url    = "http://hpac.rwth-aachen.de/~barthels/publications/bachelor_thesis.pdf"
    }
    The verification of programs using pointers and dynamic data structures requires to deal with potentially infinite state spaces. Because of that, it is reasonable to use abstraction techniques capable of dealing with those potentially infinite structures. The Juggrnaut framework applies hyperedge replacement grammars to dynamically abstract and concretize parts of a heap. Abstraction is done by the backwards application of grammar rules, which is related to subgraph isomorphism and therefore NP-complete. In this thesis, after giving a formal definition to hypergraphs, hyperedge replacement and heap representation, an automata model is introduced which is able to detect embeddings of grammar rules with certain properties efficiently. We provide an algorithm to construct an automaton that is able to detect a given set of embeddings of grammar rules. Finally, proofs of the NP-completeness of subgraph isomorphism on hypergraphs and embedding detection in general are presented.
    abstractPDFbibtexhide