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

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

1 2 3 ... 17 18 19 next

  1. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  2. Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
  3. Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
  4. Armstrong, Alasdair; Gomes, Victor B.F.; Struth, Georg: Building program construction and verification tools from algebraic principles (2016)
  5. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  6. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2016)
  7. Benzmüller, Christoph; Scott, Dana: Automating free logic in Isabelle/HOL (2016)
  8. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Cardinality of relations and relational approximation algorithms (2016)
  9. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  10. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  11. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
  12. Blanchette, Jasmin Christian (ed.); Merz, Stephan (ed.): Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22--25, 2016. Proceedings (2016)
  13. Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2016)
  14. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  15. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
  16. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
  17. Brucker, Achim D.; Wolff, Burkhart: Monadic sequence testing and explicit test-refinements (2016)
  18. Buchberger, Bruno: The GDML and eukim projects: short report on the initiative (2016)
  19. Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
  20. 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)

1 2 3 ... 17 18 19 next