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

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

1 2 3 ... 37 38 39 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. Immler, Fabian; Traut, Christoph: The flow of ODEs: formalization of variational equation and Poincaré map (2019)
  4. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
  5. Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
  6. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  7. Schmidt-Schauß, Manfred; Sabel, David; Kutz, Yunus D. K.: Nominal unification with atom-variables (2019)
  8. Achermann, Reto; Humbel, Lukas; Cock, David; Roscoe, Timothy: Physical addressing on real hardware in Isabelle/HOL (2018)
  9. 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)
  10. Avron, Arnon; Cohen, Liron: Applicable mathematics in a minimal computational theory of sets (2018)
  11. Balco, Samuel; Frittella, Sabine; Greco, Giuseppe; Kurz, Alexander; Palmigiano, Alessandra: Software tool support for modular reasoning in modal logics of actions (2018)
  12. Bannister, Callum; Höfner, Peter; Klein, Gerwin: Backwards and forwards with separation logic (2018)
  13. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
  14. Bertot, Yves; Rideau, Laurence; Théry, Laurent: Distant decimals of (\pi): formal proofs of some algorithms computing them and guarantees of exact computation (2018)
  15. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  16. Brucker, Achim D.; Ait-Sadoune, Idir; Crisafulli, Paolo; Wolff, Burkhart: Using the Isabelle ontology framework -- linking the formal with the informal (2018)
  17. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
  18. Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut: Introduction to model checking (2018)
  19. Coghetto, Roland: Klein-Beltrami model. II (2018)
  20. Coghetto, Roland: Klein-Beltrami model. I (2018)

1 2 3 ... 37 38 39 next