Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/606| Title: | Formalization of incremental simplex algorithm by stepwise refinement | Authors: | Spasić, Mirko Marić, Filip |
Affiliations: | Informatics and Computer Science Informatics and Computer Science |
Issue Date: | 13-Sep-2012 | Related Publication(s): | International Symposium on Formal Methods FM 2012 | Journal: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Abstract: | We present an Isabelle/HOL formalization and total correctness proof for the incremental version of the Simplex algorithm which is used in most state-of-the-art SMT solvers. Formalization relies on stepwise program and data refinement, starting from a simple specification, going through a number of fine refinement steps, and ending up in a fully executable functional implementation. Symmetries present in the algorithm are handled with special care. © 2012 Springer-Verlag. |
URI: | https://research.matf.bg.ac.rs/handle/123456789/606 | ISBN: | 9783642327582 | ISSN: | 03029743 | DOI: | 10.1007/978-3-642-32759-9_35 |
| Appears in Collections: | Research outputs |
Show full item record
SCOPUSTM
Citations
11
checked on Dec 20, 2024
Page view(s)
21
checked on Dec 24, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.