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. Armstrong, Alasdair; Gomes, Victor B.F.; Struth, Georg: Building program construction and verification tools from algebraic principles (2016)
  2. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  3. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Cardinality of relations and relational approximation algorithms (2016)
  4. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  5. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  6. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
  7. Buchberger, Bruno: The GDML and eukim projects: short report on the initiative (2016)
  8. Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
  9. Guttmann, Walter: An algebraic approach to computations with progress (2016)
  10. Hoare, Tony; van Staden, Stephan; Möller, Bernhard; Struth, Georg; Zhu, Huibiao: Developments in concurrent Kleene algebra (2016)
  11. Rabe, Florian: The future of logic: foundation-independence (2016)
  12. Barras, Bruno; Tankink, Carst; Tassi, Enrico: Asynchronous processing of Coq documents: from the kernel up to the user interface (2015)
  13. Benzmüller, Christoph: Invited talk: on a (quite) universal theorem proving approach and its application in metaphysics (2015)
  14. Benzmüller, Christoph; Paleo, Bruno Woltzenlogel: Interacting with modal logics in the coq proof assistant (2015)
  15. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
  16. Berger, Ulrich; Lawrence, Andrew; Forsberg, Fredrik Nordvall; Seisenberger, Monika: Extracting verified decision procedures: DPLL and resolution (2015)
  17. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Tool-based verification of a relational vertex coloring program (2015)
  18. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Witnessing (co)datatypes (2015)
  19. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Coquelicot: A user-friendly library of real analysis for Coq (2015)
  20. Christakis, Maria; Godefroid, Patrice: Proving memory safety of the ANI windows image parser using compositional exhaustive testing (2015)

1 2 3 ... 17 18 19 next