Type-driven verification of non-functional properties

Christopher Mark Brown, Adam David Barwell, Yoann Marquer, Celine Minh, Olivier Zendra

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

1 Downloads (Pure)


Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification frame-work, called Drive, which allows a developer to reason about ETS or other non-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.
Original languageEnglish
Title of host publicationProceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019 (PPDP '19)
Place of PublicationNew York
Number of pages15
ISBN (Electronic)9781450372497
Publication statusPublished - 7 Oct 2019
Event21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019) - Porto, Portugal
Duration: 7 Oct 20199 Oct 2019
Conference number: 21


Conference21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019)
Abbreviated titlePPDP 2019
Internet address


  • C
  • Time
  • Energy
  • Security
  • Non-functional properties
  • Proofs
  • Verification
  • Contracts


Dive into the research topics of 'Type-driven verification of non-functional properties'. Together they form a unique fingerprint.

Cite this