Semantics-based Program Verifiers for All Languages

  • Grigore Rosu | UIUC
  • ECC 2010

I will present our K-based language-independent verification framework that can be instantiated with an operational semantics to automatically generate a program verifier. The framework treats both the operational semantics and the program correctness specifications as reachability rules between matching logic patterns, and uses the sound, relatively complete, and language-independent reachability logic proof system to prove the program specifications using the language semantics given as axioms. We instantiated the framework with the semantics of several real-world languages like C, Java, and JavaScript, and succeeded in verifying a series of challenging heap-manipulating programs in all these languages, automatically. This is the first approach that can turn the operational semantics of real-world languages into correct-by-construction automatic verifiers.

Watch Next