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.
@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} }
Feedback for Dagstuhl Publishing