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 837 articles , 2 standard articles )

Showing results 1 to 20 of 837.
Sorted by year (citations)

1 2 3 ... 40 41 42 next

  1. Abdulaziz, Mohammad; Paulson, Lawrence C.: An Isabelle/HOL formalisation of Green’s theorem (2019)
  2. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2019)
  3. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)
  4. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  5. Gouëzel, Sébastien; Shchur, Vladimir: A corrected quantitative version of the Morse lemma (2019)
  6. Hayes, Ian J.; Meinicke, Larissa A.; Winter, Kirsten; Colvin, Robert J.: A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency (2019)
  7. Hirokawa, Nao; Middeldorp, Aart; Sternagel, Christian; Winkler, Sarah: Abstract completion, formalized (2019)
  8. Immler, Fabian; Traut, Christoph: The flow of ODEs: formalization of variational equation and Poincaré map (2019)
  9. Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
  10. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
  11. Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
  12. Lammich, Peter: Refinement to imperative HOL (2019)
  13. Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
  14. Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
  15. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  16. Marić, Filip: Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (2019)
  17. Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)
  18. Nikolić, Mladen; Marinković, Vesna; Kovács, Zoltán; Janičić, Predrag: Portfolio theorem proving and prover runtime prediction for geometry (2019)
  19. Nipkow, Tobias; Brinkop, Hauke: Amortized complexity verified (2019)
  20. Schmidt-Schauß, Manfred; Sabel, David; Kutz, Yunus D. K.: Nominal unification with atom-variables (2019)

1 2 3 ... 40 41 42 next