Package: wnpp Severity: wishlist Owner: Bo YU <tsu.y...@gmail.com> X-Debbugs-Cc: debian-devel@lists.debian.org
* Package name : sail-ocaml Version : 0.17.1 Upstream Contact: rems-project * URL : https://github.com/rems-project/sail * License : BSD-2-Clause Programming Lang: OCaml Description : Sail architecture definition language with OCaml Sail is a language for describing the instruction-set architecture (ISA) semantics of processors. Sail aims to provide a engineer-friendly, vendor-pseudocode-like language for describing instruction semantics. It is essentially a first-order imperative language, but with lightweight dependent typing for numeric types and bitvector lengths, which are automatically checked using Z3. Given a Sail definition, the tool will type-check it and generate documentation, executable emulators (in C and OCaml), theorem-prover definitions (for Isabelle, HOL4, and Coq), and definitions to integrate with our RMEM and isla-axiomatic tools for concurrency semantics. The Isla engine provides SMT-based symbolic evaluation for Sail models, and the Islaris verification tool integrates Isla output with the Iris program logic to support proof about binary code in Coq. Not all models are integrated with all tools - see the most recent papers and models for descriptions of the current state. ------------>>>---------- This is a denpendency of sail-riscv[0] and I will maintain it under Debian OCaml team. [0]: https://github.com/riscv/sail-riscv -- Regards, -- Bo YU
signature.asc
Description: PGP signature
