Logo des Repositoriums

Auflistung nach Autor:in "Hofmann, Martin"

1 - 3 von 3
  • Konferenzbeitrag
    Formal Semantics of Synchronous Transfer Architecture
    (Modellierung 2014, 2014) Cichon, Gordon; Hofmann, Martin
    This paper explores the use of formal verification methods for complex and highly parallel state machines. For this purpose, a framework named Synchronous Transfer Architecture (STA) is being used. STA is a generic framework for digital hardware development that contains VLIW, FPGA, and hardwired ASIC architectures as corner cases. It maintains a strictly deterministic system behavior in order to achieve substantial savings in hardware costs, thus enabling systems with high clock speed, low power consumption and small die area. The high degree of parallelism requires a diligent development methodology to avoid implementation errors. Consequently, formal verification is the methodology of choice for reliable verification. The contribution of this paper is a formal semantics for the STA hardware architecture framework. This semantics is then used for the formal verification of an optimized parallel implementation of Fast Fourier Transformation (FFT) on STA. This is achieved using a combination of the semantics and symbolic evaluation.
  • Zeitschriftenartikel
    Hypertext/Hypermedia
    (Informatik Spektrum: Vol. 12, No. 4, 1989) Hofmann, Martin; Cordes, Ralf; Langendörfer, Horst
  • Zeitschriftenartikel
    Schema-Guided Inductive Functional Programming
    (KI - Künstliche Intelligenz: Vol. 26, No. 1, 2012) Hofmann, Martin
    Inductive Program Synthesis or Inductive Programming (IP) is the task of generating (recursive) programs from an incomplete specification, such as input/output (I/O) examples. All known IP algorithms can be described as search in the space of all candidate programs, with consequently exponential complexity. To constrain the search space and guide the search traditionally program schemes are used, usually given a priori by an expert user. Consequently, all further given data is interpreted w.r.t. this schema which now almost exclusively decides on success and failure, depending on whether it fits the data or not. Instead of trying to fit the data to a given schema indiscriminately, in my thesis (Schema-guided inductive functional programmin through automatic detection of type morphisms, 2010) I proposed to utilise knowledge about data types to choose and fit a suitable schema to the data! Recursion operators associated with data type definitions are well known in functional programming, but less in IP. I showed how to exploit universal properties of type morphisms which may be detected in the given I/O examples. This technique allows to introduce generic recursion schemes, such as catamorphisms or paramorphisms, on arbitrary inductive data types in the analytical inductive functional programming system Igor II which was already presented here in a previous issue (Kitzelmann in Künstl. Intell. 25:179–182, 2011).