Horn Binary Serialization Analysis

Gabriele Paganelli

A bit layout is a sequence of fields of certain bit lengths that specifies how to interpret a serial stream, e.g., the MP3 audio format. A layout with variable length fields needs to include meta-information to help the parser interpret unambiguously the rest of the stream; e.g. a field providing the length of a following variable length field. If no such information is available, then the layout is ambiguous. I present a linear-time algorithm to determine whether a layout is ambiguous or not by modelling the behaviour of a serial parser reading the stream as forward chaining reasoning on a collection of Horn clauses.

In John P. Gallagher and Philipp Rümmer: Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS2016), Eindhoven, The Netherlands, 3rd April 2016, Electronic Proceedings in Theoretical Computer Science 219, pp. 56–68.
Published: 14th July 2016.

ArXived at: http://dx.doi.org/10.4204/EPTCS.219.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org