Send the link below via email or IMCopy
Present to your audienceStart 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
Making Formal Methods into Normal Methods
Transcript of Making Formal Methods into Normal Methods
into Normal Methods
September 20, 2011
Making Formal Methods
into Normal Methods
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 “ ”
assume “ ”
from this obtain x where X: “ ” ..
from X have “ ” ..
then show “ ” ..
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.
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;
Can both loads observe the old value of 0?
The memory model defines various relations over a program's memory actions.
[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
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
Integration of Interactive and Automated Provers
[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
Process calculi: A framework for parallel programming models
Algebra: Formal analysis of concurrent programs
Operational semantics: Verification of relaxed-memory concurrency