Autoref swMATH ID: 12809 Software Authors: Lammich, Peter Description: 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. Homepage: https://www21.in.tum.de/~lammich/autoref/ Dependencies: Isabelle/HOL Related Software: Isabelle/HOL; Isabelle; Archive Formal Proofs; Lifting; Transfer; HOL; Coq; Locales; Gabow SCC; CAVA LTL Modelchecker; CakeML; GitHub; Coq/SSReflect; Refinement Monadic; Real_Impl; Rank Nullity; Gauss-Jordan; kepler98; seL4; PVS Cited in: 15 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Automatic data refinement. Zbl 1317.68216Lammich, Peter 2013 all top 5 Cited by 27 Authors 5 Lammich, Peter 4 Lochbihler, Andreas 2 Aransay, Jesús 2 Divasón, Jose 1 Basin, David A. 1 Blanchette, Jasmin Christian 1 Carle, Georg 1 Diekmann, Cornelius 1 Fleury, Mathias 1 Fürer, Basil 1 Hanrot, Guillaume 1 Haslbeck, Maximilian P. L. 1 Huffman, Brian 1 Hupel, Lars 1 Immler, Fabian 1 Kunčar, Ondřej 1 Martin-Dorel, Érik 1 Mayero, Micaela 1 Michaelis, Julius 1 Nipkow, Tobias 1 Paulson, Lawrence Charles 1 Schneider, Joshua P. 1 Sefidgar, S. Reza 1 Théry, Laurent 1 Traytel, Dmitry 1 Weidenbach, Christoph 1 Wenzel, Makarius Cited in 4 Serials 8 Journal of Automated Reasoning 1 Journal of Cryptology 1 Formal Aspects of Computing 1 Logical Methods in Computer Science all top 5 Cited in 9 Fields 15 Computer science (68-XX) 3 Numerical analysis (65-XX) 2 Mathematical logic and foundations (03-XX) 2 Linear and multilinear algebra; matrix theory (15-XX) 2 Information and communication theory, circuits (94-XX) 1 Ordinary differential equations (34-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Biology and other natural sciences (92-XX) Citations by Year