into Normal Methods

Tjark Weber

September 20, 2011

System Overview

SMT

propositional logic

equality

uninterpreted functions

arrays

quantifiers

linear arithmetic

bit-vectors

data types

SAT

QBF

Boolean variables

negation

disjunction

conjunction

propositional logic

Boolean quantifiers

**Making Formal Methods**

into Normal Methods

into Normal Methods

Results

Complex systems almost inevitably contain bugs.

Program testing can be used to show the presence of bugs, but never to show their absence!

Edsger W. Dijkstra

A theorem prover is a computer program to prove theorems.

Lemma “ ”

Proof

assume “ ”

from this obtain x where X: “ ” ..

fix y

from X have “ ” ..

then show “ ” ..

qed

Interactive Proof

Notable ITP Projects

L4.verified: a machine-checked proof of the functional correctness of the seL4 micro-kernel

Flyspeck: a machine-checked proof of the Kepler conjecture

Software errors cost the U.S. economy $60 billion annually.

NIST, 2002

A memory model describes the interaction of threads through data in shared memory.

... with special thanks to my colleagues and co-authors: Hasan Amjad, Mark Batty, Jasmin Blanchette, Sascha Böhme, Simon Foster, Anthony Fox, Walter Guttmann, Ramana Kumar, Scott Owens, Susmit Sarkar, Peter Sewell, Thomas Sewell, Georg Struth, and many others

A new C++ standard (C++11) was approved in 2011.

It contains a memory model that defines how threads interact through shared data.

Example: Store Buffering

atomic_int x = 0;

atomic_int y = 0;

x.store(1, seq_cst);

y.load(seq_cst);

y.store(1, seq_cst);

x.load(seq_cst);

Can both loads observe the old value of 0?

The memory model defines various relations over a program's memory actions.

happens-before

reads-from

modification-order

sequentially-consistent

[POPL 2011, PPDP 2011]

Different choices for these relations give rise to different executions.

...

...

...

A mechanized semantics of C++ concurrency in an interactive theorem prover

CppMem: a tool for understanding what multi-threaded C++ programs will do

A proof of correctness for a compilation strategy to x86-TSO

Refinements to the Standard that will improve the C++ language

Mathematizing C++ Concurrency

Formal Methods

Mathematical analysis can contribute to the reliability of computer systems.

Given a precise description of a system, and a formal specification of its intended behavior, we can try to give a proof that the system meets its specification.

Complete formal verification is the only known way to guarantee that a system is free of programming errors.

Interactive theorem proving is powerful, but time-consuming - and requires expert knowledge.

Automated theorem proving is easy to use, but (so far) quite limited in power.

Norton Cybercrime Report, 2012

Testing?

**Tjark Weber**

**Integration of Interactive and Automated Provers**

[JAL 2009]

[ITP 2010, ITP 2011]

[ITP 2010, CPP 2011]

Proof validation is feasible for SAT, QBF and SMT. It scales to large formulas and proofs with millions of inferences.

Naive solutions are slow - efficient implementations based on sophisticated optimizations are crucial.

Our integrations provide a high degree of automation in interactive theorem provers, thereby enabling new applications.

Parosh Abdulla: Software verification and model checking

Bengt Jonsson: Formal methods for concurrent systems

Joachim Parrow: Theories and models for mobile processes

Kostis Sagonas: Concurrent functional programming

Future Directions

Process calculi: A framework for parallel programming models

Algebra: Formal analysis of concurrent programs

Operational semantics: Verification of relaxed-memory concurrency