Software verification comes in two flavors: static and dynamic. Static program verification takes place during program analysis and/or compilation, and it aims to prove the correctness of the program w.r.t. some criteria. Dynamic one takes place at run time and it’s purpose is to detect undesirable program behaviors.

Nowadays these two tasks are typically addresses by systems that offer programmers a combination of language-level constructs (procedure-level annotations such as assertions/contracts, gradual types, etc.) and associated tools (such as static code analyzers and run-time verification frameworks). However, it is often the case that these constructs and tools are not used to their full extent in practice due to a number of limitations such as excessive run-time overhead and/or limited expressiveness. This issue is especially prominent in the context of dynamic languages without an underlying strong type system, such as Prolog.

In this talk several practical solutions for minimizing the run-time overhead associated with assertion-based verification while keeping the correctness guarantees provided by run-time checks will be discussed. Additionally, a proposal of extending the expressiveness of first-order specifications to higher-order software specifications will be described. The solutions will be presented in the context of the Ciao system (developed here at IMDEA Software), where a combination of an abstract interpretation-based static analyzer and run-time verification framework is available, although our proposals can be straightforwardly adapted to any other similar system.