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


Your Answer

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

Browse other questions tagged or ask your own question.