Skip to content

Research at St Andrews

University > Research portal > Research publications > Type-driven verification of non-functional properties

Type-driven verification of non-functional properties

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

DOI

Open Access permissions

Open

Links

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

Details

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
PublisherACM
Pages1-15
Number of pages15
ISBN (Electronic)9781450372497
DOIs
Publication statusPublished - 7 Oct 2019
Event21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019) - Porto, Portugal
Duration: 7 Oct 2019 → 9 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/19 → 9/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. Refactoring for introducing and tuning parallelism for heterogeneous multicore machines in Erlang

    Janjic, V., Brown, C., Barwell, A. & Hammond, K., 24 Jun 2019, In : Concurrency and Computation : Practice and Experience. Early View, p. 1-25 25 p., e5420.

    Research output: Contribution to journal › Article

  2. Reasoning about non-functional properties using compiler intrinsic function annotations

    Brown, C. M., Jadhav, S., Roth, M., Falk, H. & Barwell, A. D., Jun 2019.

    Research output: Contribution to conference › Paper

  3. Finding parallel functional pearls: automatic parallel recursion scheme detection in Haskell functions via anti-unification

    Barwell, A. D., Brown, C. & Hammond, K., Feb 2018, In : Future Generation Computer Systems. 79, Part 2, p. 669-686

    Research output: Contribution to journal › Article

  4. 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 journal › Article

  5. 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 proceeding › Conference contribution

ID: 260324246

Top