Type-Driven Verification of Non-functional Properties - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Type-Driven Verification of Non-functional Properties

Résumé

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 framework, 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.
Fichier principal
Vignette du fichier
ppdp2019.pdf (593.73 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02314723 , version 1 (22-10-2019)

Identifiants

Citer

Christopher Brown, Adam D Barwell, Yoann Marquer, Céline Minh, Olivier Zendra. Type-Driven Verification of Non-functional Properties. PPDP 2019 - 21st International Symposium on Principles and Practice of Declarative Programming, Oct 2019, Porto, Portugal. pp.1-15, ⟨10.1145/3354166.3354171⟩. ⟨hal-02314723⟩
170 Consultations
270 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More