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

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

1 2 3 ... 18 19 20 next

  1. 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)
  2. Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
  3. Arthan, Rob: On definitions of constants and types in HOL (2016)
  4. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  5. Bettini, Lorenzo: Implementing type systems for the IDE with Xsemantics (2016)
  6. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  7. Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
  8. Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
  9. Maclean, Ewen; Ireland, Andrew; Grov, Gudmund: Proof automation for functional correctness in separation logic (2016)
  10. Maletzky, Alexander: Interactive proving, higher-order rewriting, and theory analysis in Theorema 2.0 (2016)
  11. Matichuk, Daniel; Murray, Toby; Wenzel, Makarius: Eisbach: a proof method language for Isabelle (2016)
  12. 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)
  13. Rabe, Florian: The future of logic: foundation-independence (2016)
  14. Zhang, Nan; Duan, Zhenhua; Tian, Cong: A complete axiom system for propositional projection temporal logic with cylinder computation model (2016)
  15. Zhang, Nan; Yang, Mengfei; Gu, Bin; Duan, Zhenhua; Tian, Cong: Verifying safety critical task scheduling systems in PPTL axiom system (2016)
  16. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Foundational extensible corecursion: a proof assistant perspective (2015)
  17. Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
  18. Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
  19. Dodds, Mike; Haas, Andreas; Kirsch, Christoph M.: A scalable, correct time-stamped stack (2015)
  20. Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias: A verified compiler for probability density functions (2015)

1 2 3 ... 18 19 20 next