Issue

Leibniz Transactions on Embedded Systems, Volume 10, Issue 1

LITES, Volume 10, Issue 1

Publication Details

  • published at: 2025-04-16
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Access Numbers

Documents

No documents found matching your filter selection.
Document
DOI: 10.4230/LITES.10.1.1
GDBMiner: Mining Precise Input Grammars on (Almost) Any System

Authors: Max Eisele, Johannes Hägele, Christopher Huth, and Andreas Zeller

Abstract
If one knows the input language of the system to be tested, one can generate inputs in a very efficient manner. Grammar-based fuzzers, for instance, produce inputs that are syntactically valid by construction. They are thus much more likely to be accepted by the program under test and to reach code beyond the input parser. Grammar-based fuzzers, however, need a grammar in the first place. Grammar miners are set to extract such grammars from programs. However, current grammar mining tools place huge demands on the source code they are applied on, or are too imprecise, both preventing adoption in industrial practice. We present GDBMiner, a tool to mine input grammars for binaries and executables in any (compiled) programming language, on any operating system, using any processor architecture, even without source code. GDBMiner leverages the GNU debugger (GDB) to step through the program and determine which code locations access which input bytes, generalizing bytes accessed by the same location into grammar elements. GDBMiner is slow, but versatile - and precise: In our evaluation, GDBMiner produces grammars as precise as the (more demanding) Cmimid tool, while producing more precise grammars than the (less demanding) Arvada black-box approach. GDBMiner can be applied on any recursive descent parser that can be debugged via GDB and is available as open source.
Cite as

Max Eisele, Johannes Hägele, Christopher Huth, and Andreas Zeller. GDBMiner: Mining Precise Input Grammars on (Almost) Any System. In LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1, pp. 1:1-1:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{eisele_et_al:LITES.10.1.1,
  author =	{Eisele, Max and H\"{a}gele, Johannes and Huth, Christopher and Zeller, Andreas},
  title =	{{GDBMiner: Mining Precise Input Grammars on (Almost) Any System}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{1:1--1:26},
  ISSN =	{2199-2002},
  year =	{2025},
  volume =	{10},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.10.1.1},
  URN =		{urn:nbn:de:0030-drops-230134},
  doi =		{10.4230/LITES.10.1.1},
  annote =	{Keywords: program analysis, testing, input grammar, fuzzing, grammar mining}
}
Document
DOI: 10.4230/LITES.10.1.2
Towards a Coq-verified Chain of Esterel Semantics

Authors: Lionel Rieg and Gérard Berry

Abstract
This article focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel’s circuit semantics used by compilers to generate software code and hardware designs. The article also comes with formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics, except for the loop construct of Esterel.
Cite as

Lionel Rieg and Gérard Berry. Towards a Coq-verified Chain of Esterel Semantics. In LITES, Volume 10, Issue 1 (2025). Leibniz Transactions on Embedded Systems, Volume 10, Issue 1, pp. 2:1-2:54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{rieg_et_al:LITES.10.1.2,
  author =	{Rieg, Lionel and Berry, G\'{e}rard},
  title =	{{Towards a Coq-verified Chain of Esterel Semantics}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{2:1--2:54},
  ISSN =	{2199-2002},
  year =	{2025},
  volume =	{10},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.10.1.2},
  URN =		{urn:nbn:de:0030-drops-230144},
  doi =		{10.4230/LITES.10.1.2},
  annote =	{Keywords: Esterel programming language, formal verification, Coq proof assistant}
}

Filters

  • Authors
  • B
  • Berry, Gérard
  • E
  • Eisele, Max
  • H
  • Hägele, Johannes
  • Huth, Christopher
  • R
  • Rieg, Lionel
  • Z
  • Zeller, Andreas

  • Subjects
  • Computer systems organization
  • Computer systems organization → Embedded software
  • Computer systems organization → Real-time languages
  • Hardware
  • Hardware → Theorem proving and SAT solving
  • Security and privacy
  • Security and privacy → Logic and verification
  • Software and its engineering
  • Software and its engineering → Operational analysis
  • Software and its engineering → Software testing and debugging
  • Software and its engineering → Syntax
  • Theory of computation
  • Theory of computation → Operational semantics
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact