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 961 to 980 of 1018.
Sorted by year (citations)

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

  1. Klein, Gerwin; Wildmoser, Martin: Verified bytecode subroutines (2003) ioport
  2. Klein, G.; Wildmoser, M.: Verified bytecode subroutines (2003)
  3. Mehta, Farhad; Nipkow, Tobias: Proving pointer programs in higher-order logic. (2003)
  4. Momigliano, Alberto; Ambler, Simon J.: Multi-level meta-reasoning with higher-order abstract syntax (2003)
  5. Nieto, Leonor Prensa: The rely-guarantee method in Isabelle/HOL (2003)
  6. Okuma, Koji; Minamide, Yasuhiko: Executing verified compiler specification. (2003) ioport
  7. Pilegaard, Henrik; Hansen, Michael R.; Sharp, Robin: An approach to analyzing availability properties of security protocols (2003)
  8. Röckl, Christine; Hirschkoff, Daniel: A fully adequate shallow embedding of the (\pi)-calculus in Isabelle/HOL with mechanized syntax analysis (2003)
  9. Vestergaard, René; Brotherston, James: A formalised first-order confluence proof for the (\lambda)-calculus using one-sorted variable names. (2003)
  10. Basin, David; Friedrich, Stefan; Gawkowski, Marek: Verified bytecode model checkers (2002)
  11. Bauer, Gertrud; Nipkow, Tobias: The 5 colour theorem in Isabelle/Isar (2002)
  12. Bella, Giampaolo; Paulson, Lawrence C.: A proof of non-repudiation (2002)
  13. Berghofer, Stefan; Nipkow, Tobias: Executing higher order logic (2002)
  14. Brucker, Achim D.; Wolff, Burkhart: A proposal for a formal OCL semantics in Isabelle/HOL (2002)
  15. Dawson, Jeremy E.; Goré, Rajeev: Formalised cut admissibility for display logic (2002)
  16. Nipkow, Tobias: Hoare logics for recursive procedures and unbounded nondeterminism (2002)
  17. Nipkow, Tobias: Hoare logics in Isabelle/HOL (2002)
  18. Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus: Isabelle/HOL. A proof assistant for higher-order logic (2002)
  19. Smith, Graeme; Kammüller, Florian; Santen, Thomas: Encoding object-Z in Isabelle/HOL (2002)
  20. von Oheimb, David; Nipkow, Tobias: Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited (2002)

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