Skip to content

Research at St Andrews

Type-driven verification of extra-functional properties

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

Open Access Status

  • Embargoed (until 7/10/19)

Author(s)

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

School/Research organisations

Abstract

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.
Close

Details

Original languageEnglish
Title of host publication21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019)
PublisherACM
Publication statusAccepted/In press - 21 Jul 2019
Event21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019) - Porto, Portugal
Duration: 7 Oct 20199 Oct 2019
Conference number: 21
http://ppdp2019.macs.hw.ac.uk/

Conference

Conference21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019)
Abbreviated titlePPDP 2019
CountryPortugal
CityPorto
Period7/10/199/10/19
Internet address

    Research areas

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

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. The Missing Link! A new skeleton for evolutionary multi-agent systems in Erlang

    Stypka, J., Turek, W., Byrski, A., Kisiel-Dorohinicki, M., Barwell, A. D., Brown, C. M., Hammond, K. & Janjic, V., Feb 2018, In : International Journal of Parallel Programming. 46, 1, p. 4-22 19 p.

    Research output: Contribution to journalArticle

  2. Towards semi-automatic data-type translation for parallelism in Erlang

    Barwell, A. D., Brown, C. M., Castro, D. & Hammond, K., 23 Sep 2016, Proceedings of the 15th International Workshop on Erlang. New York: ACM, p. 60-61

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

  3. Using “program shaping” and algorithmic skeletons to parallelise an evolutionary multi-agent system in Erlang

    Barwell, A. D., Brown, C. M., Hammond, K., Turek, W. & Byrski, A., 2016, In : Computing and Informatics. 35, 4, 37 p.

    Research output: Contribution to journalArticle

ID: 260324246