Stem arithmet$ (all stems)

242 papers:

DAC-2015-CiesielskiYBLR #verification

Verification of gate-level arithmetic circuits by function extraction (MJC, CY, WB, DL, AR), p. 6.

DATE-2015-GiefersPH #kernel

Accelerating arithmetic kernels with coherent attached FPGA coprocessors (HG, RP, CH), pp. 1072–1077.

DATE-2015-SunKPE #algebra #geometry #using #verification

Formal verification of sequential Galois field arithmetic circuits using algebraic geometry (XS, PK, TP, FE), pp. 1623–1628.

DATE-2015-WeiDLW #metaprogramming

A universal macro block mapping scheme for arithmetic circuits (XW, YD, TKL, YLW), pp. 1629–1634.

FoSSaCS-2015-HabermehlK #on the #quantifier

On Presburger Arithmetic Extended with Modulo Counting Quantifiers (PH, DK), pp. 375–389.

TACAS-2015-DanglLW #contest #float #recursion #source code

CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic — (Competition Contribution) (MD, SL, PW), pp. 423–425.

TACAS-2015-SebastianiT #cost analysis #modulo theories #optimisation

Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions (RS, PT), pp. 335–349.

PPDP-2015-Tarau #combinator #on the #representation

On a uniform representation of combinators, arithmetic, λ terms and types (PT), pp. 244–255.

CADE-2015-Bromberger0W #integer #linear #revisited

Linear Integer Arithmetic Revisited (MB, TS, CW), pp. 623–637.

CSL-2015-Berardi #comprehension #higher-order #induction

Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness (SB), pp. 343–358.

LICS-2015-LechnerOW #complexity #linear #on the

On the Complexity of Linear Arithmetic with Divisibility (AL, JO, JW), pp. 667–676.

DAC-2014-PrussKE #abstraction #equivalence #scalability #using #verification

Equivalence Verification of Large Galois Field Arithmetic Circuits using Word-Level Abstraction via Gröbner Bases (TP, PK, FE), p. 6.

DAC-2014-ShiBSBC #online #synthesis #trade-off

Datapath Synthesis for Overclocking: Online Arithmetic for Latency-Accuracy Trade-offs (KS, DB, EAS, SB, GAC), p. 6.

DATE-2014-LeeserMRW #effectiveness #float #reasoning

Make it real: Effective floating-point reasoning via exact arithmetic (ML, SM, JR, TW), pp. 1–4.

DATE-2014-SarafBLR #probability #using

IIR filters using stochastic arithmetic (NS, KB, DJL, MDR), pp. 1–6.

DATE-2014-SchollPDA #linear

Simple interpolants for linear arithmetic (CS, FP, SD, EA), pp. 1–6.

STOC-2014-KayalLSS #bound

Super-polynomial lower bounds for depth-4 homogeneous arithmetic formulas (NK, NL, CS, SS), pp. 119–127.

STOC-2014-KayalSS #bound

A super-polynomial lower bound for regular arithmetic formulas (NK, CS, RS), pp. 146–153.

STOC-2014-KumarS #all about #reduction

The limits of depth reduction for arithmetic formulas: it’s all about the top fan-in (MK, SS), pp. 136–145.

ICALP-v1-2014-KumarS #bound

Superpolynomial Lower Bounds for General Homogeneous Depth 4 Arithmetic Circuits (MK, SS), pp. 751–762.

LATA-2014-MasseTT #on the

On the Arithmetics of Discrete Figures (ABM, AMT, HT), pp. 198–209.

HIMI-AS-2014-HirashimaYH #learning #problem #word

Triplet Structure Model of Arithmetical Word Problems for Learning by Problem-Posing (TH, SY, YH), pp. 42–50.

PADL-2014-Tarau #declarative #specification

A Declarative Specification of Giant Number Arithmetic (PT), pp. 120–135.

SAC-2014-TarauB #algorithm

Arithmetic algorithms for hereditarily binary natural numbers (PT, BPB), pp. 1593–1600.

CAV-2014-TiwariL

A Nonlinear Real Arithmetic Fragment (AT, PL), pp. 729–736.

IJCAR-2014-StroderGBFFHS #memory management #pointer #proving #safety #source code #termination

Proving Termination and Memory Safety for Programs with Pointer Arithmetic (TS, JG, MB, FF, CF, JH, PSK), pp. 208–223.

LICS-CSL-2014-Haase #subclass

Subclasses of presburger arithmetic and the weak EXP hierarchy (CH), p. 10.

ICALP-v1-2013-KumarMN #bound

Arithmetic Circuit Lower Bounds via MaxRank (MK, GM, JS), pp. 661–672.

ICALP-v2-2013-Woods #generative

Presburger Arithmetic, Rational Generating Functions, and Quasi-Polynomials (KW), pp. 410–421.

CADE-2013-GangeSSS #composition #constraints #difference

Solving Difference Constraints over Modular Arithmetic (GG, HS, PJS, PS), pp. 215–230.

RTA-2013-WinklerZM #automation #proving #sequence #termination

Beyond Peano Arithmetic — Automatically Proving Termination of the Goodstein Sequence (SW, HZ, AM), pp. 335–351.

TLCA-2013-Blot #game studies

Realizability for Peano Arithmetic with Winning Conditions in HON Games (VB), pp. 77–92.

DAC-2012-KahngK #approximate #configuration management #design

Accuracy-configurable adder for approximate arithmetic designs (ABK, SK), pp. 820–825.

STOC-2012-Ajtai #nondeterminism #testing

Determinism versus nondeterminism with arithmetic tests and computation: extended abstract (MA), pp. 249–268.

KDIR-2012-HaanR #detection

Detecting Temporally Related Arithmetical Patterns — An Extension of Complex Event Processing (RdH, MR), pp. 329–332.

PADL-2012-Tarau #declarative #specification

A Declarative Specification of Tree-Based Symbolic Arithmetic Computations (PT), pp. 273–288.

SAC-2012-Affeldt #library #low level #on the

On construction of a library of formally verified low-level arithmetic functions (RA), pp. 1326–1331.

SAC-2012-Skubch #constraints #realtime

Solving non-linear arithmetic constraints in soft realtime environments (HS), pp. 67–73.

CSL-2012-Aschieri #axiom #interactive

Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms (FA), pp. 31–45.

CSL-2012-Hida #axiom

A Computational Interpretation of the Axiom of Determinacy in Arithmetic (TH), pp. 335–349.

CSL-2012-Kuroda #axiom #bound #concept #proving

Axiomatizing proof tree concepts in Bounded Arithmetic (SK), pp. 440–454.

ICLP-2012-FilardoE #finite #flexibility

A Flexible Solver for Finite Arithmetic Circuits (NWF, JE), pp. 425–438.

IJCAR-2012-BobotCCIMMM #integer #linear

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic (FB, SC, EC, MI, AM, AM, GM), pp. 67–81.

IJCAR-2012-FalkeK #induction #linear

Rewriting Induction + Linear Arithmetic = Decision Procedure (SF, DK), pp. 241–255.

IJCAR-2012-JovanovicM

Solving Non-linear Arithmetic (DJ, LMdM), pp. 339–354.

IJCAR-2012-SpielmannK #bound #synthesis

Synthesis for Unbounded Bit-Vector Arithmetic (AS, VK), pp. 499–513.

SAT-2012-AbalCHP #problem #term rewriting #using

Using Term Rewriting to Solve Bit-Vector Arithmetic Problems — (Poster Presentation) (IA, AC, JH, JSP), pp. 493–495.

SAT-2012-CorziliusLJA #named

SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox — (Tool Presentation) (FC, UL, SJ, EÁ), pp. 442–448.

DATE-2011-DraneC #optimisation

Optimisation of mutually exclusive arithmetic sum-of-products (TD, GAC), pp. 1388–1393.

DATE-2011-MedwedM #detection #fault #logic

Arithmetic logic units with high error detection rates to counteract fault attacks (MM, SM), pp. 1644–1649.

TACAS-2011-GriggioLS #generative #integer #linear #performance #satisfiability

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic (AG, TTHL, RS), pp. 143–157.

ICALP-v1-2011-JansenS #constant #polynomial

Permanent Does Not Have Succinct Polynomial Size Arithmetic Circuits of Constant Depth (MJJ, RS), pp. 724–735.

ICALP-v1-2011-Mengel #constraints #problem

Characterizing Arithmetic Circuit Classes by Constraint Satisfaction Problems — (Extended Abstract) (SM), pp. 700–711.

CADE-2011-JovanovicM #integer #linear

Cutting to the Chase Solving Linear Integer Arithmetic (DJ, LMdM), pp. 338–353.

CSL-2011-TatsutaB #commutative

Non-Commutative Infinitary Peano Arithmetic (MT, SB), pp. 538–552.

ICLP-J-2011-VoetsS #analysis #integer #logic programming #source code

Non-termination analysis of logic programs with integer arithmetics (DV, DDS), pp. 521–536.

VMCAI-2011-BrilloutKRW #quantifier

Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (AB, DK, PR, TW), pp. 88–102.

STOC-2010-Raz #bound

Tensor-rank and lower bounds for arithmetic formulas (RR), pp. 659–666.

LATA-2010-MarschallR #algorithm #analysis #automaton #pattern matching #probability

Exact Analysis of Horspool’s and Sunday’s Pattern Matching Algorithms with Probabilistic Arithmetic Automata (TM, SR), pp. 439–450.

ICPR-2010-AngGLLNC #human-computer #interface

A Brain-Computer Interface for Mental Arithmetic Task from Single-Trial Near-Infrared Spectroscopy Brain Signals (KKA, CG, KL, JQL, SN, BC), pp. 3764–3767.

IJCAR-2010-BrilloutKRW #calculus #quantifier

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic (AB, DK, PR, TW), pp. 384–399.

IJCAR-2010-MaricJ #named #reduction

URBiVA: Uniform Reduction to Bit-Vector Arithmetic (FM, PJ), pp. 346–352.

TACAS-2009-LerouxP #named

TaPAS: The Talence Presburger Arithmetic Suite (JL, GP), pp. 182–185.

LATA-2009-Salimov #complexity #infinity #word

Constructing Infinite Words of Intermediate Arithmetical Complexity (PVS), pp. 696–701.

SAC-2009-ZhangLZZZZ #first-order #linear #optimisation

Optimizing techniques for saturated arithmetic with first-order linear recurrence (WZ, LL, CZ, HZ, BZ, CZ), pp. 1883–1889.

CADE-2009-BorrallerasLNRR #linear #polynomial #satisfiability

Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic (CB, SL, RNM, ERC, AR), pp. 294–305.

CADE-2009-MaLZ #constraints #linear

Volume Computation for Boolean Combination of Linear Arithmetic Constraints (FM, SL, JZ), pp. 453–468.

CAV-2009-JhaLS #named #performance #smt

Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic (SJ, RL, SAS), pp. 668–674.

CAV-2009-Monniaux #float #linear #on the #using

On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure (DM), pp. 570–583.

CSL-2009-Berger #induction #proving

From Coinductive Proofs to Exact Real Arithmetic (UB), pp. 132–146.

TLCA-2009-AschieriB #interactive

Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1 (FA, SB), pp. 20–34.

DAC-2008-PangR #fixpoint #optimisation

Optimizing imprecise fixed-point arithmetic circuits specified by Taylor Series through arithmetic transform (YP, KR), pp. 397–402.

DAC-2008-QianR #logic #polynomial #probability #robust #synthesis

The synthesis of robust polynomial arithmetic with stochastic logic (WQ, MDR), pp. 648–653.

DATE-2008-VermaBI #design #latency #paradigm

Variable Latency Speculative Addition: A New Paradigm for Arithmetic Circuit Design (AKV, PB, PI), pp. 1250–1255.

DATE-2008-ZezzaM #implementation

VLSI implementation of SISO arithmetic decoders for joint source channel coding (SZ, GM), pp. 1075–1078.

SAS-2008-Leroux #automaton

Convex Hull of Arithmetic Automata (JL), pp. 47–61.

STOC-2008-DeKSS #composition #integer #multi #performance #using

Fast integer multiplication using modular arithmetic (AD, PPK, CS, RS), pp. 499–506.

STOC-2008-DvirSY #bound #trade-off

Hardness-randomness tradeoffs for bounded depth arithmetic circuits (ZD, AS, AY), pp. 741–748.

STOC-2008-Raz #bound

Elusive functions and lower bounds for arithmetic circuits (RR), pp. 711–720.

FLOPS-2008-Julien #induction #integer #using

Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base (NJ), pp. 48–63.

FLOPS-2008-KiselyovBFS #declarative

Pure, Declarative, and Constructive Arithmetic Relations (Declarative Pearl) (OK, WEB, DPF, CcS), pp. 64–80.

CAV-2008-MagillTLT #named #reasoning

THOR: A Tool for Reasoning about Shape and Arithmetic (SM, MHT, PL, YKT), pp. 428–432.

CAV-2008-PiskacK #linear

Linear Arithmetic with Stars (RP, VK), pp. 268–280.

CAV-2008-WienandWSKG #algebra #approach #correctness #proving

An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths (OW, MW, DS, WK, GMG), pp. 473–486.

CSL-2008-Berardid #calculus

A Calculus of Realizers for EM1 Arithmetic (Extended Abstract) (SB, Ud), pp. 215–229.

CSL-2008-BeyersdorffM #bound

A Tight Karp-Lipton Collapse Result in Bounded Arithmetic (OB, SM), pp. 199–214.

CSL-2008-Eisinger #automaton #bound #integer #linear

Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic (Extended Abstract) (JE), pp. 431–445.

CSL-2008-PiskacK #bound #linear

Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars (RP, VK), pp. 124–138.

RTA-2008-KobayashiO #automaton

Tree Automata for Non-linear Arithmetic (NK, HO), pp. 291–305.

SAT-2008-FaureNOR #formal method #linear #satisfiability

SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers (GF, RN, AO, ERC), pp. 77–90.

CASE-2007-BogdanKFD #analysis #design #fuzzy

Fuzzy Arithmetic-based Stability Analysis and Design of Fuzzy Controller (SB, ZK, IF, ID), pp. 968–973.

DAC-2007-BriskVIP #performance

Enhancing FPGA Performance for Arithmetic Circuits (PB, AKV, PI, HPA), pp. 334–337.

DAC-2007-PuttaswamyL #3d #scalability

Scalability of 3D-Integrated Arithmetic Units in High-Performance Microprocessors (KP, GHL), pp. 622–625.

DAC-2007-VermaBI #composition #heuristic

Progressive Decomposition: A Heuristic to Structure Arithmetic Circuits (AKV, PB, PI), pp. 404–409.

TACAS-2007-BryantKOSSB #abstraction

Deciding Bit-Vector Arithmetic with Abstraction (REB, DK, JO, SAS, OS, BAB), pp. 358–372.

SAS-2007-GoubaultP #approximate

Under-Approximations of Computations in Real Numbers Based on Generalized Affine Arithmetic (EG, SP), pp. 137–152.

SAS-2007-MagillBCC #analysis

Arithmetic Strengthening for Shape Analysis (SM, JB, EMC, BC), pp. 419–436.

SAS-2007-Martel #semantics

Semantics-Based Transformation of Arithmetic Expressions (MM), pp. 298–314.

SAS-2007-SimonK #integer

Taming the Wrapping of Integer Arithmetic (AS, AK), pp. 121–136.

STOC-2007-Shpilka #multi

Interpolation of depth-3 arithmetic circuits with two multiplication gates (AS), pp. 284–293.

CADE-2007-KuncakR #algebra #performance #satisfiability #towards

Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic (VK, MCR), pp. 215–230.

CAV-2007-BeckerDEK #constraints #integer #linear #named

LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals (BB, CD, JE, FK), pp. 307–310.

CSL-2007-KorovinV #calculus #linear

Integrating Linear Arithmetic into Superposition Calculus (KK, AV), pp. 223–237.

TLCA-2007-Berardi #game studies #semantics

Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves (SB), pp. 23–38.

TLCA-2007-DavidN #calculus #equation #normalisation #proving #recursion

An Arithmetical Proof of the Strong Normalization for the λ -Calculus with Recursive Equations on Types (RD, KN), pp. 84–101.

DAC-2006-VermaI #architecture #automation #towards

Towards the automatic exploration of arithmetic-circuit architectures (AKV, PI), pp. 445–450.

DATE-2006-HosangadiFK #optimisation #using

Optimizing high speed arithmetic circuits using three-term extraction (AH, FF, RK), pp. 1294–1299.

DATE-2006-ShekharKE #equivalence #multi #verification

Equivalence verification of arithmetic datapaths with multiple word-length operands (NS, PK, FE), pp. 824–829.

ESOP-2006-GulwaniT #abstraction #linear

Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions (SG, AT), pp. 279–293.

SAS-2006-CalcagnoDOY #abstraction #pointer #reachability

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic (CC, DD, PWO, HY), pp. 182–203.

CIAA-2006-Luttenberger #analysis #integer #reachability #source code

Reachability Analysis of Procedural Programs with Affine Integer Arithmetic (ML), pp. 281–282.

ICALP-v1-2006-DotyLN #finite

Finite-State Dimension and Real Arithmetic (DD, JHL, SN), pp. 537–547.

SAC-2006-AltLM #linear #on the #probability #problem #using

On the numerical solution to linear problems using stochastic arithmetic (RA, JLL, SM), pp. 1635–1639.

LCTES-2006-Mine #analysis #c #embedded #pointer #source code

Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics (AM), pp. 54–63.

CAV-2006-DutertreM #performance

A Fast Linear-Arithmetic Solver for DPLL(T) (BD, LMdM), pp. 81–94.

IJCAR-2006-GregoireT #composition #functional #library #scalability

A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers (BG, LT), pp. 423–437.

DAC-2005-LeeGML #named #optimisation

MiniBit: bit-width optimization via affine arithmetic (DUL, AAG, OM, WL), pp. 837–840.

DAC-2005-WedlerSK #normalisation

Normalization at the arithmetic bit level (MW, DS, WK), pp. 457–462.

ESOP-2005-Muller-OlmS #analysis #composition

Analysis of Modular Arithmetic (MMO, HS), pp. 46–60.

FoSSaCS-2005-BozgaI #decidability #on the

On Decidability Within the Arithmetic of Addition and Divisibility (MB, RI), pp. 425–439.

TACAS-2005-BozzanoBCJRSS #incremental #linear #logic #satisfiability

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic (MB, RB, AC, TAJ, PvR, SS, RS), pp. 317–333.

ESEC-FSE-2005-RenierisRR

Arithmetic program paths (MR, SR, SPR), pp. 90–98.

CADE-2005-KuncakNR #algebra #algorithm

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic (VK, HHN, MCR), pp. 260–277.

CADE-2005-McLaughlinH

A Proof-Producing Decision Procedure for Real Arithmetic (SM, JH), pp. 295–314.

CSL-2005-Kolokolova #bound

Closure Properties of Weak Systems of Bounded Arithmetic (AK), pp. 369–383.

ICLP-2005-Maher #abduction #constraints #linear

Abduction of Linear Arithmetic Constraints (MJM), pp. 174–188.

RTA-2005-DowekW #modulo theories

Arithmetic as a Theory Modulo (GD, BW), pp. 423–437.

SAT-2005-SheiniS #integer #linear #logic #satisfiability #scalability

A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic (HMS, KAS), pp. 241–256.

TLCA-2005-DavidN #normalisation #proving #symmetry #λ-calculus #μ-calculus

Arithmetical Proofs of Strong Normalization Results for the Symmetric λμ-Calculus (RD, KN), pp. 162–178.

VMCAI-2005-Feret #abstract domain #geometry

The Arithmetic-Geometric Progression Abstract Domain (JF), pp. 42–58.

DATE-v1-2004-FlottesPR #testing

An Arithmetic Structure for Test Data Horizontal Compression (MLF, RP, BR), pp. 428–435.

DATE-v1-2004-GrimmHW #refinement

Refinement of Mixed-Signal Systems with Affine Arithmetic (CG, WH, KW), pp. 372–377.

DATE-v1-2004-WedlerSK #reasoning #satisfiability

Arithmetic Reasoning in DPLL-Based SAT Solving (MW, DS, WK), pp. 30–35.

ITiCSE-2004-Waraich #education #logic #using

Using narrative as a motivating device to teach binary arithmetic and logic gates (AW), pp. 97–101.

SAS-2004-GulwaniN04a #analysis #linear

Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions (SG, GCN), pp. 328–343.

IFM-2004-BeckertS #data type #integer #refinement #verification

Software Verification with Integrated Data Type Refinement for Integer Arithmetic (BB, SS), pp. 207–226.

SAC-2004-NehabP

Schemata Theory for the real coding and arithmetical operators (DFN, MACP), pp. 1006–1012.

SAC-2004-TangMC #embedded #fixpoint #implementation #mobile #performance #using #verification

Efficient implementation of fingerprint verification for mobile embedded systems using fixed-point arithmetic (TYT, YSM, KCC), pp. 821–825.

CC-2004-RedwineR #integer

Widening Integer Arithmetic (KR, NR), pp. 232–249.

CAV-2004-BartzisB #automaton

Widening Arithmetic Automata (CB, TB), pp. 321–333.

CAV-2004-KroeningOSS #satisfiability

Abstraction-Based Satisfiability Solving of Presburger Arithmetic (DK, JO, SAS, OS), pp. 308–320.

CSL-2004-Skelley #bound #higher-order

A Third-Order Bounded Arithmetic Theory for PSPACE (AS), pp. 340–354.

LICS-2004-AkamaBHK

An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles (YA, SB, SH, UK), pp. 192–201.

LICS-2004-CookT

The Strength of Replacement in Weak Arithmetic (SAC, NT), pp. 256–264.

LICS-2004-Klaedtke #automaton #on the

On the Automata Size for Presburger Arithmetic (FK), pp. 110–119.

DAC-2003-FangRPC #modelling #performance #static analysis #towards

Toward efficient static analysis of finite-precision effects in DSP applications via affine arithmetic modeling (CFF, RAR, MP, TC), pp. 496–501.

DATE-2003-KimSLLNN #data flow #distributed #graph

Distributed Synchronous Control Units for Dataflow Graphs under Allocation of Telescopic Arithmetic Units (EK, HS, JGL, DIL, HN, TN), pp. 10276–10281.

TACAS-2003-BartzisB #bound #constraints #performance

Construction of Efficient BDDs for Bounded Arithmetic Constraints (CB, TB), pp. 394–408.

TACAS-2003-BerezinGD #linear #online

An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic (SB, VG, DLD), pp. 521–536.

STOC-2003-SauerhoffW #bound #graph #integer #multi #trade-off

Time-space tradeoff lower bounds for integer multiplication and graphs of arithmetic functions (MS, PW), pp. 186–195.

CADE-2003-GulwaniN #random

A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols (SG, GCN), pp. 167–181.

CADE-2003-ManoliosV #algorithm

Algorithms for Ordinal Arithmetic (PM, DV), pp. 243–257.

CSL-2003-HitchcockLT #complexity

The Arithmetical Complexity of Dimension and Randomness (JMH, JHL, ST), pp. 241–254.

DAC-2002-ChangC #implementation #self #verification

Self-referential verification of gate-level implementations of arithmetic circuits (YTC, KTC), pp. 311–316.

DAC-2002-UmK #synthesis

Layout-aware synthesis of arithmetic circuits (JU, TK), pp. 207–212.

PODS-2002-AfratiLM #query #using

Answering Queries Using Views with Arithmetic Comparisons (FNA, CL, PM), pp. 209–220.

CIAA-2002-BartzisB #automation #constraints #verification

Automata-Based Representations for Arithmetic Constraints in Automated Verification (CB, TB), pp. 282–288.

IFM-2002-AkbarpourDT #fixpoint #formal method

Formalization of Cadence SPW Fixed-Point Arithmetic in HOL (BA, AD, ST), pp. 185–204.

AFP-2002-BirdG02

Arithmetic Coding with Folds and Unfolds (RSB, JG), pp. 1–26.

IFL-2002-LindahlS #compilation #float

Unboxed Compilation of Floating Point Arithmetic in a Dynamically Typed Language Environment (TL, KFS), pp. 134–149.

CAV-2002-BryantLS #logic #modelling #using #verification

Modeling and Verifying Systems Using a Logic of Counter Arithmetic with λ Expressions and Uninterpreted Functions (REB, SKL, SAS), pp. 78–92.

ICLP-2002-BoigelotW #automaton #bibliography #constraints #finite #perspective #representation

Representing Arithmetic Constraints with Finite Automata: An Overview (BB, PW), pp. 1–19.

DATE-2001-DasguptaCNKC #abstraction #component #linear

Abstraction of word-level linear arithmetic functions from bit-level component descriptions (PD, PPC, AN, SK, AC), pp. 4–8.

POPL-2001-Gil #type system

Subtyping arithmetical types (JYG), pp. 276–289.

CAV-2001-MoriokaKY #algorithm #performance #towards #verification

Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m) (SM, YK, TY), pp. 465–477.

CSL-2001-Marion

Actual Arithmetic and Feasibility (JYM), pp. 115–129.

IJCAR-2001-BoigelotJW #automaton #integer #linear #on the

On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables (BB, SJ, PW), pp. 611–625.

TLCA-2001-Hofmann #behaviour #bound #complexity #memory management #type system

From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour (MH0), pp. 2–3.

DAC-2000-HuangC #composition #constraints

Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques (CYH, KTC), pp. 118–123.

DAC-2000-UmKL #fine-grained #optimisation #power management #synthesis

A fine-grained arithmetic optimization technique for high-performance/low-power data path synthesis (JU, TK, CLL), pp. 98–103.

DATE-2000-SosnowskiB #testing

Testing Arithmetic Coprocessor in System Environment (JS, TB), p. 752.

TACAS-2000-WolperB #automaton #constraints #linear #on the

On the Construction of Automata from Linear Arithmetic Constraints (PW, BB), pp. 1–19.

WLC-2000-AvgustinovichFF #complexity #infinity #word

Arithmetical Complexity of Infinite Words (SVA, DFDF, AEF), pp. 51–62.

POPL-2000-Hickey #constraints #theorem proving

Analytic Constraint Solving and Interval Arithmetic (TJH), pp. 338–351.

CSL-2000-Blumensath #bound #complexity

Bounded Arithmetic and Descriptive Complexity (AB), pp. 232–246.

DAC-1999-ErcegovacKP #behaviour #multi #optimisation #power management #precise #synthesis #using

Low-Power Behavioral Synthesis Optimization Using Multiple Precision Arithmetic (MDE, DK, MP), pp. 568–573.

DATE-1999-HuhnSKL #verification

Verifying Imprecisely Working Arithmetic Circuits (MH, KS, TK, GL), p. 65–?.

ICALP-1999-AllenderABDL #bound

Bounded Depth Arithmetic Circuits: Counting and Closure (EA, AA, DAMB, SD, HL), pp. 149–158.

ICALP-1999-EdalatK #integration

Numerical Integration with Exact Real Arithmetic (AE, MK), pp. 90–104.

LICS-1999-Johannsen #bound #problem

Weak Bounded Arithmetic, the Diffie-Hellman Problem and Constable’s Class K (JJ), pp. 268–274.

DAC-1998-BarrettDL

A Decision Procedure for Bit-Vector Arithmetic (CWB, DLD, JRL), pp. 522–527.

DAC-1998-KimJT #optimisation #using

Arithmetic Optimization Using Carry-Save-Adders (TK, WJ, SWKT), pp. 433–438.

FoSSaCS-1998-Heckmann #integer #linear

The Appearance of Big Integers in Exact Real Arithmetic Based on Linear Fractional Transformations (RH), pp. 172–188.

STOC-1998-GrigorievK #bound #exponential

An Exponential Lower Bound for Depth 3 Arithmetic Circuits (DG, MK), pp. 577–582.

ICALP-1998-BoigelotRW #automaton #integer #on the

On the Expressiveness of Real and Integer Arithmetic Automata (Extended Abstract) (BB, SR, PW), pp. 152–163.

CAV-1998-ComonJ #analysis #automaton #multi #safety

Multiple Counters Automata, Safety Analysis and Presburger Arithmetic (HC, YJ), pp. 268–279.

DAC-1997-SudarsanamLD #analysis #architecture #evaluation

Analysis and Evaluation of Address Arithmetic Capabilities in Custom DSP Architectures (AS, SYL, SD), pp. 287–292.

EDTC-1997-MignotteP #scheduling #using

Scheduling using mixed arithmetic: an ILP formulation (AM, OP), p. 621.

CAV-1997-BultanGP #infinity #model checking #using

Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic (TB, RG, WP), pp. 400–411.

CSL-1997-Staiger #higher-order #monad

Rich ω-Words and Monadic Second-Order Arithmetic (LS), pp. 478–490.

LICS-1997-PottsEE #semantics

Semantics of Exact Real Arithmetic (PJP, AE, MHE), pp. 248–257.

RTA-1997-ContejeanMR #term rewriting

Rewrite Systems for Natural, Integral, and Rational Arithmetic (EC, CM, LR), pp. 98–112.

DAC-1996-TsaiM #logic #multi #synthesis

Multilevel Logic Synthesis for Arithmetic Functions (CCT, MMS), pp. 242–247.

ICALP-1996-Razborov #bound #independence #proving

Lower Bounds for Propositional Proofs and Independence Results in Bounded Arithmetic (AAR), pp. 48–62.

CAV-1996-Fujita #verification

Verification of Arithmetic Circuits by Comparing Two Similar Circuits (MF), pp. 159–168.

DAC-1995-BryantC #diagrams #verification

Verification of Arithmetic Circuits with Binary Moment Diagrams (REB, YAC), pp. 535–541.

DAC-1995-Kimura #verification

Residue BDD and Its Application to the Verification of Arithmetic Circuits (SK), pp. 542–545.

DAC-1995-ZhouB #canonical #equivalence

Equivalence Checking of Datapaths Based on Canonical Arithmetic Expressions (ZZ, WB), pp. 546–551.

SAS-1995-WolperB #approach #constraints

An Automata-Theoretic Approach to Presburger Arithmetic Constraints (Extended Abstract) (PW, BB), pp. 21–32.

CAV-1995-Bryant #multi #verification

Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract) (REB), pp. 1–3.

RTA-1995-WaltersZ #integer #term rewriting

Rewrite Systems for Integer Arithmetic (HRW, HZ), pp. 324–338.

PLILP-1994-MetzemakersMSS #performance #using

Improving Arithmetic Performance using Fine-Grain Unfolding (TM, AM, DS, RS), pp. 324–339.

CADE-1994-FribourgP #bottom-up #constraints #datalog #evaluation #source code

Bottom-up Evaluation of Datalog Programs with Arithmetic Constraints (LF, MVP), pp. 311–325.

ILPS-1994-MarriottS #approximate #constraints #interactive #linear

Approximating Interaction between Linear Arithmetic Constraints (KM, PJS), pp. 571–585.

ILPS-1994-MichaylovP #compilation #constraints #linear #logic programming #optimisation #source code

Optimizing Compilation of Linear Arithmetic in a Class of Constraint Logic Programs (SM, BP), pp. 586–600.

STOC-1993-AllenderJ #commutative #reduction

Depth reduction for noncommutative arithmetic circuits (EA, JJ), pp. 515–522.

STOC-1992-BshoutyHH #learning

Learning Arithmetic Read-Once Formulas (NHB, TRH, LH), pp. 370–381.

WSA-1992-AmeurCFG #abstract interpretation #float

An Application of Abstract Interpretation to Floating Point Arithmetic (YAA, PC, JJF, AG), pp. 205–212.

AdaEurope-1992-BrosgolEE #ada

Decimal Arithmetic in Ada (BMB, RIE, DEE), pp. 138–149.

LICS-1992-Fribourg #recursion

Mixing List Recursion and Arithmetic (LF), pp. 419–429.

AdaEurope-1991-Gudenberg #ada #parallel

Modellin SIMD — Type Parallel Arithmetic Operations in Ada (JWvG), pp. 110–124.

RTA-1991-CohenW #performance #representation #term rewriting

An Efficient Representation of Arithmetic for Term Rewriting (DC, PW), pp. 240–251.

PLILP-1990-Fribourg #execution #prolog

A New Presburger Arithmetic Decision Procedure Based on Extended Prolog Execution (LF), pp. 174–188.

CSL-1990-CantoneCS #problem #set

Decision Problems for Tarski and Presburger Arithmetics Extended With Sets (DC, VC, JTS), pp. 95–109.

CSL-1990-Pudlak #bound #theorem

Ramsey’s Theorem in Bounded Arithmetic (PP), pp. 308–317.

STOC-1989-CookU #functional

Functional Interpretations of Feasibly Constructive Arithmetic (Extended Abstract) (SAC, AU), pp. 107–112.

CSL-1989-KrajicekP #modelling

Propositional Provability and Models of Weak Arithmetic (JK, PP), pp. 193–210.

NACLP-1989-LassezHM #constraints #linear

Simplification and Elimination of Redundant Linear Arithmetic Constraints (JLL, TH, KM), pp. 37–51.

RTA-1989-Vorobyov #induction

Conditional Rewrite Rule Systems with Built-In Arithmetic and Induction (SGV), pp. 492–512.

LFP-1988-Vuillemin

Exact Real Computer Arithmetic with Continued Fractions (JV), pp. 14–27.

JICSCP-1988-AptB88 #classification #modelling #source code

Arithmetic Classification of Perfect Models of Stratified Programs (KRA, HAB), pp. 765–779.

LICS-1988-Vorobyov #on the #term rewriting

On the Arithmetic Inexpressiveness of Term Rewriting Systems (SGV), pp. 212–217.

STOC-1987-CoppersmithW #matrix #multi

Matrix Multiplication via Arithmetic Progressions (DC, SW), pp. 1–6.

STOC-1987-Vaidya #algorithm #linear #programming

An Algorithm for Linear Programming which Requires O(((m+n)n^2 + (m+n)^1.5 n)L) Arithmetic Operations (PMV), pp. 29–38.

POPL-1987-BernsteinJR #parallel #scheduling

Scheduling Arithmetic and Load Operations in Parallel with No Spilling (DB, JMJ, MR), pp. 263–273.

STOC-1986-Kosaraju #evaluation #parallel

Parallel Evaluation of Division-Free Arithmetic Expressions (SRK), pp. 231–239.

LFP-1986-BoehmCRO #case study #higher-order #programming

Exact Real Arithmetic: A Case Study in Higher Order Programming (HJB, RC, MR, MJO), pp. 162–173.

STOC-1985-Buss #bound #polynomial

The Polynomial Hierarchy and Fragments of Bounded Arithmetic (Extended Abstract) (SRB), pp. 285–290.

POPL-1985-BernsteinPR #memory management #parallel #scheduling

Optimal Scheduling of Arithmetic Operations in Parallel with Memory Accesses (DB, RYP, MR), pp. 325–333.

STOC-1984-Alt #comparison

Comparison of Arithmetic Functions with Respect to Boolean Circuit Depth (Extended Abstract) (HA), pp. 466–470.

DAC-1981-AtkinsLO #bibliography #design

Overview of an Arithmetic Design System (DEA, WL, SO), pp. 314–321.

STOC-1981-JosephY #modelling #performance #polynomial #source code

Fast Programs for Initial Segments and Polynomial Time Computation in Weak Models of Arithmetic (Preliminary Abstract) (DJ, PY), pp. 55–61.

ICALP-1981-IbarraLM #complexity #on the

On the Complexity of Simple Arithmetic Expressions (OHI, BSL, SM), pp. 294–304.

STOC-1980-BrentK #complexity

The Chip Complexity of Binary Arithmetic (RPB, HTK), pp. 190–200.

STOC-1979-ODonnell #independence #programming language #theorem

A Programming Language Theorem Which Is Independent of Peano Arithmetic (MO), pp. 176–188.

STOC-1978-Dowd #proving #representation

Propositional Representation of Arithmetic Proofs (Preliminary Version) (MD), pp. 246–252.

STOC-1978-ReddyL #bound #quantifier

Presburger Arithmetic with Bounded Quantifier Alternation (CRR, DWL), pp. 320–325.

ICALP-1978-Harel #logic #source code

Arithmetical Completeness in Logics of Programs (DH), pp. 268–288.

DAC-1974-WeberS #algorithm #integer

An integer arithmetic path expansion algorithm (TAW, DGS), pp. 62–69.

STOC-1973-Oppen #bound

Elementary Bounds for Presburger Arithmetic (DCO), pp. 34–37.

STOC-1972-Horowitz #algorithm

Algorithms for Rational Function Arithmetic Operations (EH), pp. 108–118.

STOC-1969-Avizienis #complexity #on the #problem

On the Problem of Computational Time and Complexity of Arithmetic Functions (AA), pp. 255–258.