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

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

1 2 3 ... 18 19 20 next

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

1 2 3 ... 18 19 20 next