Isabelle/HOL

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.


References in zbMATH (referenced in 1018 articles , 2 standard articles )

Showing results 941 to 960 of 1018.
Sorted by year (citations)

previous 1 2 3 ... 46 47 48 49 50 51 next

  1. Lindegaard, Morten P.; Haxthausen, Anne E.: Proof support for RAISE by a reuse approach based on institutions (2004)
  2. Longley, John; Pollack, Randy: Reasoning about CBV functional programs in Isabelle/HOL (2004)
  3. Lyaletski, Alexander; Paskevich, Andrey; Verchinine, Konstantin: Theorem proving and proof verification in the system SAD (2004)
  4. Momigliano, Alberto; Tiu, Alwen: Induction and co-induction in sequent calculus (2004)
  5. O’Keefe, Greg: Towards a readable formalisation of category theory (2004)
  6. Paulson, Lawrence C.: Organizing numerical theories using axiomatic type classes (2004)
  7. Rukšėnas, Rimvydas: A rigorous environment for development of concurrent systems (2004)
  8. Schirmer, Norbert: Analysing the java package/access concepts in Isabelle/HOL (2004) ioport
  9. Siekmann, Jörg; Benzmüller, Christoph: (\Omega)MEGA: Computer supported mathematics (2004)
  10. Wang, Farn: Inductive composition of numbers with maximum, minimum, and addition (2004)
  11. Weber, Tjark: Towards mechanized program verification with separation logic (2004)
  12. Wildmoser, Martin; Nipkow, Tobias: Certifying machine code safety: Shallow versus deep embedding (2004)
  13. Wildmoser, Martin; Nipkow, Tobias; Klein, Gerwin; Nanz, Sebastian: Prototyping proof carrying code (2004)
  14. Basin, David; Friedrich, Stefan; Gawkowski, Marek: Bytecode verification by model checking (2003)
  15. Berghofer, Stefan: Program extraction in simply-typed higher order logic (2003)
  16. Beringer, Lennart; MacKenzie, Kenneth; Stark, Ian: Grail: a functional form for imperative mobile code (2003)
  17. Brucker, Achim D.; Wolff, Burkhart: Using theory morphisms for implementing formal methods tools (2003)
  18. Brucker, A. D.; Rittinger, F.; Wolff, B.: Hol-z 2.0: a proof environment for z-specifications (2003) ioport
  19. Dawson, Jeremy E.; Goré, Rajeev: A new machine-checked proof of strong normalisation for display logic (2003)
  20. Klein, Gerwin; Nipkow, Tobias: Verified bytecode verifiers. (2003)

previous 1 2 3 ... 46 47 48 49 50 51 next