More MatchC Online Instructions
From Matching Logic
(back to MatchC Online)
You can download MatchC from here. When verifying C programs with MatchC, keep in mind the following:
- Matching logic builds upon an executable (or operational) rewrite semantics of the language, which is used unchanged for verification. An alternative, axiomatic (or of any other nature) semantics is not needed for the sole purpose of program verification. In matching logic, all program specifications are rewrite rules between program configurations (as opposed to Hoare triples), which thus replace the more conventional pre- and post-conditions. Loop invariants are syntactic sugar also for rewrite rules. In configurations, semantic data is organized in cells, which are written using the XML notation. The <k>...</k> cell holds the code, <heap>...</heap> holds the heap, etc. Rewrite rules use the K contextual notation, i.e., rewrites are distributed over the common configuration structure to the places where changes actually take place. $ stands for the function body. As usual in rewriting, if something is not mentioned in a rule it means that rule does not touch it. We call structural frame for a rule all the configuration parts that the rule does not touch. More explanations will be given in the examples on the MatchC Online interface. See the papers on the Matching Logic page for foundational and notational details. HERE you can see the complete K semantics of the C fragment considered in MatchC, called KernelC, as well as the K semantics of its extensions with specifications.
- All examples on the MatchC Online interface are verified for full functional correctness, not only for memory safety or other weaker properties. The latter can and have also been verified using matching logic, but they are much simpler and we do not demostrate them here. For examples showing how to use matching logic for checking memory safety, see our first MatchC prototype. MatchC currently only considers partial (as oppossed to total) correctness, that is, it does not prove that the programs also terminate. See, again, the papers on the Matching Logic page.
- The C fragment supported by MatchC is an idealized fragment of the C standard. In particular it works with arbitrarily large integer numbers, each pointer is precisely one location, and all language constructs are deterministic. Thus, there could be C programs which are undefined according to the C standard but MatchC cannot detect it. All examples below lay in the semantic intersection of the actual C and MatchC's C.
- Matching logic uses patterns to structurally match mathematical objects, e.g., sequences, trees, graphs, etc., in the configuration. Consequently, matching reduces reasoning about programs to reasoning about mathematical objects. The latter, however, requires mathematical theories for the involved domains. Currently, MatchC includes several mathematical domains defined equationally using Maude, which can be found HERE. Some theories are very broad in scope, like multisets, while others are very specialized, like schorr-waite.
See the MatchC readme file for additional details.