vault backup: 2025-05-06 16:56:24

This commit is contained in:
Dane Sabo 2025-05-06 16:56:24 -04:00
parent 9d2a1fa352
commit 12cb7786e2

View File

@ -1,9 +1,22 @@
# First Pass
**Category:**
**Context:**
**Correctness:**
**Category:** This paper is an experimental paper.
**Context:** The context of this paper is using a couple different techniques
synthesize control programs using different formal methods tools.
**Correctness:** I trust Max's integrity. Some of the citations were funky and
the intro was fluffy though.
**Contributions:**
This paper shows that using LTL and other formal methods still struggles to
generate controllers for significantly challenging systems. The high bay
warehouse used to create this paper had to be simplified. Then, they introduce
an SMT solver based method to try to generate code.
**Clarity:**
The intro and conclusion do not provide very strong clarity on what they
actually did other than "high assurance is high difficulty", and that we're not
really there yet on HACPS.
# Second Pass
**What is the main thrust?**