34 lines
1.0 KiB
Markdown
34 lines
1.0 KiB
Markdown
# First Pass
|
|
**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?**
|
|
|
|
**What is the supporting evidence?**
|
|
|
|
**What are the key findings?**
|
|
|
|
# Third Pass
|
|
**Recreation Notes:**
|
|
|
|
**Hidden Findings:**
|
|
|
|
**Weak Points? Strong Points?**
|