Loading presentation...

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Make your likes visible on Facebook?

Connect your Facebook account to Prezi and let your likes appear on your timeline.
You can change this under Settings & Account at any time.

No, thanks

Making Formal Methods into Normal Methods

Uppsala University; September 20, 2012
by

Tjark Weber

on 5 October 2013

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Making Formal Methods into Normal Methods

Making Formal Methods
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

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
Full transcript