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

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

1 2 3 ... 18 19 20 next

  1. Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
  2. Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
  3. Armstrong, Alasdair; Gomes, Victor B.F.; Struth, Georg: Building program construction and verification tools from algebraic principles (2016)
  4. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  5. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2016)
  6. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Cardinality of relations and relational approximation algorithms (2016)
  7. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  8. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  9. Blanchette, Jasmin Christian (ed.); Merz, Stephan (ed.): Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22--25, 2016. Proceedings (2016)
  10. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  11. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
  12. Brucker, Achim D.; Wolff, Burkhart: Monadic sequence testing and explicit test-refinements (2016)
  13. Buchberger, Bruno: The GDML and eukim projects: short report on the initiative (2016)
  14. Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
  15. Greuel, Gert-Martin (ed.); Koch, Thorsten (ed.); Paule, Peter (ed.); Sommese, Andrew (ed.): Mathematical software -- ICMS 2016. 5th international conference, Berlin, Germany, July 11--14, 2016. Proceedings (2016)
  16. Guttmann, Walter: An algebraic approach to computations with progress (2016)
  17. Hoare, Tony; van Staden, Stephan; Möller, Bernhard; Struth, Georg; Zhu, Huibiao: Developments in concurrent Kleene algebra (2016)
  18. Lochbihler, Andreas; Schneider, Joshua: Equational reasoning with applicative functors (2016)
  19. Rabe, Florian: The future of logic: foundation-independence (2016)
  20. Zhan, Bohua: AUTO2, A saturation-based heuristic prover for higher-order logic (2016)

1 2 3 ... 18 19 20 next