AMulet 2.0 for Verifying Multiplier Circuits

Daniela Kaufmann; Armin Biere

doi:10.1007/978-3-030-72013-1_19

AMulet 2.0 for Verifying Multiplier Circuits

Daniela Kaufmann
, Armin Biere

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

AMulet 2.0 is a fully automatic tool for the verification ofinteger multipliers using computer algebra. Our tool models multipliercircuits given as and-inverter graphs as a set of polynomials and appliespreprocessing techniques based on elimination theory of Gr ̈obner bases.Finally it uses a polynomial reduction algorithm to verify the correctnessof the given circuit.AMulet 2.0is a reactorization and improved re-implementation of our previous multiplier verification toolAMulet 1.0.

Original language	English
Title of host publication	International Conference on Tools and Algorithms for the Construction and Analysis of Systems , TACAS 2021.
Editors	Jan Friso Groote, Kim Guldstrand Larsen
Publisher	Springer
Pages	357-364
Number of pages	8
Volume	12652
ISBN (Print)	9783030720124
DOIs	https://doi.org/10.1007/978-3-030-72013-1_19
Publication status	Published - 2021

Publication series

Name	Lecture Notes in Computer Science
Volume	12652 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

Access to Document

10.1007/978-3-030-72013-1_19

Cite this

@inproceedings{7598404fd40842d8af6e874ad2d7c844,

title = "AMulet 2.0 for Verifying Multiplier Circuits",

abstract = "AMulet 2.0 is a fully automatic tool for the verification ofinteger multipliers using computer algebra. Our tool models multipliercircuits given as and-inverter graphs as a set of polynomials and appliespreprocessing techniques based on elimination theory of Gr{\" }obner bases.Finally it uses a polynomial reduction algorithm to verify the correctnessof the given circuit.AMulet 2.0is a reactorization and improved re-implementation of our previous multiplier verification toolAMulet 1.0.",

author = "Daniela Kaufmann and Armin Biere",

year = "2021",

doi = "10.1007/978-3-030-72013-1\_19",

language = "English",

isbn = "9783030720124",

volume = "12652",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "357--364",

editor = "Groote, \{Jan Friso\} and Larsen, \{Kim Guldstrand\}",

booktitle = "International Conference on Tools and Algorithms for the Construction and Analysis of Systems , TACAS 2021.",

}

AMulet 2.0 for Verifying Multiplier Circuits. / Kaufmann, Daniela; Biere, Armin.
International Conference on Tools and Algorithms for the Construction and Analysis of Systems , TACAS 2021.. ed. / Jan Friso Groote; Kim Guldstrand Larsen. Vol. 12652 Springer, 2021. p. 357-364 (Lecture Notes in Computer Science; Vol. 12652 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - AMulet 2.0 for Verifying Multiplier Circuits

AU - Kaufmann, Daniela

AU - Biere, Armin

PY - 2021

Y1 - 2021

N2 - AMulet 2.0 is a fully automatic tool for the verification ofinteger multipliers using computer algebra. Our tool models multipliercircuits given as and-inverter graphs as a set of polynomials and appliespreprocessing techniques based on elimination theory of Gr ̈obner bases.Finally it uses a polynomial reduction algorithm to verify the correctnessof the given circuit.AMulet 2.0is a reactorization and improved re-implementation of our previous multiplier verification toolAMulet 1.0.

AB - AMulet 2.0 is a fully automatic tool for the verification ofinteger multipliers using computer algebra. Our tool models multipliercircuits given as and-inverter graphs as a set of polynomials and appliespreprocessing techniques based on elimination theory of Gr ̈obner bases.Finally it uses a polynomial reduction algorithm to verify the correctnessof the given circuit.AMulet 2.0is a reactorization and improved re-implementation of our previous multiplier verification toolAMulet 1.0.

UR - https://www.scopus.com/pages/publications/85134345076

U2 - 10.1007/978-3-030-72013-1_19

DO - 10.1007/978-3-030-72013-1_19

M3 - Conference proceedings

SN - 9783030720124

VL - 12652

T3 - Lecture Notes in Computer Science

SP - 357

EP - 364

BT - International Conference on Tools and Algorithms for the Construction and Analysis of Systems , TACAS 2021.

A2 - Groote, Jan Friso

A2 - Larsen, Kim Guldstrand

PB - Springer

ER -

AMulet 2.0 for Verifying Multiplier Circuits

Abstract

Publication series

Fields of science

Access to Document

Other files and links

Cite this