Search Results

Documents authored by Brauer, Jörg

Document
Complete Volume
DOI: 10.4230/OASIcs.SSV.2011
OASIcs, Volume 24, SSV'11, Complete Volume

Authors: Jörg Brauer, Marco Roveri, and Hendrik Tews

Published in: OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012)

Abstract
OASIcs, Volume 24, SSV'11, Complete Volume
Cite as

6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@Proceedings{brauer_et_al:OASIcs.SSV.2011,
  title =	{{OASIcs, Volume 24, SSV'11, Complete Volume}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011},
  URN =		{urn:nbn:de:0030-drops-35937},
  doi =		{10.4230/OASIcs.SSV.2011},
  annote =	{Keywords: Software/Program Verification}
}
Document
Front Matter
DOI: 10.4230/OASIcs.SSV.2011.i
Frontmatter, Table of Contents, Preface

Authors: Jörg Brauer, Marco Roveri, and Hendrik Tews

Published in: OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012)

Abstract
Frontmatter, Table of Contents, Preface
Cite as

6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. i-vii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{brauer_et_al:OASIcs.SSV.2011.i,
  author =	{Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
  title =	{{Frontmatter, Table of Contents, Preface}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  pages =	{i--vii},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.i},
  URN =		{urn:nbn:de:0030-drops-35854},
  doi =		{10.4230/OASIcs.SSV.2011.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface}
}
Document
DOI: 10.4230/OASIcs.SSV.2011.32
Adaptable Value-Set Analysis for Low-Level Code

Authors: Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen

Published in: OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012)

Abstract
This paper presents a framework for binary code analysis that uses only SAT-based algorithms. Within the framework, incremental SAT solving is used to perform a form of weakly relational value-set analysis in a novel way, connecting the expressiveness of the value sets to computational complexity. Another key feature of our framework is that it translates the semantics of binary code into an intermediate representation. This allows for a straightforward translation of the program semantics into Boolean logic and eases the implementation efforts, too. We show that leveraging the efficiency of contemporary SAT solvers allows us to prove interesting properties about medium-sized microcontroller programs.
Cite as

Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen. Adaptable Value-Set Analysis for Low-Level Code. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 32-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{brauer_et_al:OASIcs.SSV.2011.32,
  author =	{Brauer, J\"{o}rg and Hansen, Ren\'{e} Rydhof and Kowalewski, Stefan and Larsen, Kim G. and Olesen, Mads Chr.},
  title =	{{Adaptable Value-Set Analysis for Low-Level Code}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  pages =	{32--43},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.32},
  URN =		{urn:nbn:de:0030-drops-35884},
  doi =		{10.4230/OASIcs.SSV.2011.32},
  annote =	{Keywords: Abstract interpretation, SAT solving, embedded systems}
}
Document
DOI: 10.4230/OASIcs.MEMICS.2010.101
Test-Case Generation for Embedded Binary Code Using Abstract Interpretation

Authors: Thomas Reinbacher, Jörg Brauer, Martin Horauer, Andreas Steininger, and Stefan Kowalewski

Published in: OASIcs, Volume 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (2011)

Abstract
This paper describes a framework for test-case generation for microcontroller binary programs using abstract interpretation techniques. The key idea of our approach is to derive program invariants a priori, and then use backward analysis to obtain test vectors that are executed on the target microcontroller. Due to the structure of binary code, the abstract interpretation framework is based on propositional encodings of the program semantics and SAT solving.
Cite as

Thomas Reinbacher, Jörg Brauer, Martin Horauer, Andreas Steininger, and Stefan Kowalewski. Test-Case Generation for Embedded Binary Code Using Abstract Interpretation. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. 101-108, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{reinbacher_et_al:OASIcs.MEMICS.2010.101,
  author =	{Reinbacher, Thomas and Brauer, J\"{o}rg and Horauer, Martin and Steininger, Andreas and Kowalewski, Stefan},
  title =	{{Test-Case Generation for Embedded Binary Code Using Abstract Interpretation}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{101--108},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Matyska, Ludek and Kozubek, Michal and Vojnar, Tomas and Zemcik, Pavel and Antos, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2010.101},
  URN =		{urn:nbn:de:0030-drops-30586},
  doi =		{10.4230/OASIcs.MEMICS.2010.101},
  annote =	{Keywords: Test-Case Generation, Embedded Binary Code, Abstract Interpretation}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact