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

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

1 2 3 ... 31 32 33 next

  1. Albert, Elvira; Bezirgiannis, Nikolaos; de Boer, Frank; Martin-Martin, Enrique: A formal, resource consumption-preserving translation of actors to Haskell (2017)
  2. 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)
  3. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2017)
  4. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  5. Berghammer, Rudolf; Stucke, Insa; Winter, Michael: Using relation-algebraic means and tool support for investigating and computing bipartitions (2017)
  6. Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy: Foundational (co)datatypes and (co)recursion for higher-order logic (2017)
  7. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  8. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
  9. Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel: A lambda-free higher-order recursive path order (2017)
  10. Bowles, Juliana; Caminati, Marco B.: A verified algorithm enumerating event structures (2017)
  11. Brockschmidt, Marc; Joosten, Sebastiaan J.C.; Thiemann, René; Yamada, Akihisa: Certifying safety and termination proofs for integer transition systems (2017)
  12. Butler, David; Aspinall, David; Gascón, Adrià: How to simulate it in Isabelle: towards formal proof for secure multi-party computation (2017)
  13. Butterfield, Andrew: Utpcalc -- a calculator for UTP predicates (2017)
  14. Cruz-Filipe, Luís; Heule, Marijn J.H.; Hunt Jr., Warren A.; Kaufmann, Matt; Schneider-Kamp, Peter: Efficient certified RAT verification (2017)
  15. da Costa Cavalheiro, Simone André; Foss, Luciana; Ribeiro, Leila: Theorem proving graph grammars with attributes and negative application conditions (2017)
  16. Eberl, Manuel: Proving divide and conquer complexities in Isabelle/HOL (2017)
  17. Felgenhauer, Bertram; Thiemann, René: Reachability, confluence, and termination analysis with state-compatible automata (2017)
  18. Foster, Simon; Thiele, Bernhard; Cavalcanti, Ana; Woodcock, Jim: Towards a UTP semantics for Modelica (2017)
  19. 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)
  20. Guttmann, Walter: Stone relation algebras (2017)

1 2 3 ... 31 32 33 next