Computer Aided Verification (CAV) 2012

Classical synthesis derives programs from a specification. We show an alternative approach where programs are obtained through search in a space of candidate programs. Searching for a program that meets a specification frees us from having to develop a sufficiently complete set of derivation rules, a task that is more challenging than merely describing the syntactic shape of the desired program. To make the search for a program efficient, we exploit symbolic constraint solving, lifted to synthesis from the setting of program verification.

IC3, a SAT-based safety model checking algorithm introduced in 2010, is considered among the best safety model checkers. This tutorial discusses its essential ideas: the use of concrete states, called counterexamples to induction, to motivate lemma discovery; the incremental application of induction to generate the lemmas; and the use of stepwise assumptions to allow dynamic shifting between inductive lemma generation and propagation of lemmas as predicates.

Researchers are beginning to be able to engineer synthetic genetic circuits for a range of applications in the environmental, medical, and energy domains. Crucial to the success of these efforts is the development of methods and tools to verify the correctness of these designs. This verification though is complicated by the fact that genetic circuit components are inherently noisy making their behavior asynchronous, analog, and stochastic in nature [2]. Therefore, rather than definite results, researchers are often interested in the probability of the system reaching a given state within a certain amount of time. Usually, this involves simulating the system to produce some time series data and analyzing this data to discern the state probabilities. However, as the complexity of models of genetic circuits grow, it becomes more difficult for researchers to reason about the different states by looking only at time series simulation results of the models. To address this problem, techniques from the formal verification community, such as stochastic model checking, can be leveraged [3, 4]. This tutorial will introduce the basic biology concepts needed to understand genetic circuits, as well as, the modeling and analysis techniques currently being employed. Finally, it will give insight into how formal verification techniques can be applied to genetic circuits.

In this tutorial I'll show how to prove deep functional properties of tricky sequential and concurrent C programs using VCC. I'll get into induction, termination, algebraic data types, infinite maps, and lemmas, all unified as ghost data and C-like code manipulating it. Once these are provided, verification is automatic, but the development process of such annotations tends to be very interactive, thus ``auto-active’’ verification using C as a proof language.