Fast three-valued abstract bit-vector arithmetic

DOI10.1007/978-3-030-94583-1_12MaRDI QIDQ2152654zbMATH OpenOpenAlexFDO

Authors Jan Onderka, Stefan Ratschan

Publication date 8 July 2022

Full work available at URL https://doi.org/10.1007/978-3-030-94583-1_12

zbMATH Keywords

multiplicationformal verificationadditioncomputer arithmeticthree-valued abstractionpseudo-Boolean modular inequality

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Fast vector arithmetic over \(\mathbb{F}_3\)
• Vector-matrix multiplication in ternary optimal computer
• Deciding Bit-Vector Arithmetic with Abstraction
• 3-valued abstraction: More precision at less cost
• Family of Fast Linearly Independent Ternary Arithmetic Transforms
• Properties and experimental results of fastest linearly independent ternary arithmetic transforms
• Fast garbling of circuits over 3-valued logic
• Efficient software implementation of binary field arithmetic using vector instruction sets
• Efficiently solving quantified bit-vector formulas

Cites work

• Automating abstract interpretation
• Handbook of model checking
• Matters computational. Ideas, algorithms, source code.
• On notation for ordinal numbers
• Pseudo-Boolean optimization
• Systematic design of program transformation frameworks by abstract interpretation
• The algorithm design manual

Cited in

(3)

• Computer Aided Verification
• Fast vector arithmetic over \(\mathbb{F}_3\)
• Deciding Bit-Vector Arithmetic with Abstraction

Describes a project that uses

Uses Software

• hfloat
• Stony Brook

This page was built for publication: Fast three-valued abstract bit-vector arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2152654)