Isabelle

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.

This software is also referenced in ORMS.


References in zbMATH (referenced in 576 articles , 1 standard article )

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

1 2 3 ... 27 28 29 next

  1. Chan, Hing-Lun; Norrish, Michael: Classification of finite fields with applications (2019)
  2. de Gouw, Stijn; de Boer, Frank S.; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic: Verifying OpenJDK’s sort method for generic collections (2019)
  3. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  4. Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
  5. Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
  6. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
  7. Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
  8. Libal, Tomer; Volpe, Marco: A general proof certification framework for modal logic (2019)
  9. Li, Li-Ming; Shi, Zhi-Ping; Guan, Yong; Zhang, Qian-Ying; Li, Yong-Dong: Formalization of geometric algebra in HOL Light (2019)
  10. Lin, Yuhui; Bundy, Alan; Grov, Gudmund; Maclean, Ewen: Automating Event-B invariant proofs by rippling and proof patching (2019)
  11. Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)
  12. Miller, Dale: Mechanized metatheory Revisited (2019)
  13. Narboux, Julien; Janičić, Predrag; Fleuriot, Jacques: Computer-assisted theorem proving in synthetic geometry (2019)
  14. Rabe, Florian: MMTTeX: connecting content and narration-oriented document formats (2019)
  15. Rabe, Florian; Sharoda, Yasmine: Diagram combinators in MMT (2019)
  16. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
  17. Aiguier, Marc; Atif, Jamal; Bloch, Isabelle; Hudelot, Céline: Belief revision, minimal change and relaxation: A general framework based on satisfaction systems, and applications to description logics (2018)
  18. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  19. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
  20. Benzaken, V.; Contejean, É.; Keller, Ch.; Martins, E.: A Coq formalisation of SQL’s execution engines (2018)

1 2 3 ... 27 28 29 next