1. Research with MATF
  2. MATF
  3. Research outputs
Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/606
DC FieldValueLanguage
dc.contributor.authorSpasić, Mirkoen_US
dc.contributor.authorMarić, Filipen_US
dc.date.accessioned2022-08-13T15:50:06Z-
dc.date.available2022-08-13T15:50:06Z-
dc.date.issued2012-09-13-
dc.identifier.isbn9783642327582-
dc.identifier.issn03029743en
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/606-
dc.description.abstractWe 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.en
dc.publisherSpringeren_US
dc.relation.ispartofLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)en_US
dc.titleFormalization of incremental simplex algorithm by stepwise refinementen_US
dc.typeConference Objecten_US
dc.relation.conferenceInternational Symposium Formal Methods FM (18 ; 2012 ; Paris)en_US
dc.relation.publicationProceedings of the 18th International Symposium on Formal Methods FM 2012en_US
dc.identifier.doi10.1007/978-3-642-32759-9_35-
dc.identifier.scopus2-s2.0-84865959941-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/84865959941-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.isbn978-3-642-32758-2en_US
dc.description.rankM33en_US
dc.relation.firstpage434en_US
dc.relation.lastpage449en_US
dc.relation.volume7436 LNCSen_US
item.grantfulltextnone-
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.openairetypeConference Object-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0002-9304-4007-
crisitem.author.orcid0000-0001-7219-6960-
Appears in Collections:Research outputs
Show simple item record

SCOPUSTM   
Citations

12
checked on Nov 27, 2025

Page view(s)

22
checked on Jan 19, 2025

Google ScholarTM

Check

Altmetric

Altmetric


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