rsm4hm 源码

基于模板的超级市场排名更高时刻的综合器 这是我们的TACAS论文“”方法的实现。 我们的工具计算给定随机程序的运行时E [T ^ k]的第k个矩的上限,其中k是自然数,T是代表程序运行时的随机变量。 我们的工具通过从离散/连续分布中采样以及恶魔般的不确定性(延长运行时间)来支持随机程序。 建立 我们的工具是用OCaml编写的。 对于线性模板,您需要 ;对于多项式模板,您需要 。 我们在以下环境上进行了测试,但我们的工具也可以在其他平台上使用。 作业系统:Ubuntu 18.04.1 OCaml版本4.09.0 menhir版本20190924 MATLAB R2018b SOSTOOLS 3.03 SDPT3 4.0 对于Ubuntu 安装所需的软件包(ocaml,menhir)。 $ sudo apt install ocaml menhir 编译。 $ cd l