<p>I am reading on Automata, Model Checking and CTL/LTL. I am looking for examples/references/books that help me understand the following:</p>
<ol>
<li>Given a program (for example Python or Java), how can I change various parts to automata / logical languages, to perform formal analysis / model checking?</li>
<li>Given an automata and a logical specification (which has been verified to be correct) how can I construct a program (for example Python or Java) that will also be correct?</li>
</ol>
<p>Thanks in advance.</p>

CC BY-SA 4.0
2022-05-10T14:16:41.570Z
Are you asking for software that will help you do this, or for the theory of how one would carry this out?
cody
CC BY-SA 4.0
2022-06-03T08:21:07.543Z
@cody Pehaps first theory, and secondly, a software would be interesting too. But theory is what I am really looking for.
Karl 17302
<reference-request><model-checking><formal-methods><program-verification><temporal-logic>
From formal models to programs - Model Checking
Karl 17302
# From formal models to programs - Model Checking

(Asked by: username_0 on 2022-05-05)

I am reading on Automata, Model Checking and CTL/LTL. I am looking for examples/references/books that help me understand the following:

1. Given a program (for example Python or Java), how can I change various parts to automata / logical languages, to perform formal analysis / model checking?
2. Given an automata and a logical specification (which has been verified to be correct) how can I construct a program (for example Python or Java) that will also be correct?

Thanks in advance.

**Tags:** reference-request, model-checking, formal-methods, program-verification, temporal-logic
> **Comments:**
> **username_1**: Are you asking for software that will help you do this, or for the theory of how one would carry this out?  
> **username_0**: @cody Pehaps first theory, and secondly, a software would be interesting too. But theory is what I am really looking for.  

---

## 0 answers

