Summary
Lightweight formal methods offer a way to increase the use of rigorous techniques for finding more bugs during everyday software development. Runtime verification (RV) is such a method; it monitors program executions against behavioral safety properties that are specified in logic. In many open-source projects, RV has helped find hundreds of confirmed bugs that were missed during software testing; but RV is often too slow. While several optimizations have been proposed for speeding up RV, no extant framework implements all of them. The project’s novelties are a framework for implementing RV op
