Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/509
DC FieldValueLanguage
dc.contributor.authorMarić, Filipen_US
dc.contributor.authorJaničić, Predragen_US
dc.date.accessioned2022-08-13T10:14:42Z-
dc.date.available2022-08-13T10:14:42Z-
dc.date.issued2010-08-10-
dc.identifier.isbn3642142028-
dc.identifier.issn03029743en
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/509-
dc.description.abstractWe describe a system URBiVA for specifying and solving a range of problems by uniformly reducing them to bit-vector arithmetic (bva). A problem description is given in a C-like specification language and this high-level specification is transformed to a bva formula by symbolic execution. The formula is passed to a bva solver and, if it is satisfiable, its models give solutions of the problem. The system can be used for efficient modelling (specifying and solving) of a wide class of problems. Several state-of-the-art solvers for bva are currently used (Boolector, MathSAT, Yices) and additional solvers can be easily included. Hence, the system can be used not only as a specification and solving tool, but also as a platform for evaluation and comparison between bva solvers. © 2010 Springer-Verlag.en
dc.relation.ispartofLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)en_US
dc.titleURBiVA: Uniform reduction to bit-vector arithmeticen_US
dc.typeConference Paperen_US
dc.relation.publicationInternational Joint Conference on Automated Reasoning IJCAR 2010en_US
dc.identifier.doi10.1007/978-3-642-14203-1_29-
dc.identifier.scopus2-s2.0-77955245910-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/77955245910-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.firstpage346en_US
dc.relation.lastpage352en_US
dc.relation.volume6173 LNAIen_US
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.openairetypeConference Paper-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0001-7219-6960-
crisitem.author.orcid0000-0001-8922-4948-
Appears in Collections:Research outputs
Show simple item record

SCOPUSTM   
Citations

8
checked on Dec 18, 2024

Page view(s)

12
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


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