Try Matching Logic Online
(back to the Matching Logic page)
Enter your C program annotated with matching logic specifications or choose (and modify) one example from the menu. Click Verify to run MatchC. The tool answers whether the program satisfies the specification and outputs statistics about the time, number of rewrites and number of paths analyzed. If the verification fails, additional information about the configuration is generated at the bottom of the page. When verifying C programs with MatchC, keep the following in mind:
- Matching logic builds upon an executable semantics of the language, which is used unchanged for verification ... [ more ]
- All examples below are verified for full functional correctness, not only for memory safety or other weaker properties ... [ more ]
- The C fragment supported by MatchC is an idealized fragment of the C standard ... [ more ]
- HERE are MatchC's current mathematical theories (defined in Maude) ... [ more ]
HERE are more detailed instructions and additional links.
Please press the Verify button once and wait; it may take a few seconds to run MatchC; the execution of MatchC using this web interface is limited to 2 minutes of CPU time and 500 MB of RAM.
All examples above except avl_tree/insert and avl_tree/delete should verify in less than 2 seconds. Please let us know at mailto:firstname.lastname@example.org if any of them gets stuck, telling us what browser and operating system you are using. We recommend you to install the version of MatchC available for download http://github.com/andreistefanescu/matching-logic/releases/tag/v1.1 if you have any problems using the web interface above.