From b5ce6769b8a8659c22fa8a0ca30f11c60555c5ee Mon Sep 17 00:00:00 2001 From: KirisameVanilla <118162831+KirisameVanilla@users.noreply.github.com> Date: Mon, 29 Sep 2025 15:32:48 +0800 Subject: [PATCH] =?UTF-8?q?feat:=20=E8=BD=AF=E4=BB=B6=E5=88=86=E6=9E=90?= =?UTF-8?q?=E4=B8=8E=E9=AA=8C=E8=AF=81=E5=89=8D=E6=B2=BF?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../软件工程学院/软件分析与验证前沿/README.md | 10 +++++++ .../软件分析与验证前沿/labs/README.md | 9 +++++++ .../labs/苏亭/2025-2026学年上学期/lab1.md | 26 +++++++++++++++++++ 3 files changed, 45 insertions(+) create mode 100644 docs/undergraduate/软件工程学院/软件分析与验证前沿/README.md create mode 100644 docs/undergraduate/软件工程学院/软件分析与验证前沿/labs/README.md create mode 100644 docs/undergraduate/软件工程学院/软件分析与验证前沿/labs/苏亭/2025-2026学年上学期/lab1.md diff --git a/docs/undergraduate/软件工程学院/软件分析与验证前沿/README.md b/docs/undergraduate/软件工程学院/软件分析与验证前沿/README.md new file mode 100644 index 0000000..fe1f5fa --- /dev/null +++ b/docs/undergraduate/软件工程学院/软件分析与验证前沿/README.md @@ -0,0 +1,10 @@ +--- +title: 软件分析与验证前沿 +--- + +## 2025-2026学年上学期 + +### 苏亭 + +- 很好的一门课, 只不过平时需要做的事比较多, 只想混学分不建议来 +- [实验作业](labs/) diff --git a/docs/undergraduate/软件工程学院/软件分析与验证前沿/labs/README.md b/docs/undergraduate/软件工程学院/软件分析与验证前沿/labs/README.md new file mode 100644 index 0000000..02d81c4 --- /dev/null +++ b/docs/undergraduate/软件工程学院/软件分析与验证前沿/labs/README.md @@ -0,0 +1,9 @@ +--- +title: 实验 +--- + +## 2025-2026学年上学期 + +### 苏亭 + +- [lab1](苏亭/2025-2026学年上学期/lab1) diff --git a/docs/undergraduate/软件工程学院/软件分析与验证前沿/labs/苏亭/2025-2026学年上学期/lab1.md b/docs/undergraduate/软件工程学院/软件分析与验证前沿/labs/苏亭/2025-2026学年上学期/lab1.md new file mode 100644 index 0000000..bdd2db8 --- /dev/null +++ b/docs/undergraduate/软件工程学院/软件分析与验证前沿/labs/苏亭/2025-2026学年上学期/lab1.md @@ -0,0 +1,26 @@ +--- +title: lab1 +--- + +:::info +本次实验作为第一次实验, 只需要跟着实验手册一步步做就行. +由于实验结果可能有个体差异性, 所以在此不提供个人作业 +::: + +1. 运行 `make all` +2. 打开 `answers.txt` 和 `c_programs` 里面的十份源码 +3. 挨个阅读源码, 脑测一下是否会出现 `division by zero` 错误, 如果会的话, 就在 `ground truth` 列填 `right`; 反之填写 `wrong` +4. 这个时候你的 `make all` 应该运行完了, 没有的话等它运行完 +5. 打开 `results`, 里面有 `afl_logs` 和 `csa_logs` + 1. 对于 `afl_logs`, 我们查看 `afl_logs/test{n}/afl_output/crashes` 中是否有文件, 如果有, 说明对于 `test{n}`, afl 检测到了 `division by zero` 错误, 那么我们在对应的 `AFL` 列填写 `reject`; 反之, 填写 `accept` + 2. 对于 `csa_logs`, 我们挨个查看 `test{n}_out.txt`, 并在每个之中查找字符串 `Division by zero`, 如果查找到了, 说明对于 `test{n}`, csa 检测到了 `division by zero` 错误, 那么我们在对应的 `CSA` 列填写 `reject`; 反之, 填写 `accept` +6. 根据刚刚填写的内容计算 `AFL` 和 `CSA` 列的 `Precision`, `Recall` 和 `F1 score` + 1. Precision: 准确率, 即不误报, 即对于所有检测结果为 `Reject` 的行里 `Ground Truth` 为 `wrong` 的比例 + 2. Recall: 召回率, 即不漏报, 即对于所有 `Ground Truth` 为 `wrong` 的行, 检测结果为 `Reject` 的比例 + 3. F1 score: 计算公式: + $$ + F1 = \frac{2 \cdot \text{Precision} \cdot \text{Recall}}{\text{Precision} + \text{Recall}} + $$ +7. 回答下方的问题 + 1. 第 1, 2 题中的 sound 对应 Precision, complete 对应 Recall, 根据自己的运行结果回答即可 + 2. 讨论 `CSA` 的 `accuracy` 和 `cost` 的时候要关注它的性质——静态分析工具