float

---

float

Tag #float

115 papers:

POPL-2020-ZouZXFZS #detection #fault

Detecting floating-point errors via atomic conditions (DZ, MZ, YX, ZF, LZ0, ZS), p. 27.

FM-2019-MoscatoTFM #algorithm #implementation

Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm (MMM, LT, MAF, CAM), pp. 21–37.

OOPSLA-2019-Adams

Ryū revisited: printf floating point conversion (UA), p. 23.

PLDI-2019-FuS #analysis #effectiveness

Effective floating-point analysis via weak-distance minimization (ZF, ZS), pp. 439–452.

POPL-2019-YiCMJ #automation #fault #library #performance

Efficient automated repair of high floating-point errors in numerical libraries (XY, LC, XM, TJ), p. 29.

ASE-2019-Laguna #detection #exception #gpu #named

FPChecker: Detecting Floating-Point Exceptions in GPU Applications (IL), pp. 1126–1129.

ESEC-FSE-2019-LiewCDS #constraints #fuzzing #using

Just fuzz it: solving floating-point constraints using coverage-guided fuzzing (DL, CC, AFD, JRS), pp. 521–532.

CADE-2019-TrentinS #formal method #optimisation

Optimization Modulo the Theory of Floating-Point Numbers (PT, RS), pp. 550–567.

CAV-2019-BrainNPRBT

Invertibility Conditions for Floating-Point Formulas (MB, AN, MP, AR, CWB, CT), pp. 116–136.

FM-2018-BeckerPDT #analysis #optimisation #tool support

Combining Tools for Optimization and Analysis of Floating-Point Computations (HB, PP, ED, ZT), pp. 355–363.

FM-2018-TitoloMMDB #algorithm #implementation

A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (LT, MMM, CAM, AD, FB), pp. 364–381.

LOPSTR-2018-TitoloMFM #source code #testing

Eliminating Unstable Tests in Floating-Point Programs (LT, CAM, MAF, MMM), pp. 169–183.

PLDI-2018-Adams #named #performance #string

Ryū: fast float-to-string conversion (UA), pp. 270–282.

PLDI-2018-Sanchez-SternPL #fault

Finding root causes of floating point error (ASS, PP, SL, ZT), pp. 256–269.

SAS-2018-JacqueminPV #analysis #bound #fault

A Reduced Product of Absolute and Relative Error Bounds for Floating-Point Analysis (MJ, SP, FV), pp. 223–242.

IJCAR-2018-ZeljicBWR #approximate #using

Exploring Approximations for Floating-Point Arithmetic Using UppSAT (AZ, PB, CMW, PR), pp. 246–262.

VMCAI-2018-TitoloFMM #abstract interpretation #analysis #fault #framework #source code

An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs (LT, MAF, MMM, CAM), pp. 516–537.

PLDI-2017-FuS #programming

Achieving high coverage for floating-point code via unconstrained programming (ZF, ZS), pp. 306–319.

POPL-2017-ChiangBBSGR

Rigorous floating-point mixed-precision tuning (WFC, MB, IB, AS, GG, ZR), pp. 300–315.

ASE-2017-LiewSCDZW #case study #execution #programming #symbolic computation

Floating-point symbolic execution: a case study in n-version programming (DL, DS, CC, AFD, RZ, KW), pp. 601–612.

CAV-2017-ConchonIJMF #reasoning #smt

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT (SC, MI, KJ, GM, CF), pp. 419–435.

VMCAI-2017-GuW #analysis #source code #using

Stabilizing Floating-Point Programs Using Provenance Analysis (YG, TW), pp. 228–245.

FM-2016-Mukherjee0GKM #c #equivalence

Equivalence Checking of a Floating-Point Unit Against a High-Level C Model (RM, SJ0, AG, DK, TM), pp. 551–558.

PLDI-2016-LeeSA #verification

Verifying bit-manipulations of floating-point (WL0, RS0, AA), pp. 70–84.

POPL-2016-AndryscoJL #performance

Printing floating-point numbers: a faster, always correct method (MA, RJ, SL), pp. 555–567.

SAS-2016-MauricaMP #linear #on the #problem #ranking

On the Linear Ranking Problem for Simple Floating-Point Loops (FM, FM, ÉP), pp. 300–316.

SAS-2016-MenendezNG #automation #named #optimisation #verification

Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM (DM, SN, AG), pp. 317–337.

FSE-2016-Quan #execution #source code #symbolic computation

Hotspot symbolic execution of floating-point programs (MQ), pp. 1112–1114.

FSE-2016-WangZHXZ0 #detection #fault

Detecting and fixing precision-specific operations for measuring floating-point errors (RW, DZ, XH, YX, LZ0, GH0), pp. 619–630.

ICSE-2016-Rubio-Gonzalez0 #analysis #precise #using

Floating-point precision tuning using blame analysis (CRG, CN0, BM, KS, JD, WK, CI, WL, DHB, DH), pp. 1074–1085.

ESOP-2016-KawabataI #adaptation #approach #lazy evaluation #refinement

Improving Floating-Point Numbers: A Lazy Approach to Adaptive Accuracy Refinement for Numerical Computations (HK, HI), pp. 390–418.

CAV-2016-FuS #named #performance #satisfiability

XSat: A Fast Floating-Point Satisfiability Solver (ZF, ZS), pp. 187–209.

ICTSS-2016-CollavizzaMR #source code

Searching Critical Values for Floating-Point Programs (HC, CM, MR), pp. 209–217.

FM-2015-SolovyevJRG #estimation #fault

Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions (AS, CJ, ZR, GG), pp. 532–550.

OOPSLA-2015-LeeBZZVG #assessment #named #runtime

RAIVE: runtime assessment of floating-point instability by vectorization (WCL, TB, YZ, XZ, KV, RG), pp. 623–638.

PLDI-2015-PanchekhaSWT #automation

Automatically improving accuracy for floating point expressions (PP, ASS, JRW, ZT), pp. 1–11.

ICSE-v1-2015-ZouWXZSM #algorithm #detection #search-based

A Genetic Algorithm for Detecting Significant Floating-Point Inaccuracies (DZ, RW, YX, LZ, ZS, HM), pp. 529–539.

DAC-2015-TziantzioulisGF #correlation #fault #integer #named

b-HiVE: a bit-level history-based error model with value correlation for voltage-scaled integer and floating point units (GT, AMG, SMF, NH, SOM, SP), p. 6.

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

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

CHI-PLAY-2014-ChenBRGM #concept #education #interactive #simulation

ASPECT sinking and floating: an interactive playable simulation for teaching buoyancy concepts (STC, DB, MR, RG, JM), pp. 327–330.

CHI-PLAY-2014-ChenBRGM14a #named #student

ASPECT: sinking and floating haptics for elementary school students (STC, DB, MR, RG, JM), pp. 405–406.

PLDI-2014-Schkufza0A #optimisation #precise #probability #source code

Stochastic optimization of floating-point programs with tunable precision (ES, RS, AA), p. 9.

ASPLOS-2014-LuponGMSMSD #hardware #multi

Speculative hardware/software co-designed floating-point multiply-add fusion (ML, EG, GM, SS, RM, KS, DRD), pp. 623–638.

DAC-2014-KrautzPAKPB #automation #verification

Automatic Verification of Floating Point Units (UK, VP, AA, SK, SP, TB), p. 6.

DATE-2014-LeeserMRW #effectiveness #reasoning

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

PPoPP-2014-ChiangGRS #fault #performance

Efficient search for inputs causing high floating-point errors (WFC, GG, ZR, AS), pp. 43–52.

SMT-2014-Melquiond #algorithm #automation #verification

Automating the Verification of Floating-Point Algorithms (GM), p. 63.

VMCAI-2014-Romano #integer #testing

Practical Floating-Point Tests with Integer Code (AR), pp. 337–356.

OOPSLA-2013-BaoZ #detection #execution #on the fly #problem

On-the-fly detection of instability problems in floating-point program execution (TB, XZ), pp. 817–832.

POPL-2013-BarrVLS #automation #detection #exception

Automatic detection of floating-point exceptions (ETB, TV, VL, ZS), pp. 549–560.

SAS-2013-BrainDGHK #source code #verification

Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL (MB, VD, AG, LH, DK), pp. 412–432.

DATE-2013-ZhaiYZ #algorithm #random

GPU-friendly floating random walk algorithm for capacitance extraction of VLSI interconnects (KZ, WY, HZ), pp. 1661–1666.

ICST-2013-BagnaraCGG #generative #source code #testing

Symbolic Path-Oriented Test Data Generation for Floating-Point Programs (RB, MC, RG, AG), pp. 1–10.

PLDI-2012-BenzHH #problem #program analysis

A dynamic program analysis to find floating-point accuracy problems (FB, AH, SH), pp. 453–462.

QAPL-2012-GazeauMP #analysis #robust #source code

A non-local method for robustness analysis of floating point programs (IG, DM, CP), pp. 63–76.

DATE-2012-MarinhoNPP #analysis #scheduling

Preemption delay analysis for floating non-preemptive region scheduling (JM, VN, SMP, IP), pp. 497–502.

ICST-2012-DanH #analysis #comparison #mutation testing #semantics

Semantic Mutation Analysis of Floating-Point Comparison (HD, RMH), pp. 290–299.

ICST-2012-PonsiniMR #abstract interpretation #analysis #constraints #programming #source code

Combining Constraint Programming and Abstract Interpretation for Value Analysis of Floating-point Programs (OP, CM, MR), pp. 775–776.

SMT-2012-ConchonMRI #axiom #smt

Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers (SC, GM, CR, MI), pp. 12–21.

HCI-MIIE-2011-ShibuyaNM #diagrams #documentation #mobile #performance

An Efficient Document Browsing Method with Floating Diagram Window on Mobile Device (YS, KN, KM), pp. 101–106.

ICEIS-v2-2011-YuanL #enterprise #research #standard

The Research of Public Transport Enterprises Quota Floating Fuel — National Standard GB4353 Fuel Consumption for Passenger Vehicles in Operation Applied to the Public Transport Enterprise (YY, ML), pp. 291–296.

PLDI-2010-Loitsch #integer

Printing floating-point numbers quickly and accurately with integers (FL), pp. 233–243.

SAS-2010-Chapoutot #abstract domain

Interval Slopes as a Numerical Abstract Domain for Floating-Point Variables (AC), pp. 184–200.

ICSE-2010-KornstaedtR #development #eclipse #framework #platform

Staying afloat in an expanding sea of choices: emerging best practices for eclipse rich client platform development (AK, ER), pp. 59–67.

ICTSS-2010-LakhotiaTHH #constraints #execution #named #search-based #symbolic computation #theorem proving

FloPSy — Search-Based Floating Point Constraint Solving for Symbolic Execution (KL, NT, MH, JdH), pp. 142–157.

IJCAR-2010-AyadM #multi #source code #verification

Multi-Prover Verification of Floating-Point Programs (AA, CM), pp. 127–141.

ISSTA-2010-GodefroidK #memory management #program analysis #proving #safety

Proving memory safety of floating-point computations by combining static and dynamic program analysis (PG, JK), pp. 1–12.

ISSTA-2010-TangBLS #analysis #statistics

Perturbing numerical calculations for statistical analysis of floating-point program (in)stability (ET, ETB, XL, ZS), pp. 131–142.

HT-2009-AcottoBBPPV #named

ArsMeteo: artworks and tags floating over the planet art (EA, MB, CB, VP, FP, GV), pp. 331–332.

ICALP-v2-2009-Boldo #case study #verification

Floats and Ropes: A Case Study for Formal Numerical Program Verification (SB), pp. 91–102.

DATE-2009-GuntoroG #flexibility

A flexible floating-point wavelet transform and wavelet packet processor (AG, MG), pp. 1314–1319.

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

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

DAC-2008-ChongP #agile #generative

Rapid application specific floating-point unit generation with bit-alignment (YJC, SP), pp. 62–67.

DocEng-2007-MarriottMH #automation #documentation #multi

Automatic float placement in multi-column documents (KM, PM, NH), pp. 125–134.

DiGRA-2007-Consalvo #game studies

Visiting the Floating World: Tracing a Cultural History of Games Through Japan and America (MC).

MLDM-2007-Olvera-LopezTC #strict

Restricted Sequential Floating Search Applied to Object Selection (JAOL, JFMT, JACO), pp. 694–702.

DATE-2007-ChongP #automation #generative

Automatic application specific floating-point unit generation (YJC, SP), pp. 461–466.

PDP-2007-QianHZLZF #architecture #design #implementation #stack

Design and Implementation of Floating Point Stack on General RISC Architecture (XQ, HH, HZ, GL, JZ, DF), pp. 238–245.

SFM-2006-Harrison #proving #theorem proving #using #verification

Floating-Point Verification Using Theorem Proving (JH), pp. 211–242.

DATE-2006-MatulaM #algorithm #formal method #generative #performance #standard #traversal #verification

A formal model and efficient traversal algorithm for generating testbenches for verification of IEEE standard floating point division (DWM, LDM), pp. 1134–1138.

DATE-DF-2006-KaruriLAMK #composition #design #implementation

Design and implementation of a modular and portable IEEE 754 compliant floating-point unit (KK, RL, GA, HM, MK), pp. 221–226.

IJCAR-2006-Boldo #algorithm #proving

Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms (SB), pp. 52–66.

FM-2005-Harrison #verification

Floating-Point Verification (JH), pp. 529–532.

CAV-2005-Monniaux #analysis #composition #linear

Compositional Analysis of Floating-Point Linear Numerical Filters (DM), pp. 199–212.

DAC-2004-RoyB #algorithm #design #fixpoint #matlab

An algorithm for converting floating-point computations to fixed-point in MATLAB based FPGA design (SR, PB), pp. 484–487.

ESOP-2004-Mine #abstract domain #detection #fault #relational #runtime

Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors (AM), pp. 3–17.

PDP-2003-DaneseLLSS #precise

An Accelerator for Double Precision Floating Point Operations (GD, IDL, FL, MS, AS), p. 57–?.

IFL-2002-LindahlS #compilation

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

SAS-2002-SerebrenikS #logic programming #on the #source code #termination

On Termination of Logic Programs with Floating Point Computations (AS, DDS), pp. 151–164.

DATE-2002-DrozdLD #array #online #performance #testing

Efficient On-Line Testing Method for a Floating-Point Iterative Array Divider (AVD, MVL, JVD), p. 1127.

DATE-2002-KaivolaN #multi #verification

Formal Verification of the Pentium ® 4 Floating-Point Multiplier (RK, NN), pp. 20–27.

DATE-2002-PronathGA #design #fault

A Test Design Method for Floating Gate Defects (FGD) in Analog Integrated Circuits (MP, HEG, KA), pp. 78–83.

ESOP-2002-GoubaultMP #interpreter #precise

Asserting the Precision of Floating-Point Computations: A Simple Abstract Interpreter (EG, MM, SP), pp. 209–212.

SAS-2001-Goubault #analysis #precise

Static Analyses of the Precision of Floating-Point Operations (EG), pp. 234–259.

ASE-2001-SyD #automation #generative #integer #source code #testing

Automatic Test Data Generation for Programs with Integer and Float Variables (NTS, YD), pp. 13–21.

DATE-2001-DrozdL #online #performance #testing

Efficient on-line testing method for a floating-point adder (AVD, MVL), pp. 307–313.

DATE-2001-YildizSV #bias #integer #linear #programming

Minimizing the number of floating bias voltage sources with integer linear programming (EY, AvS, CJMV), p. 816.

ICPR-v2-2000-PingLK #detection #recognition

A Floating Feature Detector for Handwritten Numeral Recognition (ZP, CL, ACK), pp. 2553–2556.

CADE-2000-Seger #model checking #proving #theorem proving

Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice (CJHS), p. 235.

CC-1999-CilioC #c #fixpoint

Floating Point to Fixed Point Conversion of C Code (AGMC, HC), pp. 229–243.

PLDI-1998-SastryPS #execution #integer

Exploiting Idle Floating-Point Resources for Integer Execution (SSS, SP, JES), pp. 118–129.

CAV-1998-ChenB #verification

Verification of Floating-Point Adders (YAC, REB), pp. 488–499.

ICFP-1996-JonesPS #named #performance #source code

Let-floating: Moving Bindings to Give Faster Programs (SLPJ, WP, AS), pp. 1–12.

PLDI-1996-BurgerD

Printing Floating-Point Numbers Quickly and Accurately (RGB, RKD), pp. 108–116.

EDAC-1994-XueDJ #analysis #fault #probability

Probability Analysis for CMOS Floating Gate Faults (HX, CD, JAGJ), pp. 443–448.

PDP-1993-BagliettoM #parallel

Floating point computation in SIMD massively parallel computers (PB, MM), pp. 197–202.

WSA-1992-AmeurCFG #abstract interpretation

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

ASPLOS-1991-LeeKB #performance

The Floating-Point Performance of a Superscalar SPARC Processor (RLL, AYK, FAB), pp. 28–37.

PLDI-1990-Clinger #how

How to Read Floating-Point Numbers Accurately (WDC), pp. 92–101.

PLDI-1990-SteeleW #how

How to Print Floating-Point Numbers Accurately (GLSJ, JLW), pp. 112–126.

Best-of-PLDI-1990-Clinger90a #how

How to read floating point numbers accurately (with retrospective) (WDC), pp. 360–371.

Best-of-PLDI-1990-SteeleW90a #how

How to print floating-point numbers accurately (with retrospective) (GLSJ, JLW), pp. 372–389.

ASPLOS-1989-Dally

Micro-Optimization of Floating Point Operations (WJD), pp. 283–289.

ASPLOS-1989-JouppiBW #architecture

A Unified Vector/Scalar Floating-Point Architecture (NPJ, JB, DWW), pp. 134–143.

DAC-1976-WuS #algorithm

A new routing algorithm for two-sided boards with floating vias (WW, DCS), pp. 151–160.