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

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

1 2 3 ... 44 45 46 next

  1. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  2. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  3. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  4. 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)
  5. Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank: Unifying theories of reactive design contracts (2020)
  6. Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of algebraic numbers in Isabelle/HOL (2020)
  7. Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
  8. Li, Wenda; Paulson, Lawrence C.: Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (2020)
  9. Roffé, Ariel Jonathan: Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts (2020)
  10. Strobel, Michael: Non-standard analysis in dynamic geometry (2020)
  11. Zhang, Xingyuan; Urban, Christian; Wu, Chunhan: Priority inheritance protocol proved correct (2020)
  12. Abdulaziz, Mohammad; Paulson, Lawrence C.: An Isabelle/HOL formalisation of Green’s theorem (2019)
  13. Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark: Extending SMT solvers to higher-order logic (2019)
  14. Bayer, Jonas; David, Marco; Pal, Abhik; Stock, Benedikt: Beginners’ quest to formalize mathematics: a feasibility study in Isabelle (2019)
  15. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2019)
  16. Bohrer, Brandon; Fernández, Manuel; Platzer, André: (\mathsfdL_\iota): definite descriptions in differential dynamic logic (2019)
  17. Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
  18. Brown, Chad E.; Pąk, Karol: A tale of two set theories (2019)
  19. Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
  20. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)

1 2 3 ... 44 45 46 next