Let n the number of variables, and m the depth of the formulas of the experiments. (don't forget edit the location path in the file Core.hs). This verifier extends naturally to the CTL* temporal logic (and thus, to the CTL logic). In summary, this repository contains a model verifier for LTL temporal logic, which, does not use Büchi'sĪutomatons or Strongly Connected Components, is only based on formal semantics. See Efficient On-the-Fly Model Checking for CTL* for more details. This work simplifies and improves Girish Bhat, Rance Cleaveland and Orna Grumberg work. This repository contains my work for obtain my computer scientist master degree: a simple model checker Haskell is faster than C++, more concise than Perl, more regular than Python, more flexible than Ruby, more typeful than C#, more robust than Java, and has absolutely nothing in common with PHP. To me, mathematics, computer science, and the arts are insanely related. While simulation and testing explore some of the possible behaviors and scenarios of the system, leaving open the question of whether the unexplored trajectories may contain the fatal bug, formal verification conducts an exhaustive exploration of all possible behaviors. Simple and Efficient On-the-Fly Model Checking for LTL, CTL and CTL*
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |