Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/24676
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Abal, Iago | - |
dc.contributor.author | Cunha, Alcino | - |
dc.contributor.author | Hurd, Joe | - |
dc.contributor.author | Pinto, Jorge Sousa | - |
dc.date.accessioned | 2013-07-12T17:44:01Z | - |
dc.date.available | 2013-07-12T17:44:01Z | - |
dc.date.issued | 2012 | - |
dc.identifier.isbn | 978-3-642-31611-1 | - |
dc.identifier.issn | 0302-9743 | - |
dc.identifier.uri | https://hdl.handle.net/1822/24676 | - |
dc.description.abstract | Among many theories supported by SMT solvers, the theory of finite-precision bit-vector arithmetic is one of the most useful, for both hardware and software systems verification. This theory is also particularly useful for some specific domains such as cryptography, in which algorithms are naturally expressed in terms of bit-vectors. Cryptol is an example of a domain-specific language (DSL) and toolset for cryptography developed by Galois, Inc.; providing an SMT backend that relies on bit-vector decision procedures to certify the correctness of cryptographic specifications [3]. Most of these decision procedures use bit-blasting to reduce a bit-vector problem into pure propositional SAT. Unfortunately bit-blasting does not scale very well, especially in the presence of operators like multiplication or division. | por |
dc.description.sponsorship | (undefined) | por |
dc.language.iso | eng | por |
dc.publisher | Springer | por |
dc.relation | info:eu-repo/grantAgreement/FCT/3599-PPCDT/105034/PT | - |
dc.rights | openAccess | por |
dc.title | Using term rewriting to solve Bit-vector arithmetic problems (Poster Presentation) | por |
dc.type | conferencePaper | - |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | http://link.springer.com/chapter/10.1007/978-3-642-31612-8_51 | por |
sdum.publicationstatus | published | por |
oaire.citationStartPage | 493 | por |
oaire.citationEndPage | 495 | por |
oaire.citationTitle | 15th International Conference on Theory and Applications of Satisfiability Testing | por |
oaire.citationVolume | 7317 LNCS | por |
dc.identifier.doi | 10.1007/978-3-642-31612-8_51 | - |
sdum.journal | Lecture Notes in Computer Science (including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | por |
sdum.conferencePublication | 15th International Conference on Theory and Applications of Satisfiability Testing | por |
dc.subject.acm | Hardware_ARITHMETICANDLOGICSTRUCTURES | - |
Aparece nas coleções: |