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

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

1 2 3 ... 45 46 47 next

  1. Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
  2. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  3. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  4. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  5. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  6. Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (2020)
  7. Dolu, Nazlı; Hastürk, Umur; Tural, Mustafa Kemal: Solution methods for a min-max facility location problem with regional customers considering closest Euclidean distances (2020)
  8. Echenim, Mnacho; Guiol, Hervé; Peltier, Nicolas: Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (2020)
  9. Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank: Unifying theories of reactive design contracts (2020)
  10. Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
  11. Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of algebraic numbers in Isabelle/HOL (2020)
  12. Kirchner, Daniel; Benzmüller, Christoph; Zalta, Edward N.: Mechanizing Principia Logico-Metaphysica in functional type-theory (2020)
  13. Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
  14. Li, Wenda; Paulson, Lawrence C.: Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (2020)
  15. Peña, Ricardo: An assertional proof of red-black trees using Dafny (2020)
  16. Roffé, Ariel Jonathan: Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts (2020)
  17. Shi, Zhiping; Guan, Yong; Li, Ximeng: Formalization of complex analysis and matrix theory (2020)
  18. Sternagel, Christian: A mechanized proof of Higman’s lemma by open induction (2020)
  19. Strobel, Michael: Non-standard analysis in dynamic geometry (2020)
  20. Zhang, Xingyuan; Urban, Christian; Wu, Chunhan: Priority inheritance protocol proved correct (2020)

1 2 3 ... 45 46 47 next