@inproceedings{dd3a6aeed2c549968ecbc40b4db719f6,
title = "A Verified Decision Procedure for Orders in Isabelle/HOL",
abstract = "We present the first verified implementation of a decision procedure for the quantifier-free theory of partial and linear orders. We formalise the procedure in Isabelle/HOL and provide a specification that is made executable using Isabelle{\textquoteright}s code generator. The procedure is already part of the development version of Isabelle as a sub-procedure of the simplifier.",
author = "Lukas Stevens and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 ; Conference date: 18-10-2021 Through 22-10-2021",
year = "2021",
doi = "10.1007/978-3-030-88885-5_9",
language = "English",
isbn = "9783030888848",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "127--143",
editor = "Zhe Hou and Vijay Ganesh",
booktitle = "Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings",
}