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

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

1 2 3 ... 49 50 51 next

  1. Baxter, James; Ribeiro, Pedro; Cavalcanti, Ana: Sound reasoning in \textittock-CSP (2022)
  2. Dalvandi, Sadegh; Dongol, Brijesh; Doherty, Simon; Wehrheim, Heike: Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (2022)
  3. Dubut, Jérémy; Yamada, Akihisa: Fixed points theorems for non-transitive relations (2022)
  4. Fürer, Basil; Lochbihler, Andreas; Schneider, Joshua; Traytel, Dmitriy: Quotients of bounded natural functors (2022)
  5. Huerta y Munive, Jonathan Julián; Struth, Georg: Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (2022)
  6. Karayel, Emin; Gonzàlez, Edgar: Strong eventual consistency of the collaborative editing framework WOOT (2022)
  7. Arusoaie, Andrei: Certifying Findel derivatives for blockchain (2021)
  8. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  9. Bordg, Anthony; Lachnitt, Hanna; He, Yijun: Certified quantum computation in Isabelle/HOL (2021)
  10. Bromberger, Martin; Dragoste, Irina; Faqeh, Rasha; Fetzer, Christof; Krötzsch, Markus; Weidenbach, Christoph: A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (2021)
  11. Butler, D.; Lochbihler, A.; Aspinall, D.; Gascón, A.: Formalising (\varSigma)-protocols and commitment schemes using crypthol (2021)
  12. Chan, Hing Lun; Norrish, Michael: Mechanisation of the AKS algorithm (2021)
  13. Cristiá, Maximiliano; Rossi, Gianfranco: Automated proof of Bell-LaPadula security properties (2021)
  14. Foster, Simon; Nemouchi, Yakoub; Gleirscher, Mario; Wei, Ran; Kelly, Tim: Integration of formal proof into unified assurance cases with Isabelle/SACM (2021)
  15. From, Asta Halkjær; Eschen, Agnes Moesgård; Villadsen, Jørgen: Formalizing axiomatic systems for propositional logic in Isabelle/HOL (2021)
  16. Han, Ning; Li, Ximeng; Zhang, Qianying; Wang, Guohui; Shi, Zhiping; Guan, Yong: Executable semantics of Ethereum intermediate language (2021)
  17. Holub, Štěpán; Starosta, Štěpán: Lyndon words formalized in Isabelle/HOL (2021)
  18. Holub, Štěpán; Starosta, Štěpán: Binary intersection formalized (2021)
  19. Hóu, Zhé; Sanan, David; Tiu, Alwen; Liu, Yang; Hoa, Koh Chuen; Dong, Jin Song: An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model (2021)
  20. Jared Mejia, Alex Devonport, Murat Arcak: DaDRA: A Python Library for Data-Driven Reachability Analysis (2021) arXiv

1 2 3 ... 49 50 51 next