Isabelle/Isar

Building formal method tools in the Isabelle/Isar framework --------- siehe Isar sid: 4599

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 96 articles )

Showing results 61 to 80 of 96.
Sorted by year (citations)
  1. Haftmann, Florian; Wenzel, Makarius: Local theory specifications in Isabelle/Isar (2009)
  2. Kaliszyk, Cezary; Wiedijk, Freek: Merging procedural and declarative proof (2009)
  3. Aransay, Jesús; Ballarin, Clemens; Rubio, Julio: A mechanized proof of the basic perturbation lemma (2008)
  4. Berghofer, Stefan; Wenzel, Makarius: Logic-free reasoning in Isabelle/Isar (2008)
  5. Rodríguez-Hortalá, Juan: A hierarchy of semantics for non-deterministic term rewriting systems (2008)
  6. Spichkova, Maria: Refinement-based verification of interactive real-time systems (2008)
  7. Wasserrab, Daniel; Lochbihler, Andreas: Formalizing a framework for dynamic slicing of program dependence graphs in Isabelle/HOL (2008)
  8. Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias: The Isabelle framework (2008)
  9. Billingsley, William; Robinson, Peter: Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book (2007)
  10. Brucker, Achim D.; Wolff, Burkhart: Test-sequence generation with Hol-TestGen with an application to firewall testing (2007)
  11. Haftmann, Florian; Wenzel, Makarius: Constructive type classes in Isabelle (2007)
  12. Narboux, Julien: Mechanical theorem proving in Tarski’s geometry (2007)
  13. Wenzel, Makarius; Wolff, Burkhart: Building formal method tools in the Isabelle/Isar framework (2007)
  14. Aboul-Hosn, Kamal; Kozen, Dexter: KAT-ML: an interactive theorem prover for Kleene algebra with tests (2006)
  15. Aspinall, David; Lüth, Christoph; Wolff, Burkhart: Assisted proof document authoring (2006)
  16. Avigad, Jeremy: Mathematical method and proof (2006)
  17. Ballarin, Clemens: Interpretation of locales in Isabelle: theories and proof contexts (2006)
  18. Berghofer, Stefan: Extracting a normalization algorithm in Isabelle/HOL (2006)
  19. Bortin, Maksym; Broch Johnsen, Einar; Lüth, Christoph: Structured formal development in Isabelle (2006)
  20. Meng, Jia; Quigley, Claire; Paulson, Lawrence C.: Automation for interactive proof: first prototype (2006)