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

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

1 2 3 ... 39 40 41 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. Hayes, Ian J.; Meinicke, Larissa A.; Winter, Kirsten; Colvin, Robert J.: A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency (2019)
  4. Immler, Fabian; Traut, Christoph: The flow of ODEs: formalization of variational equation and Poincaré map (2019)
  5. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
  6. Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
  7. Lammich, Peter: Refinement to imperative HOL (2019)
  8. Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
  9. Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
  10. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  11. Marić, Filip: Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (2019)
  12. Nipkow, Tobias; Brinkop, Hauke: Amortized complexity verified (2019)
  13. Schmidt-Schauß, Manfred; Sabel, David; Kutz, Yunus D. K.: Nominal unification with atom-variables (2019)
  14. Achermann, Reto; Humbel, Lukas; Cock, David; Roscoe, Timothy: Physical addressing on real hardware in Isabelle/HOL (2018)
  15. Avelar da Silva, Andréia B.; de Lima, Thaynara Arielly; Galdino, André Luiz: Formalizing ring theory in PVS (2018)
  16. 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)
  17. Avron, Arnon; Cohen, Liron: Applicable mathematics in a minimal computational theory of sets (2018)
  18. Balco, Samuel; Frittella, Sabine; Greco, Giuseppe; Kurz, Alexander; Palmigiano, Alessandra: Software tool support for modular reasoning in modal logics of actions (2018)
  19. Bannister, Callum; Höfner, Peter; Klein, Gerwin: Backwards and forwards with separation logic (2018)
  20. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)

1 2 3 ... 39 40 41 next