Skip to content

Research at St Andrews

Type-driven verification of non-functional properties

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

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 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 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. Programming heterogeneous parallel machines using refactoring and Monte-Carlo tree search

    Brown, C. M., Janjic, V., Goli, M. & McCall, J., Aug 2020, In: International Journal of Parallel Programming. 48, 4, p. 583–602 20 p.

    Research output: Contribution to journalArticlepeer-review

  2. Refactoring GrPPI: generic refactoring for generic parallelism in C++

    Brown, C. M., Janjic, V., Barwell, A. D., Garcia, J. D. & MacKenzie, K., 10 Jul 2020, In: International Journal of Parallel Programming. First Online, 23 p.

    Research output: Contribution to journalArticlepeer-review

  3. Restoration of legacy parallelism in C and C++ applications

    Brown, C. M., Barwell, A. D. & Janjic, V., 1 Jul 2020, (Accepted/In press).

    Research output: Contribution to conferencePaperpeer-review

  4. A hybrid approach to parallel pattern discovery in C++

    Brown, C. M., Janjic, V., Barwell, A. D., Thomson, J. D., Castañeda Lozano, R., Cole, M., Franke, B., Garcia-Sanchez, J. D., Del Rio Astorga, D. & MacKenzie, K., 14 May 2020, 2020 28th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP). IEEE Computer Society, 5 p. 9092377. (Proceedings - Euromicro Workshop on Parallel and Distributed Processing).

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

  5. A trustworthy framework for resource-aware embedded programming

    Barwell, A. D. & Brown, C. M., 11 Feb 2020, (Accepted/In press) Proceedings of International Symposium on Implementation and Application of Functional Languages (IFL'19). ACM

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

ID: 260324246

Top