Quelle  root.bib

@article{Armstrong2019,
abstract = {Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification. But in practice, they are typically prose and pseudocode documents, not rigorous or executable artifacts, leaving software and verification on shaky ground. In this paper, we present rigorous semantic models for the sequential behaviour of large parts of the mainstream ARMv8-A, RISC-V, and MIPS architectures, and the research CHERI-MIPS architecture, that are complete enough to boot operating systems, variously Linux, FreeBSD, or seL4. Our ARMv8-A models are automatically translated from authoritative ARM-internal definitions, and (in one variant) tested against the ARM Architecture Validation Suite. We do this using a custom language for ISA semantics, Sail, with a lightweight dependent type system, that supports automatic generation of emulator code in C and OCaml, and automatic generation of proof-assistant definitions for Isabelle, HOL4, and (currently only for MIPS) Coq. We use the former for validation, and to assess specification coverage. To demonstrate the usability of the latter, we prove (in Isabelle) correctness of a purely functional characterisation of ARMv8-A address translation. We moreover integrate the RISC-V model into the RMEM tool for (user-mode) relaxed-memory concurrency exploration. We prove (on paper) the soundness of the core Sail type system. We thereby take a big step towards making the architectural abstraction actually well-defined, establishing foundations for verification and reasoning.},
author = {Armstrong, Alasdair and Pulte, Christopher and Flur, Shaked and Stark, Ian and Krishnaswami, Neel and Sewell, Peter and Bauereiss, Thomas and Campbell, Brian and Reid, Alastair and Gray, Kathryn E. and Norton, Robert M. and Mundkur, Prashanth and Wassell, Mark and French, Jon},
doi = {10.1145/3290384},
file = {:E$\backslash$:/Mark/PhD/ReadingMaterial/SAIL/sail-popl2019.pdf:pdf},
issn = {2475-1421},
journal = {Proceedings of the ACM on Programming Languages},
number = {POPL},
pages = {1--31},
title = {{ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS}},
volume = {3},
year = {2019}
}
@article{Vazou2014,
abstract = {SMT-based checking of refinement types for call-by-value languages is a well-studied subject. Unfortunately, the classical translation of refinement types to verification conditions is unsound under lazy evaluation. When checking an expression, such systems implicitly assume that all the free variables in the expression are bound to values. This property is trivially guaranteed by eager, but does not hold under lazy, evaluation. Thus, to be sound and precise, a refinement type system for Haskell and the corresponding verification conditions must take into account which subset of binders actually reduces to values. We present a stratified type system that labels binders as potentially diverging or not, and that (circularly) uses refinement types to verify the labeling. We have implemented our system in LIQUIDHASKELL and present an experimental evaluation of our approach on more than 10,000 lines of widely used Haskell libraries. We show that LIQUIDHASKELL is able to prove 96{\%} of all recursive functions terminating, while requiring a modest 1.7 lines of termination-annotations per 100 lines of code.},
annote = {ICFP Video - https://www.youtube.com/watch?v=vqvNQixKr6w},
archivePrefix = {arXiv},
arxivId = {arXiv:1604.02480v1},
author = {Vazou, Niki and Seidel, Eric L and Peyton-jones, Simon},
doi = {10.1145/2628136.2628161},
eprint = {arXiv:1604.02480v1},
file = {:C$\backslash$:/Users/User/AppData/Local/Mendeley Ltd./Mendeley Desktop/Downloaded/Merz, Vanzetto - 2014 - Refinement types for Haskell.pdf:pdf},
isbn = {9781450328739},
issn = {15232867},
journal = {ICFP '14 Proceedings of the 19th ACM SIGPLAN international conference on Functional programming},
mendeley-groups = {Semantic Tools/RefinementTypes},
title = {{Refinement Types For Haskell}},
year = {2014}
}