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 667 articles , 1 standard article )

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

1 2 3 ... 32 33 34 next

  1. Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
  2. Chan, Hing Lun; Norrish, Michael: Mechanisation of the AKS algorithm (2021)
  3. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
  4. Fervari, Raul; Trucco, Francisco; Ziliani, Beta: Verification of dynamic bisimulation theorems in Coq (2021)
  5. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
  6. Koutsoukou-Argyraki, Angeliki: Formalising mathematics -- in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started (2021)
  7. Maletzky, Alexander: A generic and executable formalization of signature-based Gröbner basis algorithms (2021)
  8. Xie, Wanling; Zhu, Huibiao; Xu, Qiwen: A process calculus BigrTiMo of mobile systems and its formal semantics (2021)
  9. Ballarin, Clemens: Exploring the structure of an algebra text with locales (2020)
  10. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  11. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  12. Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)
  13. Cui, Xiangyu; Li, Xun; Yang, Lanzhi: Better than optimal mean-variance portfolio policy in multi-period asset-liability management problem (2020)
  14. Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias: Verified analysis of random binary tree structures (2020)
  15. Echenim, Mnacho; Guiol, Hervé; Peltier, Nicolas: Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (2020)
  16. Elderhalli, Yassmeen; Hasan, Osman; Tahar, Sofiène: A framework for formal dynamic dependability analysis using HOL theorem proving (2020)
  17. Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
  18. Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of algebraic numbers in Isabelle/HOL (2020)
  19. Kaufmann, Matt; Moore, J Strother: Limited second-order functionality in a first-order setting (2020)
  20. Kovács, Laura; Lachnitt, Hanna; Szeider, Stefan: Formalizing graph trail properties in Isabelle/HOL (2020)

1 2 3 ... 32 33 34 next