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

Showing results 1 to 20 of 393.
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. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  3. Felgenhauer, Bertram; Thiemann, René: Reachability, confluence, and termination analysis with state-compatible automata (2017)
  4. Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \ssfAProVE (2017)
  5. Juliana Bowles, Marco B. Caminati: A Verified Algorithm Enumerating Event Structures (2017) arXiv
  6. Kanckos, Annika; Woltzenlogel Paleo, B.: Variants of Gödel’s ontological proof in a natural deduction calculus (2017)
  7. Nagele, Julian; Felgenhauer, Bertram; Zankl, Harald: Certifying confluence proofs via relative termination and rule labeling (2017)
  8. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  9. Stucke, Insa: Reasoning about cardinalities of relations with applications supported by proof assistants (2017)
  10. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  11. Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
  12. Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
  13. Armstrong, Alasdair; Gomes, Victor B.F.; Struth, Georg: Building program construction and verification tools from algebraic principles (2016)
  14. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  15. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2016)
  16. Benzmüller, Christoph; Scott, Dana: Automating free logic in Isabelle/HOL (2016)
  17. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Cardinality of relations and relational approximation algorithms (2016)
  18. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  19. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  20. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)

1 2 3 ... 18 19 20 next