I am reading on Automata, Model Checking and CTL/LTL. I am looking for examples/references/books that help me understand the following:
- Given a program (for example Python or Java), how can I change various parts to automata / logical languages, to perform formal analysis / model checking?
- 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.