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

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

1 2 3 ... 36 37 38 next

  1. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)
  2. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  3. Schmidt-Schauß, Manfred; Sabel, David; Kutz, Yunus D. K.: Nominal unification with atom-variables (2019)
  4. Achermann, Reto; Humbel, Lukas; Cock, David; Roscoe, Timothy: Physical addressing on real hardware in Isabelle/HOL (2018)
  5. Avigad, Jeremy (ed.); Blanchette, Jasmin Christian (ed.); Klein, Gerwin (ed.); Paulson, Lawrence (ed.); Popescu, Andrei (ed.); Snelting, Gregor (ed.): Introduction to “Milestones in interactive theorem proving” (2018)
  6. Avron, Arnon; Cohen, Liron: Applicable mathematics in a minimal computational theory of sets (2018)
  7. Balco, Samuel; Frittella, Sabine; Greco, Giuseppe; Kurz, Alexander; Palmigiano, Alessandra: Software tool support for modular reasoning in modal logics of actions (2018)
  8. Bannister, Callum; Höfner, Peter; Klein, Gerwin: Backwards and forwards with separation logic (2018)
  9. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
  10. Bertot, Yves; Rideau, Laurence; Théry, Laurent: Distant decimals of $\pi $: formal proofs of some algorithms computing them and guarantees of exact computation (2018)
  11. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  12. Brucker, Achim D.; Ait-Sadoune, Idir; Crisafulli, Paolo; Wolff, Burkhart: Using the Isabelle ontology framework -- linking the formal with the informal (2018)
  13. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
  14. Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut: Introduction to model checking (2018)
  15. Coghetto, Roland: Klein-Beltrami model. Part I (2018)
  16. Coghetto, Roland: Klein-Beltrami model. Part II (2018)
  17. Czajka, Łukasz; Ekici, Burak; Kaliszyk, Cezary: Concrete semantics with Coq and CoqHammer (2018)
  18. Diekmann, Cornelius; Hupel, Lars; Michaelis, Julius; Haslbeck, Maximilian; Carle, Georg: Verified iptables firewall analysis and verification (2018)
  19. Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa: A formalization of the LLL basis reduction algorithm (2018)
  20. Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias: Verified analysis of random binary tree structures (2018)

1 2 3 ... 36 37 38 next