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

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

1 2 3 ... 18 19 20 next

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

1 2 3 ... 18 19 20 next