Programming with triggers
Michał Moskal · 2009
We give a case study for a Satisfiability Modulo Theories (SMT) solver usage in functional verification of a real world operating system. In particular, we present a view of the E-matching pattern annotations on quantified formulas as a kind of logic programming language, used to encode semantics of the programming language undergoing verification. We postulate a few encoding patterns to be benchmark problems for a possible E-matching alternative. We also describe features required from the SMT solver in deductive software verification scenarios.