I am happy to announce that our recent efforts to extend the RAPID verification framework have been peer-reviewed and accepted for publication at two topnotch venues for software verification and theoretical computer science. Our work on lemmaless induction has been accepted at the Conference on Intelligent Computer Mathematics 2022 taking place in Tbilisi, Georgia in September (CICM’22). Further we submitted a tool paper on the RAPID framework containing details about the workings and usage of the Rapid tool, aggregating information about all our verification modes, to the Conference in Formal Methods in Computer-Aided Design (FMCAD'22) that has been accepted by peers for publication and will be presented in October 2022 in Trento, Italy. 

Find the exact titles and abstracts below: 

A. Bhayat, P. Georgiou, C. Eisenhofer, L. Kovács, and G. Reger, “Lemmaless Induction in Trace Logic”.

Abstract: We present a novel approach to automate the verification of first-order inductive program properties capturing the partial correctness of imperative pro- gram loops with branching, integers and arrays. We rely on trace logic, an in- stance of first-order logic with theories, to express first-order program semantics by quantifying over program execution timepoints. Program verification in trace logic is translated into a first-order theorem proving problem where, to date, effective reasoning has required the introduction of so-called trace lemmas to establish inductive properties. In this work, we extend trace logic with generic induction schemata over timepoints and loop counters, reducing reliance on trace lemmas. Inferring and proving loop invariants becomes an inductive inference step within superposition-based first-order theorem proving. We implemented our approach in the RAPID framework, using the first-order theorem prover VAMPIRE. Our ex- tensive experimental analysis show that automating inductive verification in trace logic improves over existing approaches. 

P. Georgiou, B. Gleiss, L. Kovács, A. Bhayat, M. Rawson and G. Reger, “The RAPID Software Verification Framework”.

Abstract: We present the RAPID framework for automatic software verification by applying first-order reasoning in trace logic. RAPID establishes partial correctness of programs with loops and arrays by inferring invariants necessary to prove program correctness using a saturation-based automated theorem prover. RAPID can heuristically generate trace lemmas, common program properties that guide inductive invariant reasoning. Alternatively, RAPID can exploit nascent support for induction in modern provers to fully automate inductive reasoning without the use of trace lemmas. In addition, RAPID can be used as an invariant generation engine, supplying other verification tools with quantified loop invariants necessary for proving partial program correctness.