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 541 articles , 1 standard article )

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

1 2 3 ... 26 27 28 next

  1. de Gouw, Stijn; de Boer, Frank S.; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic: Verifying OpenJDK’s sort method for generic collections (2019)
  2. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  3. Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
  4. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
  5. Lin, Yuhui; Bundy, Alan; Grov, Gudmund; Maclean, Ewen: Automating Event-B invariant proofs by rippling and proof patching (2019)
  6. Aiguier, Marc; Atif, Jamal; Bloch, Isabelle; Hudelot, Céline: Belief revision, minimal change and relaxation: A general framework based on satisfaction systems, and applications to description logics (2018)
  7. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  8. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
  9. Benzaken, V.; Contejean, É.; Keller, Ch.; Martins, E.: A Coq formalisation of SQL’s execution engines (2018)
  10. Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René: A verified efficient implementation of the LLL basis reduction algorithm (2018)
  11. Brucker, Achim D.; Ait-Sadoune, Idir; Crisafulli, Paolo; Wolff, Burkhart: Using the Isabelle ontology framework -- linking the formal with the informal (2018)
  12. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
  13. Charpentier, Isabelle; Cochelin, Bruno: Towards a full higher order AD-based continuation and bifurcation framework (2018)
  14. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  15. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  16. Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike: Mechanized proofs of opacity: a comparison of two techniques (2018)
  17. Diekmann, Cornelius; Hupel, Lars; Michaelis, Julius; Haslbeck, Maximilian; Carle, Georg: Verified iptables firewall analysis and verification (2018)
  18. Guttmann, Walter: An algebraic framework for minimum spanning tree problems (2018)
  19. Guttmann, Walter: Verifying minimum spanning tree algorithms with Stone relation algebras (2018)
  20. Hupel, Lars; Nipkow, Tobias: A verified compiler from Isabelle/HOL to CakeML (2018)

1 2 3 ... 26 27 28 next