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.
This software is also referenced in ORMS.
Keywords for this software
References in zbMATH (referenced in 393 articles , 1 standard article )
Showing results 1 to 20 of 393.
Sorted by year (- 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)
- Bowles, Juliana; Caminati, Marco B.: A verified algorithm enumerating event structures (2017)
- Kaliszyk, Cezary; Pąk, Karol: Presentation and manipulation of Mizar properties in an Isabelle object logic (2017)
- Maletzky, Alexander; Windsteiger, Wolfgang: The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema (2017)
- Stucke, Insa: Reasoning about cardinalities of relations with applications supported by proof assistants (2017)
- Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
- Arthan, Rob: On definitions of constants and types in HOL (2016)
- Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
- Bettini, Lorenzo: Implementing type systems for the IDE with Xsemantics (2016)
- Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
- Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
- Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
- Maclean, Ewen; Ireland, Andrew; Grov, Gudmund: Proof automation for functional correctness in separation logic (2016)
- Maletzky, Alexander: Interactive proving, higher-order rewriting, and theory analysis in Theorema 2.0 (2016)
- Matichuk, Daniel; Murray, Toby; Wenzel, Makarius: Eisbach: a proof method language for Isabelle (2016)
- Nixon, Richard; Dierig, Christoph; Mt-Isa, Shahrul; Stöckert, Isabelle; Tong, Thaison; Kuhls, Silvia; Hodgson, Gemma; Pears, John; Waddingham, Ed; Hockley, Kimberley; Thomson, Andrew: A case study using the PrOACT-URL and BRAT frameworks for structured benefit risk assessment (2016)
- Rabe, Florian: The future of logic: foundation-independence (2016)
- Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (extended version) (2016)
- Zhang, Nan; Duan, Zhenhua; Tian, Cong: A complete axiom system for propositional projection temporal logic with cylinder computation model (2016)
- Zhang, Nan; Yang, Mengfei; Gu, Bin; Duan, Zhenhua; Tian, Cong: Verifying safety critical task scheduling systems in PPTL axiom system (2016)