| Stable release | Isabelle 2009-1 |
|---|---|
| Written in | Standard ML |
| Operating system | Linux, Solaris, Mac OS X, Windows (Cygwin) |
| Type | Mathematics |
| License | BSD license |
| Website | http://isabelle.in.tum.de/ |
The Isabelle theorem prover is an interactive theorem proving framework, a successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or ZFC. Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification. Though interactive, Isabelle also features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, as well as various decision procedures. Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem, correctness of security protocols, and properties of programming language semantics. The Isabelle theorem prover is free software, released under the revised BSD license.
Contents |
Example proof
Isabelle's proof language Isar aims to support proofs that are both human-readable and machine-checkable. For example, the proof that the square root of two is not rational can be written as follows.
theorem sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" proof assume "sqrt (real 2) ∈ ℚ" then obtain m n :: nat where n: "n ≠ 0" and sqrt_rat: "¦sqrt (real 2)¦ = real m / real n" and gcd: "gcd m n = 1" .. from n and sqrt_rat have "real m = ¦sqrt (real 2)¦ * real n" by simp then have "real (m²) = (sqrt (real 2))² * real (n²)" by (auto simp add: power2_eq_square) also have "(sqrt (real 2))² = real 2" by simp also have "... * real (n²) = real (2 * n²)" by simp finally have eq: "m² = 2 * n²" .. hence "2 dvd m²" .. with two_is_prime have dvd_m: "2 dvd m" by (rule prime_dvd_power_two) then obtain k where "m = 2 * k" .. with eq have "2 * n² = 2² * k²" by (auto simp add: power2_eq_square mult_ac) hence "n² = 2 * k²" by simp hence "2 dvd n²" .. with two_is_prime have "2 dvd n" by (rule prime_dvd_power_two) with dvd_m have "2 dvd gcd m n" by (rule gcd_greatest) with gcd have "2 dvd 1" by simp thus False by arith qed
Usage
Among other places, Isabelle has been applied by Hewlett-Packard in the design of the HP 9000 line of server's Runway bus where it discovered a number of bugs uncaught by previous testing and simulation[1].
More recently, Isabelle has also been used successfully in software implementation verification. In 2009, the L4.verified project at NICTA produced the first formal proof of functional correctness of a general-purpose operating system kernel [2]: the seL4 (secure embedded L4) microkernel. The proof is constructed and checked in Isabelle/HOL and comprises over 200,000 lines of proof script. The verification covers code, design, and implementation and the main theorem states that the C code correctly implements the formal specification of the kernel. The proof uncovered 160 bugs in the C code of the seL4 kernel, and about 150 issues in each of design and specification.
Larry Paulson keeps a list of research projects using Isabelle.
See also
Notes
- ^ Philip Wadler's "An Angry Half-Dozen" (1998) attributes this result to: Albert J. Camilleri. "A hybrid approach to verifying liveness in a symmetric multiprocessor". 10th International Conference on Theorem Proving in Higher-Order Logics, Elsa Gunter and Amy Felty, editors, Murray Hill, New Jersey, August 1997. Lecture Notes in Computer Science (LNCS) Vol. 1275, Springer Verlag, 1997
- ^ Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel". 22nd ACM Symposium on Operating System Principles. Big Sky, MT, USA. pp. 207-200. http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf.
References
- Lawrence C. Paulson: The foundation of a generic theorem prover. Journal of Automated Reasoning, Volume 5 , Issue 3 (September 1989), Pages: 363-397, ISSN 0168-7433
- Lawrence C. Paulson: The Isabelle Reference Manual
- M. A. Ozols, K. A. Eastaughffe, and A. Cant. "DOVE: Design Oriented Verification and Evaluation". Proceedings of AMAST 97, M. Johnson, editor, Sydney, Australia. Lecture Notes in Computer Science (LNCS) Vol. 1349, Springer Verlag, 1997.
- Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL - A Proof Assistant for Higher-Order Logic
External links
This entry is from Wikipedia, the leading user-contributed encyclopedia. It may not have been reviewed by professional editors (see full disclaimer)
