State-of-the-art deductive verification tools for programs containing inductive data structures and loops largely depend on satisfiability modulo theories (SMT) solvers to discharge verification conditions and establish software correctness. These approaches are mostly restricted to inferring and proving universally quantified properties in fragments of first-order theories of various potentially unbounded data structures, such as arrays, lists and integers. 

In contrast, the RAPID verification framework supports reasoning with arbitrary quantifiers in full first-order logic with theories. Program semantics and properties are directly encoded in trace logic - an instance of full first-order logic with equality - by simulating program execution over multiple states at once. This is powered by allowing quantification over multiple timepoints of program execution and expressing program behavior over such timepoints. Specifically, this differentiates program semantics from traditional state-driven program semantics where different variable states throughout program execution are represented by fresh variables. This allows simultaneous reasoning about sets of program states, unlike most verification approaches based on model-checking. 

To make things more precise: unlike model-checking based approaches, a loop iteration in RAPID is based upon multiple program locations rather than a single state, which in turn enables RAPID to express arbitrarily quantified loop properties at various program locations and iterations. This gain in logical expressiveness is, for example, beneficial for reasoning about programs with unbounded arrays or proving security and privacy properties.

Given a program loop annotated with pre/post-conditions, RAPID proves partial program correctness of such input problems by automatically translating input problems to such program semantics in trace logic and, most importantly, automatically adding necessary instances of so-called trace lemmas. These are apriori-identified inductive properties that are integrated in the RAPID framework and automatically instantiated for all relevant program variables and program locations. Why do we need such lemmas? Given that our input programs contain loops, we need inductive reasoning to be able to derive a property from axioms. It is well-known that automating such induction is one of the biggest problems in automated software verification since finding and proving induction schemes automatically is not always possible. 

However, we identified three schemes for lemmas that represent common inductive properties that allow to abstract such inductive schemes for the underlying prover. This allows for the underlying first-order theorem prover to use inductive proof steps during proof search and thus deriving the safety property from the program semantics and trace lemmas, hence certifying that the program indeed satisfies the safety property. RAPID uses the automated theorem prover VAMPIRE to produce such proofs. Our experimental evaluations give practical evidence of the efficacy of RAPID and can be found in our 2020 paper at https://publik.tuwien.ac.at/files/publik_293904.pdf.