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 23, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.