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

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

1 2 3 ... 28 29 30 next

  1. Andronick, June: Reasoning about concurrency in high-assurance, high-performance software systems (2017)
  2. Aransay, Jesús; Divasón, Jose: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (2017)
  3. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  4. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  5. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
  6. Bowles, Juliana; Caminati, Marco B.: A verified algorithm enumerating event structures (2017)
  7. Brockschmidt, Marc; Joosten, Sebastiaan J.C.; Thiemann, René; Yamada, Akihisa: Certifying safety and termination proofs for integer transition systems (2017)
  8. Cruz-Filipe, Luís; Heule, Marijn J.H.; Hunt Jr., Warren A.; Kaufmann, Matt; Schneider-Kamp, Peter: Efficient certified RAT verification (2017)
  9. Eberl, Manuel: Proving divide and conquer complexities in Isabelle/HOL (2017)
  10. Felgenhauer, Bertram; Thiemann, René: Reachability, confluence, and termination analysis with state-compatible automata (2017)
  11. Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \ssfAProVE (2017)
  12. Guttmann, Walter: Stone relation algebras (2017)
  13. Juliana Bowles, Marco B. Caminati: A Verified Algorithm Enumerating Event Structures (2017) arXiv
  14. Kanckos, Annika; Woltzenlogel Paleo, B.: Variants of Gödel’s ontological proof in a natural deduction calculus (2017)
  15. Kunčar, Ondřej; Popescu, Andrei: Comprehending Isabelle/HOL’s consistency (2017)
  16. Lammich, Peter: Efficient verified (UN)SAT certificate checking (2017)
  17. Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
  18. Nagashima, Yutaka; Kumar, Ramana: A proof strategy language and proof script generation for Isabelle/HOL (2017)
  19. Nagele, Julian; Felgenhauer, Bertram; Zankl, Harald: Certifying confluence proofs via relative termination and rule labeling (2017)
  20. Sternagel, Christian; Sternagel, Thomas: Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (2017)

1 2 3 ... 28 29 30 next