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

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

1 2 3 ... 35 36 37 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. 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)
  5. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
  6. Bertot, Yves; Rideau, Laurence; Théry, Laurent: Distant decimals of $\pi $: formal proofs of some algorithms computing them and guarantees of exact computation (2018)
  7. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  8. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
  9. Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut: Introduction to model checking (2018)
  10. Diekmann, Cornelius; Hupel, Lars; Michaelis, Julius; Haslbeck, Maximilian; Carle, Georg: Verified iptables firewall analysis and verification (2018)
  11. Foster, Simon; Cavalcanti, Ana; Woodcock, Jim; Zeyda, Frank: Unifying theories of time with generalised reactive processes (2018)
  12. Immler, Fabian: A verified ODE solver and the Lorenz attractor (2018)
  13. Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)
  14. Maggesi, Marco: A formalization of metric spaces in HOL light (2018)
  15. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
  16. Shankar, Natarajan: Combining model checking and deduction (2018)
  17. Steffen, Bernhard; Rüthing, Oliver; Huth, Michael: Mathematical foundations of advanced informatics. Volume 1. Inductive approaches (2018)
  18. Strecker, Martin: Interactive and automated proofs for graph transformations (2018)
  19. Struth, Georg: Hoare semigroups (2018)
  20. Albert, Elvira; Bezirgiannis, Nikolaos; de Boer, Frank; Martin-Martin, Enrique: A formal, resource consumption-preserving translation of actors to Haskell (2017)

1 2 3 ... 35 36 37 next