Publications

  • [PDF] Z. Fu, “Static analysis of numerical properties in the presence of pointers,” Thèse pour le grade de Docteur PhD Thesis, INRIA, Rennes, France, 2013.
    [Bibtex]
    @PhDThesis{thesis,
    Title = "Static Analysis of Numerical Properties in the Presence of Pointers",
    Author = "Z. Fu",
    Type = "Th\`{e}se pour le grade de
    Docteur",
    School = "\'{E}cole doctorale MATISSE, Universit\'{e} de Rennes 1
    sous le sceau de l'Universit\'e Europ\'eenne de Bretagne",
    Address = "INRIA, Rennes, France",
    Month = dec,
    Year = 2013,
    Abstract = "
    The fast and furious pace of change in computing technology has become an article of faith for many. The reliability of computer-based systems crucially depends on the correctness of its computing. Can man, who created the computer, be capable of preventing machine-made misfortune? The theory of static analysis strives to achieve this ambition.
    The analysis of numerical properties of programs has been an essential research topic for static analysis. These kinds of properties are commonly modeled and handled by the concept of numerical abstract domains. Unfor- tunately, lifting these domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have been intensively studied to analyze pointer behaviors and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. The static numerical analysis is prototyped using the SOOT framework for pointer analyses and the PPL library for numerical domains. The implementation is able to analyze large Java program within several minutes.
    The second part of this thesis consists of a theoretical study of the combination of the points-to analysis with another pointer analysis providing information called must-alias. Two pointer variables must alias at some program control point if they hold equal reference whenever the control point is reached. We have developed an algorithm of quartic complexity that removes a part of redundant arcs obtained from points-to analysis using must-alias information. The algorithm is proved correct following a semantics-based formalization and the concept of bisimulation borrowed from the game theory, model checking etc. This redundancy removal is partial because we have constructed a non-trivial example showing the incompleteness of the proposed algorithm. As a conclusion, we have proved that to find an efficient and complete solution to the question raised in the part of research is an NP-hard problem. "
    }
  • [PDF] Z. Fu, “Modularly combining numeric abstract domains with points-to analysis, and a scalable static numeric analyzer for java,” in Verification, model checking, and abstract interpretation: proceedings of the 15th international conference (VMCAI), San Diego, US, 2014.
    [Bibtex]
    @Inproceedings{nump,
    Author = "Z. Fu",
    Title = "Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java",
    Booktitle = "Verification, Model Checking, and Abstract Interpretation:
    Proceedings of the 15th International Conference ({VMCAI})",
    Address = "San Diego, US",
    Editor = "K. McMillan and X. Rival",
    Publisher = "Springer-Verlag, Berlin",
    Year = 2014,
    Abstract = "This paper contributes to a new abstract domain that
    combines static numeric analysis and points-to
    analysis. One particularity of this abstract domain lies
    in its high degree of modularity, in the sense that the
    domain is constructed by reusing its combined components
    as black-boxes. This modularity dramatically eases the
    proof of its soundness and renders its algorithm
    intuitive. We have prototyped the abstract domain for
    analyzing real-world Java programs. Our experimental
    results show a tangible precision enhancement compared
    to what is possible by traditional static numeric
    analysis, and this at a cost that is comparable to the
    cost of running the numeric and pointer analyses
    separately."
    }
  • [PDF] Z. Fu, “Targeted update — aggressive memory abstraction beyond common sense and its application on static numeric analysis,” in The 23rd european symposium on programming (ESOP), Grenoble, France, 2014.
    [Bibtex]
    @Inproceedings{targetupdate,
    Author = "Z. Fu",
    Title = "Targeted Update -- Aggressive Memory Abstraction Beyond Common
    Sense and its Application on Static Numeric Analysis",
    Booktitle = "The 23rd European Symposium on Programming
    ({ESOP})",
    Address = "Grenoble, France",
    Editor = "Z. Shao",
    Publisher = "Springer-Verlag, Berlin",
    Year = 2014,
    Abstract = "Summarizing techniques are widely used in the reasoning
    of unbounded data structures. These techniques prohibit
    strong update unless certain restricted safety
    conditions are satisfied. We find that by setting and
    enforcing the analysis boundaries to a limited scope of
    program identifiers, called targets in this paper, more
    cases of strong update can be shown sound, not with
    regard to the entire heap, but with regard to the
    targets. We have implemented the analysis for inferring
    numeric properties in Java programs. The experimental
    results show a tangible precision enhancement compared
    with classical approaches while preserving high
    scalability."
    }
  • [PDF] T. Su, Z. Fu, G. Pu, J. He, and Z. Su, “Combining symbolic execution and model checking for data flow testing,” in The 37th international conference on software engineering (ICSE), Firenze, Italy, 2015.
    [Bibtex]
    @inproceedings{SuFPHS15,
    Author = "T. Su and Z. Fu and G. Pu and J. He and Z. Su",
    Title = "Combining Symbolic Execution and Model Checking for Data Flow Testing",
    Booktitle = "The 37th International Conference on Software Engineering ({ICSE})",
    Address = "Firenze, Italy",
    Year ="2015",
    Abstract="Data flow testing (DFT) focuses on the flow of data through a program. Desipte its higher fault-detection ability over other structural testing techniques, practical DFT remains a significant challenge. This paper tackles this challenge by introducing a hybrid DFT framework: (1) The core of our framework is based on Dynamic Symbolic Execution (DSE), enhanced with a novel guided path search strategy to improve testing performance; and (2) we systematically cast the DFT problem as reachability checking in software model checking to complement our DSE-based approach, yielding a practical hybrid DFT technique that combines the two approaches's respective strengths. Evaluated on both open source and industrial programs, our DSE-based approach improves DFT performance by 60~80% in terms of testing time compared with state-of-the-art search strategies, while our combined technique further reduces 40% testing time and improves data-flow coverage by 20% by eliminating infeasile test objectives. This combined approach also enables the cross-checking of each component for reliable and robust testing results."
    }
  • [PDF] Z. Fu, Z. Bai, and Z. Su, “Automated backward error analysis for numerical code,” in Object-oriented programming, systems, languages & applications (OOPSLA), Pittsburgh, Pennsylvania, United States, 2015.
    [Bibtex]
    @inproceedings{bea,
    Author = "Z. Fu and Z. Bai and Z. Su",
    Title = "Automated Backward Error Analysis for Numerical Code",
    Booktitle = "Object-Oriented Programming, Systems, Languages & Applications ({OOPSLA})",
    Year ="2015",
    Address="Pittsburgh, Pennsylvania, United States",
    Abstract="Numerical code uses floating-point arithmetic and necessarily suffers from roundoff and truncation errors. Error analysis is the process to quantify such uncertainty. Forward error analysis and backward error analysis are two popular paradigms of error analysis. Forward error analysis is intuitive, and has been explored and automated by the programming languages (PL) community. In contrast, although backward error analysis is fundamental for numerical stability and is preferred by numerical analysts, it is less known and unexplored by the PL community.
    To fill this gap, this paper presents an automated backward error analysis for numerical code to empower both numerical analysts and application developers. In addition, we use the computed backward error results to compute the condition number, an important quantity recognized by numerical analysts for measuring a function’s sensitivity to errors in the input and finite precision arithmetic. Experimental results on Intel x87 FPU instructions and widely-used GNU C Library functions demonstrate that our analysis is effective at analyzing the accuracy of floating-point programs."
    }
  • [PDF] Z. Fu and Z. Su, “XSat: a fast floating-point satisfiability solver,” in Computer aided verification (CAV), 2016.
    [Bibtex]
    @inproceedings{xsat,
    Title= "X{S}at: A Fast Floating-Point Satisfiability Solver",
    Author = "Z. Fu and Z. Su",
    booktitle="Computer Aided Verification ({CAV})",
    year={2016},
    }
  • Z. Fu and Z. Su, “Mathematical execution: A unified approach for testing numerical code,” Corr, vol. abs/1610.01133, 2016.
    [Bibtex]
    @article{me,
    author = {Zhoulai Fu and
    Zhendong Su},
    title = {Mathematical Execution: {A} Unified Approach for Testing Numerical
    Code},
    journal = {CoRR},
    volume = {abs/1610.01133},
    year = {2016},
    url = {http://arxiv.org/abs/1610.01133},
    timestamp = {Wed, 02 Nov 2016 09:51:26 +0100},
    biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/FuS16a},
    }
  • [PDF] Z. Fu and Z. Su, “Achieving high coverage for floating-point code via unconstrained programming,” in The 38th ACM SIGPLAN conference on programming language design and implementation (PLDI), 2017, to appear.
    [Bibtex]
    @inproceedings{coverme_extended,
    title={Achieving High Coverage for Floating-point Code via Unconstrained Programming},
    author={Fu, Zhoulai and Su, Zhendong},
    booktitle = {The 38th {ACM} {SIGPLAN} Conference on Programming
    Language Design and Implementation ({PLDI})},
    year={2017, to appear}
    }