Debugging, on average, has grown to consume more than 60% of today's ASIC and SoC verification effort. Clearly, this is a topic the industry must address, and some organizations have done just that. Those that have adopted an assertion-based verification (ABV) methodology have seen significant reduction in simulation debugging time (as much as 50%) due to improved observability. Furthermore, organizations that have embraced an ABV methodology are able to take advantage of more advanced verification techniques, such as formal verification, thus improving their overall verification quality and results. Nonetheless, even with multiple published industry case studies from various early adopters - each touting the benefits of applying ABV - the industry as a whole has resisted adopting assertion-based techniques. This tutorial provides an industry survey of today's ABV landscape, ranging from myths to realities.

The theorem proving approach to verification involves modelling a system in a rich formalism such as higher-order logic or set theory, then performing a human-driven interactive correctness proof using a proof assistent. In a striking contrast, techniques like model checking, by limiting the user to a less expressive formalism (propositional logic, CTL etc.), can offer completely automated decision methods, making them substantially easier to use and often more productive.

With this in mind, why should one be interested in the theorem proving approach? In this tutorial I will explain some of the advantages of theorem proving, showing situations where the generality of theorem proving is beneficial, allowing us to tackle domains that are beyond the scope of automated methods or providing other important advantages. I will talk about the state of the art in theorem proving systems and give a little demonstration to give an impression of what it's like to work with such a system.

Separation logic is an extension of Hoare's logic for reasoning about programs that manipulate pointers. Its assertion language extends classical logic with a separating conjunction operator A*B, which asserts that A and B hold for separate portions of memory. In this tutorial I will first cover the basics of the logic, concentrating on highlights from the early work.
(i) The separating conjunction fits together with inductive definitions in a way that supports natural descriptions of mutable data structures.
(ii) Axiomatizations of pointer operations support in-place reasoning , where a portion of a formula is updated in place when passing from precondition to postcondition, mirroring the operational locality of heap update.
(iii) Notorious "dirty" features of low-level programming (pointer arithmetic, explicit deallocation) are dealt with smoothly, even embraced.
(iv) Frame axioms, which state what does not change, can be avoided when writing specifications.

These points together enable specifications and proofs of pointer programs that are dramatically simpler than was possible previously, in many cases approaching the simplicity associated with proofs of pure functional programs. I will describe how that is, and where rough edges lie (programs whose proofs are still more complex than we would like).

In describing these highlights I will outline how many of the points flow from Separation Logic's model theory, particularly an interaction between properties concerning the local way that imperative programs operate, and the abstract properties of its models, which it inherits from bunched logic (a species of substructural logic related to linear and relevant logics, and Lambek's syntactic calculus). Using the model theoretic perspective, I will attempt to describe the extent to which Separation Logic's "benefits" do and do not depend on its language of assertions.

After the basic part, I will then discuss how these points (i)-(iv) feed into research on mechanized verification, both for interactive proof in proof assistants and for automatic proof and abstract interpretation. Time permitting, I will close with more recent highlights, on concurrency, data abstraction, and object-oriented programming.

Abstract interpretation is one of the main verification technologies besides model checking and deductive verification.
Abstract interpretation has a rich theory of abstraction and strong support for the construction of abstract domains. It allows to express a precise relation to the (concrete) semantics of the programming language inducing a clear relation between the results of an abstract interpretation and the properties of the analyzed program. It permits trading efficiency against precision and offers means to enforce termination where this is not guaranteed.
We explain abstract interpretation using examples from a particular application domain: the determination of bounds on the execution times of programs. These bounds are used to show reliably that hard real-time systems satisfy their timing constraints.
The application domain requires a number of static analyses and domains with different characteristics. Most domains exhibit Galois connections, a few do not. Some analyses require widening to leap infinite ascending chains and ensure termination.