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

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

1 2 3 ... 48 49 50 next

  1. Arusoaie, Andrei: Certifying Findel derivatives for blockchain (2021)
  2. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  3. Bordg, Anthony; Lachnitt, Hanna; He, Yijun: Certified quantum computation in Isabelle/HOL (2021)
  4. Butler, D.; Lochbihler, A.; Aspinall, D.; Gascón, A.: Formalising (\varSigma)-protocols and commitment schemes using crypthol (2021)
  5. Chan, Hing Lun; Norrish, Michael: Mechanisation of the AKS algorithm (2021)
  6. Cristiá, Maximiliano; Rossi, Gianfranco: Automated proof of Bell-LaPadula security properties (2021)
  7. Han, Ning; Li, Ximeng; Zhang, Qianying; Wang, Guohui; Shi, Zhiping; Guan, Yong: Executable semantics of Ethereum intermediate language (2021)
  8. Holub, Štěpán; Starosta, Štěpán: Binary intersection formalized (2021)
  9. Hóu, Zhé; Sanan, David; Tiu, Alwen; Liu, Yang; Hoa, Koh Chuen; Dong, Jin Song: An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model (2021)
  10. Jared Mejia, Alex Devonport, Murat Arcak: DaDRA: A Python Library for Data-Driven Reachability Analysis (2021) arXiv
  11. Koutsoukou-Argyraki, Angeliki: Formalising mathematics -- in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started (2021)
  12. Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
  13. Maletzky, Alexander: A generic and executable formalization of signature-based Gröbner basis algorithms (2021)
  14. Nipkow, Tobias; Roßkopf, Simon: Isabelle’s metalogic: formalization and proof checker (2021)
  15. Popescu, Andrei; Lammich, Peter; Hou, Ping: CoCon: a conference management system with formally verified document confidentiality (2021)
  16. Popescu, Andrei; Traytel, Dmitriy: Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant (2021)
  17. Reed Oei, Dun Ma, Christian Schulz, Philipp Hieronymi: Pecan: An Automated Theorem Prover for Automatic Sequences using Büchi Automata (2021) arXiv
  18. Rusu, Vlad; Nowak, David: (Co)inductive proof systems for compositional proofs in reachability logic (2021)
  19. Simić, Danijela; Marić, Filip; Boutry, Pierre: Formalization of the Poincaré disc model of hyperbolic geometry (2021)
  20. Sison, Robert; Murray, Toby: Verified secure compilation for mixed-sensitivity concurrent programs (2021)

1 2 3 ... 48 49 50 next