Also I think following are good parts: A. Symbolic execution such like https://github.com/verifast/verifast IDE, because we can watch execution sequence on the IDE. See the following Steps pane on figure 1 at page 4. https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf B. Tactic such like Coq, which is useful to prove large code.
-- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dkBh_4Sq4D6ZYxK_EtRY%2B5%3Dgt1n%3DcKA6fTGEBTvjausMg%40mail.gmail.com.
