| 1. |
|
|
| 2. |
- Abrahamsson, Oskar, 1986, et al.
(författare)
-
Candle: A Verified Implementation of HOL Light
- 2022
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. ; 237
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a fully verified interactive theorem prover for higher-order logic, more specifically: a fully verified clone of HOL Light. Our verification proof of this new system results in an end-to-end correctness theorem that guarantees the soundness of the entire system down to the machine code that executes at runtime. Our theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. Our implementation consists of a read-eval-print loop (REPL) that executes the CakeML compiler internally. Throughout this work, we have strived to make the REPL of the new system provide a user experience as close to HOL Light's as possible. To this end, we have, e.g., made the new system parse the same variant of OCaml syntax as HOL Light. All of the work described in this paper has been carried out in the HOL4 theorem prover.
|
|
| 3. |
- Abrahamsson, Oskar, 1986, et al.
(författare)
-
Proof-Producing Synthesis of CakeML from Monadic HOL Functions
- 2020
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 64:7, s. 1287-1306
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.
|
|
| 4. |
- Lööw, Andreas, 1988, et al.
(författare)
-
Verified Compilation on a Verified Processor
- 2019
-
Ingår i: PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19). - New York, NY, USA : ACM. - 9781450367127 ; , s. 1041-1053
-
Konferensbidrag (refereegranskat)abstract
- Developing technology for building verified stacks, i.e., computer systems with comprehensive proofs of correctness, is one way the science of programming languages furthers the computing discipline. While there have been successful projects verifying complex, realistic system components, including compilers (software) and processors (hardware), to date these verification efforts have not been compatible to the point of enabling a single end-to-end correctness theorem about running a verified compiler on a verified processor. In this paper we show how to extend the trustworthy development methodology of the CakeML project, including its verified compiler, with a connection to verified hardware. Our hardware target is Silver, a verified proof-of-concept processor that we introduce here. The result is an approach to producing verified stacks that scales to proving correctness, at the hardware level, of the execution of realistic software including compilers and proof checkers. Alongside our hardware-level theorems, we demonstrate feasibility by hosting and running our verified artefacts on an FPGA board.
|
|
| 5. |
- Tan, Yong Kiam, et al.
(författare)
-
A new verified compiler backend for CakeML
- 2016
-
Ingår i: ACM SIGPLAN Notices. - New York, NY, USA : ACM. - 1523-2867. ; 51:9, s. 60-73
-
Tidskriftsartikel (refereegranskat)abstract
- We have developed and mechanically verified a new compiler backend for CakeML. Our new compiler features a sequence of intermediate languages that allows it to incrementally compile away high-level features and enables verification at the right levels of semantic detail. In this way, it resembles mainstream (unverified) compilers for strict functional languages. The compiler supports efficient curried multi-Argument functions, configurable data representations, exceptions that unwind the call stack, register allocation, and more. The compiler targets several architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V. In this paper, we present the overall structure of the compiler, including its 12 intermediate languages, and explain how everything fits together. We focus particularly on the interaction between the verification of the register allocator and the garbage collector, and memory representations. The entire development has been carried out within the HOL4 theorem prover.
|
|
| 6. |
- Victor, Nancy, et al.
(författare)
-
Federated learning for iout : Concepts, applications, challenges and future directions
- 2022
-
Ingår i: IEEE Internet of Things Magazine (IoT). - 2576-3180 .- 2576-3199. ; 5:4
-
Tidskriftsartikel (refereegranskat)abstract
- Internet of Underwater Things (IoUT) have gained rapid momentum over the past decade with applications spanning from environmental monitoring and exploration, defence applications, etc. The traditional IoUT systems use machine learning (ML) approaches which cater the needs of reliability, efficiency and timeliness. However, an extensive review of the various studies conducted highlight the significance of data privacy and security in IoUT frameworks as a predominant factor in achieving desired outcomes in mission critical applications. Federated learning (FL) is a secured, decentralized framework which is a recent development in ML, that can help in fulfilling the challenges faced by conventional ML approaches in IoUT. This article presents an overview of the various applications of FL in IoUT, its challenges, open issues and indicates direction of future research prospects.
|
|
