Welcome

RV-Match is a program analysis environment based on the K semantic framework. The formal semantics of a target programming language is given as input, and RV-Match provides a series of formal analysis tools specialized for that language, such as a symbolic execution engine, a semantic debugger, a systematic checker for undesired behaviors (model-checker), and even a fully fledged deductive program verifier. RV-Match is currently instantiated and optimized to work with the publicly available C11 semantics that rigorously formalizes the current ISO C11 Standard, in the form of a tool called kcc, an ISO C11-compliant compiler for C. The novel technology underlying the kcc tool and the C11 semantics are best explained in the following papers:

Dwight Guth, Chris Hathhorn, Manasvi Saxena, and Grigore Rosu. 2016. RV-Match: Practical Semantics-Based Program Analysis. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV ‘16). LNCS Volume 9779, 2016, pp 447-453. (Also available at FSL@UIUC)

Chris Hathhorn, Chucky Ellison, and Grigore Rosu. 2015. Defining the Undefinedness of C. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ‘15). ACM, New York, NY, USA, 336-345. (Also available at FSL@UIUC)

Chucky Ellison and Grigore Rosu. 2012. An Executable Formal Semantics of C with Applications. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ‘12). ACM New York, NY, USA, 533-544. (Also available at FSL@UIUC)

Unlike modern optimizing compilers, whose goal is to make binaries that are as small and as fast as possible at the expense of compiling programs that may be semantically incorrect, kcc instead aims at mathematically rigorous dynamic checking of program compliance with the ISO C11 Standard. The ISO C11 Standard includes a number of categories of behavior that are subject to change on the whim of the compiler developer. A program compiled and executed using kcc will catch many of these errors, in the same style as Valgrind or UBSan, ASan, etc., but can also catch a number of other even more subtle errors that result in undefined, unspecified, or implementation-defined behavior.

This is critical because many of these behaviors are not only unintended, but also subject to change if you switch to a new target platform, compiler, or compiler version or optimization. A program that seems to run perfectly in one environment can crash or behave incorrectly in another environment.