Automatic data refinement. We present the Autoref tool for Isabelle/HOL, which automatically refines algorithms specified over abstract concepts like maps and sets to algorithms over concrete implementations like red-black-trees, and produces a refinement theorem. It is based on ideas borrowed from relational parametricity due to Reynolds and Wadler.par The tool allows for rapid prototyping of verified, executable algorithms. Moreover, it can be configured to fine-tune the result to the user’s needs. Our tool is able to automatically instantiate generic algorithms, which greatly simplifies the implementation of executable data structures.par Thanks to its integration with the Isabelle refinement framework and the Isabelle collection framework, Autoref can be used as a backend to a stepwise refinement based development approach, having access to a rich library of verified data structures. We have evaluated the tool by synthesizing efficiently executable refinements for some complex algorithms, as well as by implementing a library of generic algorithms for maps and sets.

References in zbMATH (referenced in 15 articles , 1 standard article )

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

  1. Fürer, Basil; Lochbihler, Andreas; Schneider, Joshua; Traytel, Dmitriy: Quotients of bounded natural functors (2022)
  2. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  3. Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
  4. Lammich, Peter: Refinement to imperative HOL (2019)
  5. Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
  6. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  7. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  8. Diekmann, Cornelius; Hupel, Lars; Michaelis, Julius; Haslbeck, Maximilian; Carle, Georg: Verified iptables firewall analysis and verification (2018)
  9. Immler, Fabian: A verified ODE solver and the Lorenz attractor (2018)
  10. 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)
  11. Lochbihler, Andreas: Probabilistic functions and cryptographic oracles in higher order logic (2016)
  12. Martin-Dorel, Érik; Hanrot, Guillaume; Mayero, Micaela; Théry, Laurent: Formally verified certificate checkers for hardest-to-round computation (2015)
  13. Aransay, Jesús; Divasón, Jose: Formalization and execution of linear algebra: from theorems to algorithms (2014)
  14. Huffman, Brian; Kunčar, Ondřej: Lifting and transfer: a modular design for quotients in Isabelle/HOL (2013)
  15. Lammich, Peter: Automatic data refinement (2013)