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

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

1 2 3 ... 33 34 35 next

  1. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
  2. Foster, Simon; Cavalcanti, Ana; Woodcock, Jim; Zeyda, Frank: Unifying theories of time with generalised reactive processes (2018)
  3. Maggesi, Marco: A formalization of metric spaces in HOL light (2018)
  4. Albert, Elvira; Bezirgiannis, Nikolaos; de Boer, Frank; Martin-Martin, Enrique: A formal, resource consumption-preserving translation of actors to Haskell (2017)
  5. 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)
  6. Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke: A formally verified proof of the central limit theorem (2017)
  7. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: A formalisation of nominal $\alpha$-equivalence with A and AC function symbols (2017)
  8. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2017)
  9. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  10. Berghammer, Rudolf; Stucke, Insa; Winter, Michael: Using relation-algebraic means and tool support for investigating and computing bipartitions (2017)
  11. 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)
  12. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  13. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Soundness and completeness proofs by coinductive methods (2017)
  14. Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel: A lambda-free higher-order recursive path order (2017)
  15. Bowles, Juliana; Caminati, Marco B.: A verified algorithm enumerating event structures (2017)
  16. Brockschmidt, Marc; Joosten, Sebastiaan J.C.; Thiemann, René; Yamada, Akihisa: Certifying safety and termination proofs for integer transition systems (2017)
  17. Butler, David; Aspinall, David; Gascón, Adrià: How to simulate it in Isabelle: towards formal proof for secure multi-party computation (2017)
  18. Butterfield, Andrew: Utpcalc -- a calculator for UTP predicates (2017)
  19. Coghetto, Roland: Gauge integral (2017)
  20. Cruz-Filipe, Luís; Heule, Marijn J.H.; Hunt Jr., Warren A.; Kaufmann, Matt; Schneider-Kamp, Peter: Efficient certified RAT verification (2017)

1 2 3 ... 33 34 35 next