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.

  • $\begingroup$ Are you asking for software that will help you do this, or for the theory of how one would carry this out? $\endgroup$
    – cody
    May 10 at 14:16
  • $\begingroup$ @cody Pehaps first theory, and secondly, a software would be interesting too. But theory is what I am really looking for. $\endgroup$
    – user17302
    Jun 3 at 8:21


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy