h1

% IMPORTANT: The following is UTF-8 encoded.  This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.

@MASTERSTHESIS{QuirsAraya:229985,
      author       = {Quirós Araya, Gustavo},
      title        = {{S}tatic byte-code analysis for state space reduction},
      address      = {Aachen},
      publisher    = {Publikationsserver der RWTH Aachen University},
      reportid     = {RWTH-CONV-144790},
      pages        = {VIII, 101 S.},
      year         = {2011},
      note         = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
                      University; Aachen, Techn. Hochsch., Masterarbeit, 2006},
      abstract     = {NIPS is a virtual machine for the generation of
                      state-transition systems of concurrent models, and is
                      designed to serve as a foundation for the development of
                      model checking applications. Like any explicit-state
                      representation, the transition systems produced by NIPS
                      suffer from the state-explosion problem, by which models
                      have exponentially large state spaces. This work is
                      dedicated to the reduction of the effect of the
                      state-explosion problem in NIPS. State space reduction works
                      by obtaining a reduced state-transition system from a model,
                      which is equivalent to the original system under a given
                      specification, or a given set of specifications. Model
                      checking may be applied to the reduced system instead of to
                      the original one, thus obtaining the same result in a more
                      efficient manner. NIPS features a byte-code language for
                      encoding concurrent models. High-level modeling languages
                      may be compiled to this byte-code, and the interpretation of
                      the byte-code by the machine results in the construction of
                      the model’s state space representation. This architecture
                      allows us to implement on-the-fly reductions merely by
                      transforming the byte-code to another whose state-transition
                      system is a reduced version of the original, and employing
                      information gathered from static analysis of the byte-code
                      in the process.},
      keywords     = {Programmanalyse (SWD) / Compiler (SWD) / Model Checking
                      (SWD) / Zustandsraum (SWD) / Programmoptimierung (SWD) /
                      Verteiltes System (SWD)},
      cin          = {120000 / 121310},
      ddc          = {004},
      cid          = {$I:(DE-82)120000_20140620$ / $I:(DE-82)121310_20140620$},
      shelfmark    = {I.6.4 * D.3.4 * C.2.4},
      typ          = {PUB:(DE-HGF)19},
      urn          = {urn:nbn:de:hbz:82-opus-36528},
      doi          = {10.18154/RWTH-CONV-144790},
      url          = {https://publications.rwth-aachen.de/record/229985},
}