Abstract Interpretation of PIC programs through Logic Programming

Kim Steen Henriksen, John Patrick Gallagher

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

A logic based general approach to abstract interpretation of low-level machine programs is reported. It is based on modelling the behavior of the machine as a logic program. General purpose program analysis and transformation of logic programs, such as partial evaluation and convex hull analysis, are applied to the logic based model of the machine. A small PIC microcontroller is used as a case study. An emulator for this microcontroller is written in Prolog, and standard programming transformations and analysis techniques are used to specialise this emulator with respect to a given PIC program. The specialised emulator can now be further analysed to gain insight into the given program for the PIC microcontroller. The method describes a general framework for applying abstractions, illustrated here by linear constraints and convex hull analysis, to logic programs. Using these techniques on the specialised PIC emulator, it is possible to obtain constraints on and linear relations between data registers, enabling detection of for instance overflows, branch conditions and so on.
Original languageEnglish
Title of host publicationSixth IEEE International Workshop on Source Code Analysis and Manipulation
PublisherIEEE
Publication date2006
Pages184-193
ISBN (Print)0769523536
Publication statusPublished - 2006
EventSixth IEEE International Workshop on Source Code Analysis and Manipulation - Philadelphia, PA, United States
Duration: 27 Sept 200629 Sept 2006
Conference number: 6

Conference

ConferenceSixth IEEE International Workshop on Source Code Analysis and Manipulation
Number6
Country/TerritoryUnited States
CityPhiladelphia, PA
Period27/09/200629/09/2006

Cite this