A trustworthy framework for resource-aware embedded programming

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Downloads (Pure)


Systems with non-functional requirements, such as Energy, Time and Security (ETS), are of increasing importance due to the proliferation of embedded devices with limited resources such as drones, wireless sensors, and tablet computers. Currently, however, there are little to no programmer supported methodologies or frameworks to allow them to reason about ETS properties in their source code. Drive is one such existing framework supporting the developer by lifting non-functional properties to the source-level through the Contract Specification Language (CSL), allowing non-functional properties to be first-class citizens, and supporting programmer-written code-level contracts to guarantee the non-functional specifications of the program are met. In this paper, we extend the Drive system by providing rigorous implementations of the underlying proof-engine, modeling the specification of the annotations and assertions from CSL for a representative subset of C, called Imp. We define both an improved abstract interpretation that automatically derives proofs of assertions, and define inference algorithms for the derivation of both abstract interpretations and the context over which the interpretation is indexed. We use the dependently-typed programming language, Idris, to give a formal definition, and implementation, of our abstract interpretation. Finally, we show our well-formed abstract interpretation over some representative exemplars demonstrating provable assertions of ETS.
Original languageEnglish
Title of host publicationProceedings of International Symposium on Implementation and Application of Functional Languages (IFL'19)
EditorsJurriën Stutterheim, Wei Ngan Chin
Publication statusAccepted/In press - 11 Feb 2020
EventThe 31st symposium on Implementation and Application of Functional Languages (IFL 2019) - Singapore, Singapore
Duration: 25 Sept 201927 Sept 2019
Conference number: 31


ConferenceThe 31st symposium on Implementation and Application of Functional Languages (IFL 2019)
Abbreviated titleIFL 2019
Internet address


  • Dependent types
  • Idris
  • LIghtweight verification
  • Non-functional properties
  • Abstract interpretation
  • Proof-carrying code
  • Embedded systems


Dive into the research topics of 'A trustworthy framework for resource-aware embedded programming'. Together they form a unique fingerprint.

Cite this