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

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

1 2 3 ... 22 23 24 next

  1. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  2. 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)
  3. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
  4. Brucker, Achim D.; Ait-Sadoune, Idir; Crisafulli, Paolo; Wolff, Burkhart: Using the Isabelle ontology framework -- linking the formal with the informal (2018)
  5. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
  6. Charpentier, Isabelle; Cochelin, Bruno: Towards a full higher order AD-based continuation and bifurcation framework (2018)
  7. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  8. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  9. Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike: Mechanized proofs of opacity: a comparison of two techniques (2018)
  10. Diekmann, Cornelius; Hupel, Lars; Michaelis, Julius; Haslbeck, Maximilian; Carle, Georg: Verified iptables firewall analysis and verification (2018)
  11. Mendes, Alexandra; Ferreira, João F.: Towards verified handwritten calculational proofs (short paper) (2018)
  12. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
  13. Shi, Ling; Zhao, Yongxin; Liu, Yang; Sun, Jun; Dong, Jin Song; Qin, Shengchao: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (2018)
  14. Aransay, Jesús; Divasón, Jose: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (2017)
  15. Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
  16. Bowles, Juliana; Caminati, Marco B.: A verified algorithm enumerating event structures (2017)
  17. Cauderlier, Raphaël; Dubois, Catherine: Focalize and dedukti to the rescue for proof interoperability (2017)
  18. Felgenhauer, Bertram; Thiemann, René: Reachability, confluence, and termination analysis with state-compatible automata (2017)
  19. Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: JTabWb: a Java framework for implementing terminating sequent and tableau calculi (2017)
  20. Glück, Roland: Algebraic investigation of connected components (2017)

1 2 3 ... 22 23 24 next