Posted on by Achim D. Brucker, licensed under CC BY-ND 4.0.

Release: Isabelle/DOF 1.3.0

We are proud to announce the release of Isabelle/DOF 1.3.0. Isabelle/DOF is a Document Ontology Framework on top of Isabelle 2021-1. Isabelle/DOF allows for both conventional typesetting and formal development.


The most important user-visible changes are:

  • Isabelle/DOF is now a proper Isabelle component that should be installed using the isabelle components command. The installation script is now only a convenient way of installing the required AFP entries.
  • The tool mkroot_DOF has been renamed to dof_mkroot (and reimplemented in Scala).
  • The project-specific configuration is not part of the ROOT file, the formerly used isadof.cfg is obsolete and no longer supported.
  • Removed explicit use of the document/build script in favor of reimplementing its functionality in Scala as an Isabelle/DOF specific document generator.

Migrating Existing Projects

The following steps need to be executed to migrate existing projects from older version of Isabelle/DOF:

  • If your ROOT file does not contain the option document_build = dof, add it.

  • The script document/build should be removed and its entry in the ROOT file deleted.

  • The configuration (i.e., which ontologies to use and which document template to use) needs to be upgraded. For example, if you document/isadof.cfg looks as follows:

    Template: scrreprt-modern
    Ontology: technical_report cenelec_50128

    The options of the corresponding ROOT file needs to be updated to include:

      dof_ontologies = "Isabelle_DOF.technical_report Isabelle_DOF.cenelec_50128", dof_template = "Isabelle_DOF.scrreprt-modern",

    Thereafter, the file document/isadof.cfg should be removed nd its entry in the ROOT file deleted.


Isabelle/DOF 1.3.0 is available for Isabelle 2021-1:

Welcome to the blog of the Software Assurance & Security Research Team at the University of Exeter. We blog regularly news, tips & tricks, as well as fun facts about software assurance, reliability, security, testing, verification, hacking, and logic.

You can also follow us on Twitter: @logicalhacking.




academia ai android apidesign appsec bitcoin blockchain bpmn browser browserextensions browsersecurity bug certification chrome composition cordova dast devops devsecops dom dsbd efsm epsrc event extensions fixeffort floss formaldocument formalmethods funding hol-ocl hol-testgen humanfactor hybridapps iast industry internetofthings iot isabelle/hol isabelledof isadof latex logic maintance malicous mbst mobile mobile apps modelinference modeling monads monitoring msc ocl ontology opensource owasp patches pet phd phdlife phishing policy protocols publishing reliability research safelinks safety sap sast sdlc secdevops secureprogramming security securityengineering securitytesting semantics servicecomposition skills smartcontract smartthings softwareeinginering softwaresecurity softwaresupplychain solidity staff&positions statemachine studentproject tcb test&proof testing tips&tricks tools transport tuos uk uoe upgrade usability verification vulnerabilities vulnerableapplication webinar websecurity


blog whole site