Isabelle

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.

This software is also referenced in ORMS.


References in zbMATH (referenced in 710 articles , 1 standard article )

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

1 2 3 ... 34 35 36 next

  1. Dalvandi, Sadegh; Dongol, Brijesh; Doherty, Simon; Wehrheim, Heike: Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (2022)
  2. Miller, Dale; Viel, Alexandre: The undecidability of proof search when equality is a logical connective (2022)
  3. Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
  4. Cau, Antonio; Kuhn, Stefan; Hoey, James: Reversibility of executable interval temporal logic specifications (2021)
  5. Chan, Hing Lun; Norrish, Michael: Mechanisation of the AKS algorithm (2021)
  6. de Lima, Thaynara Arielly; Galdino, André Luiz; Avelar, Andréia Borges; Ayala-Rincón, Mauricio: Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem (2021)
  7. De Lon, Adrian; Koepke, Peter; Lorenzen, Anton; Marti, Adrian; Schütz, Marcel; Sturzenhecker, Erik: Beautiful formalizations in Isabelle/Naproche (2021)
  8. Edmonds, Chelsea; Paulson, Lawrence C.: A modular first formalisation of combinatorial design theory (2021)
  9. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
  10. Fervari, Raul; Trucco, Francisco; Ziliani, Beta: Verification of dynamic bisimulation theorems in Coq (2021)
  11. Foster, Simon; Nemouchi, Yakoub; Gleirscher, Mario; Wei, Ran; Kelly, Tim: Integration of formal proof into unified assurance cases with Isabelle/SACM (2021)
  12. From, Asta Halkjær; Eschen, Agnes Moesgård; Villadsen, Jørgen: Formalizing axiomatic systems for propositional logic in Isabelle/HOL (2021)
  13. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
  14. Holub, Štěpán; Starosta, Štěpán: Binary intersection formalized (2021)
  15. Holub, Štěpán; Starosta, Štěpán: Lyndon words formalized in Isabelle/HOL (2021)
  16. Hou, Zhe: Fundamentals of logic and computation. With practical automated reasoning and verification (2021)
  17. Kohlhase, Michael; Rabe, Florian: Experiences from exporting major proof assistant libraries (2021)
  18. Koliesnikova, Daria; Ramière, Isabelle; Lebon, Frédéric: A unified framework for the computational comparison of adaptive mesh refinement strategies for all-quadrilateral and all-hexahedral meshes: locally adaptive multigrid methods versus h-adaptive methods (2021)
  19. Koutsoukou-Argyraki, Angeliki: Formalising mathematics -- in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started (2021)
  20. Li, Liyi; Gunter, Elsa L.: A complete semantics of (\mathbbK) and its translation to Isabelle (2021)

1 2 3 ... 34 35 36 next