research-article

Open access

Program analysis via efficient symbolic abstraction

Authors:

Charles ZhangAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue OOPSLA

Article No.: 118, Pages 1 - 32

https://doi.org/10.1145/3485495

Published: 15 October 2021 Publication History

Abstract

This paper concerns the scalability challenges of symbolic abstraction: given a formula ϕ in a logic L and an abstract domain A, find a most precise element in the abstract domain that over-approximates the meaning of ϕ. Symbolic abstraction is an important point in the space of abstract interpretation, as it allows for automatically synthesizing the best abstract transformers. However, current techniques for symbolic abstraction can have difficulty delivering on its practical strengths, due to performance issues.

In this work, we introduce two algorithms for the symbolic abstraction of quantifier-free bit-vector formulas, which apply to the bit-vector interval domain and a certain kind of polyhedral domain, respectively. We implement and evaluate the proposed techniques on two machine code analysis clients, namely static memory corruption analysis and constrained random fuzzing. Using a suite of 57,933 queries from the clients, we compare our approach against a diverse group of state-of-the-art algorithms. The experiments show that our algorithms achieve a substantial speedup over existing techniques and illustrate significant precision advantages for the clients. Our work presents strong evidence that symbolic abstraction of numeric domains can be efficient and practical for large and realistic programs.

Supplementary Material

Auxiliary Presentation Video (oopsla21main-p90-p-video.mp4)

Paper 90

Download
93.08 MB

References

[1]

2014. AFL: american fuzzy lop. http://lcamtuf.coredump.cx/afl/ Accessed: 2014

[2]

Bijan Alizadeh and Masahiro Fujita. 2009. Modular arithmetic decision procedure with auto-correction mechanism. In IEEE International High Level Design Validation and Test Workshop, HLDVT 2009, San Francisco, CA, USA, 4-6 November 2009. IEEE Computer Society, 138–145.

[3]

Dennis S. Arnon. 1988. A Bibliography of Quantifier Elimination for Real Closed Fields. J. Symb. Comput., 5, 1/2 (1988).

Digital Library

[4]

Benjamin Assarf, Ewgenij Gawrilow, Katrin Herr, Michael Joswig, Benjamin Lorenz, Andreas Paffenholz, and Thomas Rehn. 2017. Computing convex hulls and counting integer points with polymake. Math. Program. Comput., 9, 1 (2017), 1–38.

[5]

Peter Backeman, Philipp Rümmer, and Aleksandar Zeljic. 2018. Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction. In 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, Nikolaj Bjørner and Arie Gurfinkel (Eds.). IEEE, 1–10.

[6]

Tiffany Bao, Ruoyu Wang, Yan Shoshitaishvili, and David Brumley. 2017. Your Exploit is Mine: Automatic Shellcode Transplant for Remote Exploits. In 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017. IEEE Computer Society, 824–839.

[7]

Clark W. Barrett and Cesare Tinelli. 2018. Satisfiability Modulo Theories. In Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer, 305–343.

[8]

Edd Barrett and Andy King. 2010. Range and Set Abstraction using SAT. Electron. Notes Theor. Comput. Sci., 267, 1 (2010).

[9]

Thomas Becker, Volker Weispfenning, and Heinz Kredel. 1993. Gröbner bases - a computational approach to commutative algebra (Graduate texts in mathematics, Vol. 141). Springer. isbn:978-3-540-97971-5

[10]

Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, and Roberto Sebastiani. 2009. Software model checking via large-block encoding. In Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA. IEEE, 25–32.

[11]

Fabrizio Biondi, Michael A. Enescu, Annelie Heuser, Axel Legay, Kuldeep S. Meel, and Jean Quilbeuf. 2018. Scalable Approximation of Quantitative Information Flow in Programs. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, Isil Dillig and Jens Palsberg (Eds.) (Lecture Notes in Computer Science, Vol. 10747). Springer, 71–93.

[12]

Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein. 2015. ν Z-an optimizing SMT solver. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035. Springer-Verlag, Berlin, Heidelberg. 194–199. isbn:978-3-662-46680-3

[13]

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2003. A Static Analyzer for Large Safety-critical Software. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI ’03). ACM, New York, NY, USA. 196–207. isbn:1-58113-662-5

Digital Library

[14]

Jörg Brauer and Andy King. 2010. Automatic Abstraction for Intervals Using Boolean Formulae. In Proceedings of the 17th International Conference on Static Analysis (SAS’10). Springer-Verlag, Berlin, Heidelberg. 167–183. isbn:3-642-15768-8, 978-3-642-15768-4

Digital Library

[15]

Michael Brickenstein, Alexander Dreyer, Gert-Martin Greuel, Markus Wedler, and Oliver Wienand. 2009. New developments in the theory of Gröbner bases and applications to formal verification. Journal of Pure and Applied Algebra, 213, 8 (2009).

[16]

Stefan Bygde, Björn Lisper, and Niklas Holsti. 2012. Fully Bounded Polyhedral Analysis of Integers with Wrapping. Electron. Notes Theor. Comput. Sci., 288 (2012), 3–13.

Digital Library

[17]

P. Chen and H. Chen. 2018. Angora: Efficient Fuzzing by Principled Search. In 2018 IEEE Symposium on Security and Privacy (SP). 00, 711–725. issn:2375-1207

[18]

Yuansi Chen, Raaz Dwivedi, Martin J. Wainwright, and Bin Yu. 2018. Fast MCMC Sampling Algorithms on Polytopes. J. Mach. Learn. Res., 19 (2018), 55:1–55:86.

[19]

Victor Chernozhukov and Han Hong. 2003. An MCMC approach to classical estimation. Journal of Econometrics, 115, 2 (2003), 293–346.

[20]

Patrick Cousot and Radhia Cousot. 1977. Static Determination of Dynamic Properties of Generalized Type Unions. In Proceedings of an ACM Conference on Language Design for Reliable Software. Association for Computing Machinery, New York, NY, USA. 77–94. isbn:9781450373807

Digital Library

[21]

Patrick Cousot and Radhia Cousot. 1979. Systematic Design of Program Analysis Frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL ’79). Association for Computing Machinery, New York, NY, USA. 269–282. isbn:9781450373579

Digital Library

[22]

Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Restraints Among Variables of a Program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, Alfred V. Aho, Stephen N. Zilles, and Thomas G. Szymanski (Eds.). ACM Press, 84–96.

Digital Library

[23]

Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, and Grigore Rosu. 2019. A complete formal semantics of x86-64 user-level instruction set architecture. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM, 1133–1148.

Digital Library

[24]

Sumanth Dathathri, Nikos Aréchiga, Sicun Gao, and Richard M. Murray. 2017. Learning-Based Abstractions for Nonlinear Constraint Solving. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, Carles Sierra (Ed.). ijcai.org, 592–599.

[25]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg. 337–340. isbn:3-540-78799-2, 978-3-540-78799-0

Digital Library

[26]

B. Dolan-Gavitt, P. Hulin, E. Kirda, T. Leek, A. Mambretti, W. Robertson, F. Ulrich, and R. Whelan. 2016. LAVA: Large-Scale Automated Vulnerability Addition. In 2016 IEEE Symposium on Security and Privacy (SP). 110–121. issn:2375-1207

[27]

Rafael Dutra, Kevin Laeufer, Jonathan Bachrach, and Koushik Sen. 2018. Efficient Sampling of SAT Solutions for Testing. In Proceedings of the 40th International Conference on Software Engineering (ICSE ’18). Association for Computing Machinery, New York, NY, USA. 549–559. isbn:9781450356381

Digital Library

[28]

Martin E. Dyer and Alan M. Frieze. 1988. On the Complexity of Computing the Volume of a Polyhedron. SIAM J. Comput., 17, 5 (1988), 967–974.

Digital Library

[29]

Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, and Bart Selman. 2013. Taming the Curse of Dimensionality: Discrete Integration by Hashing and Optimization. In Proceedings of the 30th International Conference on Machine Learning, ICML 2013, Atlanta, GA, USA, 16-21 June 2013 (JMLR Workshop and Conference Proceedings, Vol. 28). JMLR.org, 334–342.

[30]

Katalin Fazekas, Fahiem Bacchus, and Armin Biere. 2018. Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories. In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Didier Galmiche, Stephan Schulz, and Roberto Sebastiani (Eds.) (Lecture Notes in Computer Science, Vol. 10900). Springer, 134–151.

[31]

Vijay Ganesh and David L Dill. 2007. A decision procedure for bit-vectors and arrays. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV’07). Springer-Verlag, Berlin, Heidelberg. 519–531. isbn:978-3-540-73367-6

Digital Library

[32]

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2015. Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss. ACM Trans. Program. Lang. Syst., 37, 1 (2015), Article 1, Jan., 1:1–1:35 pages. issn:0164-0925

Digital Library

[33]

Denis Gopan and Thomas Reps. 2007. Low-level Library Analysis and Summarization. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV’07). Springer-Verlag, Berlin, Heidelberg. 68–81. isbn:978-3-540-73367-6

Digital Library

[34]

Sumit Gulwani and Madan Musuvathi. 2008. Cover Algorithms and Their Combination. In Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Sophia Drossopoulou (Ed.) (Lecture Notes in Computer Science, Vol. 4960). Springer, 193–207.

[35]

Jingxuan He, Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2020. Learning fast and precise numerical analysis. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 1112–1127.

Digital Library

[36]

Julien Henry, Mihail Asavoae, David Monniaux, and Claire Maiza. 2014. How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. In SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2014, LCTES ’14, Edinburgh, United Kingdom - June 12 - 13, 2014, Youtao Zhang and Prasad Kulkarni (Eds.). ACM, 43–52.

Digital Library

[37]

Heqing Huang, Peisen Yao, Rongxin Wu, Qingkai Shi, and Charles Zhang. 2020. Pangolin: Incremental Hybrid Fuzzing with Polyhedral Path Abstraction. In 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020. IEEE, 1613–1627.

[38]

Jiahong Jiang, Liqian Chen, Xueguang Wu, and Ji Wang. 2017. Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, Ahmed Bouajjani and David Monniaux (Eds.) (Lecture Notes in Computer Science, Vol. 10145). Springer, 310–329.

[39]

Ajith K John and Supratik Chakraborty. 2011. A quantifier elimination algorithm for linear modular equations and disequations. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11). Springer-Verlag, Berlin, Heidelberg. 486–503. isbn:978-3-642-22109-5

Digital Library

[40]

Ajith K John and Supratik Chakraborty. 2013. Extending quantifier elimination to linear inequalities on bit-vectors. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13). Springer-Verlag, Berlin, Heidelberg. 78–92. isbn:978-3-642-36741-0

Digital Library

[41]

Martin Jonás and Jan Strejcek. 2016. Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Nadia Creignou and Daniel Le Berre (Eds.) (Lecture Notes in Computer Science, Vol. 9710). Springer, 267–283.

[42]

Ravi Kannan and Hariharan Narayanan. 2009. Random Walks on Polytopes and an Affine Interior Point Method for Linear Programming. In Proceedings of the Forty-first Annual ACM Symposium on Theory of Computing (STOC ’09). ACM, New York, NY, USA. 561–570. isbn:978-1-60558-506-2

Digital Library

[43]

Ravindran Kannan and Hariharan Narayanan. 2012. Random Walks on Polytopes and an Affine Interior Point Method for Linear Programming. Math. Oper. Res., 37, 1 (2012), 1–20.

Digital Library

[44]

Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps. 2017. Non-Linear Reasoning for Invariant Synthesis. Proc. ACM Program. Lang., 2, POPL (2017), Article 54, Dec., 33 pages.

[45]

Nathan Kitchen and Andreas Kuehlmann. 2007. Stimulus generation for constrained random simulation. In 2007 International Conference on Computer-Aided Design, ICCAD 2007, San Jose, CA, USA, November 5-8, 2007, Georges G. E. Gielen (Ed.). IEEE Computer Society, 258–265.

[46]

Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. 2012. Constraints as Control. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’12). Association for Computing Machinery, New York, NY, USA. 151–164. isbn:9781450310833

Digital Library

[47]

Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2016. SMT-based model checking for recursive programs. Formal Methods Syst. Des., 48, 3 (2016), 175–205.

Digital Library

[48]

Soonho Kong, Armando Solar-Lezama, and Sicun Gao. 2018. Delta-Decision Procedures for Exists-Forall Problems over the Reals. 10982 (2018), 219–235.

[49]

Shuvendu K Lahiri, Robert Nieuwenhuis, and Albert Oliveras. 2006. SMT techniques for fast predicate abstraction. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV’06). Springer-Verlag, Berlin, Heidelberg. 424–437. isbn:3-540-37406-X, 978-3-540-37406-0

Digital Library

[50]

Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, and Marsha Chechik. 2014. Symbolic optimization with SMT solvers. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). ACM, New York, NY, USA. 607–618. isbn:978-1-4503-2544-8

Digital Library

[51]

Junghee Lim and Thomas Reps. 2013. TSL: A System for Generating Abstract Interpreters and Its Application to Machine-Code Analysis. ACM Trans. Program. Lang. Syst., 35, 1 (2013), Article 4, April, 59 pages. issn:0164-0925

Digital Library

[52]

Fangzhen Lin. 2001. On strongest necessary and weakest sufficient conditions. Artif. Intell., 128, 1-2 (2001), 143–159.

[53]

Fangzhen Lin and Ray Reiter. 1994. Forget it. In Working Notes of AAAI Fall Symposium on Relevance. 154–159.

[54]

Björn Lisper. 2003. Fully Automatic, Parametric Worst-Case Execution Time Analysis. In Proceedings of the 3rd International Workshop on Worst-Case Execution Time Analysis, WCET 2003 - a Satellite Event to ECRTS 2003, Polytechnic Institute of Porto, Portugal, July 1, 2003, Jan Gustafsson (Ed.). MDH-MRTC-116/2003-1-SE, Department of Computer Science and Engineering, Mälardalen University, Box 883, 721 23 Västerås, Sweden, 99–102.

[55]

Francesco Logozzo and Manuel Fähndrich. 2008. On the Relative Completeness of Bytecode Analysis Versus Source Code Analysis. In Compiler Construction, 17th International Conference, CC 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, Laurie J. Hendren (Ed.) (Lecture Notes in Computer Science, Vol. 4959). Springer, 197–212.

[56]

Rüdiger Loos and Volker Weispfenning. 1993. Applying Linear Quantifier Elimination. Comput. J., 36, 5 (1993), 450–462.

[57]

Kuldeep S. Meel and S. Akshay. 2020. Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’20). Association for Computing Machinery, New York, NY, USA. 728–741. isbn:9781450371049

[58]

Antoine Miné. 2001. A New Numerical Abstract Domain Based on Difference-Bound Matrices. In Proceedings of the Second Symposium on Programs As Data Objects (PADO ’01). Springer-Verlag, London, UK, UK. 155–172. isbn:3-540-42068-1

Digital Library

[59]

Antoine Miné. 2006. The octagon abstract domain. High. Order Symb. Comput., 19, 1 (2006), 31–100.

Digital Library

[60]

David Monniaux. 2009. Automatic Modular Abstractions for Linear Constraints. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’09). ACM, New York, NY, USA. 140–151. isbn:978-1-60558-379-2

Digital Library

[61]

David Monniaux. 2010. Quantifier Elimination by Lazy Model Enumeration. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV’10). Springer-Verlag, Berlin, Heidelberg. 585–599. isbn:364214294X

Digital Library

[62]

Alexander Nadel and Vadim Ryvchin. 2016. Bit-vector optimization. In Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636 (TACAS’16). Springer-Verlag New York, Inc., New York, NY, USA. 851–867. isbn:978-3-662-49673-2

Digital Library

[63]

Nina Narodytska and Fahiem Bacchus. 2014. Maximum satisfiability using core-guided MaxSAT resolution. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence (AAAI’14). AAAI Press, 2717–2723.

Digital Library

[64]

Reuven Naveh and Amit Metodi. [n. d.]. Beyond Feasibility: CP Usage in Constrained-Random Functional Hardware Verification. In Principles and Practice of Constraint Programming - 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, Christian Schulte (Ed.) (Lecture Notes in Computer Science, Vol. 8124).

[65]

Nicholas Nethercote and Julian Seward. 2007. Valgrind: A Framework for Heavyweight Dynamic Binary Instrumentation. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’07). Association for Computing Machinery, New York, NY, USA. 89–100. isbn:9781595936332

Digital Library

[66]

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. 2018. Solving Quantified Bit-Vectors Using Invertibility Conditions. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, Hana Chockler and Georg Weissenbacher (Eds.) (Lecture Notes in Computer Science, Vol. 10982). Springer, 236–255.

[67]

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. 2021. Syntax-Guided Quantifier Instantiation. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, Jan Friso Groote and Kim Guldstrand Larsen (Eds.) (Lecture Notes in Computer Science, Vol. 12652). Springer, 145–163.

Digital Library

[68]

Robert Nieuwenhuis and Albert Oliveras. 2006. On SAT modulo theories and optimization problems. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT’06). Springer-Verlag, Berlin, Heidelberg. 156–169. isbn:3-540-37206-7, 978-3-540-37206-6

Digital Library

[69]

Sebastian Poeplau and Aurélien Francillon. 2020. Symbolic execution with SymCC: Don’t interpret, compile!. In 29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020, Srdjan Capkun and Franziska Roesner (Eds.). USENIX Association, 181–198.

[70]

Mathias Preiner, Aina Niemetz, and Armin Biere. 2017. Counterexample-Guided Model Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, Axel Legay and Tiziana Margaria (Eds.) (Lecture Notes in Computer Science, Vol. 10205). 264–280.

[71]

John Regehr and Alastair Reid. 2004. HOIST: A System for Automatically Deriving Static Analyzers for Embedded Systems. In Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XI). ACM, New York, NY, USA. 133–143. isbn:1-58113-804-0

Digital Library

[72]

Thomas Reps and Gogul Balakrishnan. 2008. Improved Memory-access Analysis for x86 Executables. In Proceedings of the Joint European Conferences on Theory and Practice of Software 17th International Conference on Compiler Construction (CC’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg. 16–35. isbn:3-540-78790-9, 978-3-540-78790-7

Digital Library

[73]

Thomas W. Reps, Shmuel Sagiv, and Greta Yorsh. 2004. Symbolic Implementation of the Best Transformer. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings, Bernhard Steffen and Giorgio Levi (Eds.) (Lecture Notes in Computer Science, Vol. 2937). Springer, 252–266.

[74]

Thomas W. Reps and Aditya V. Thakur. 2016. Automating Abstract Interpretation. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings, Barbara Jobstmann and K. Rustan M. Leino (Eds.) (Lecture Notes in Computer Science, Vol. 9583). Springer, 3–40.

[75]

Fabian Ritter. 2015. Compiler Optimizations using Symbolic Abstraction. Ph. D. Dissertation. Saarland University.

[76]

Sriram Sankaranarayanan, Franjo Ivančić, Ilya Shlyakhter, and Aarti Gupta. 2006. Static Analysis in Disjunctive Numerical Domains. In Proceedings of the 13th International Conference on Static Analysis (SAS’06). Springer-Verlag, Berlin, Heidelberg. 3–17. isbn:3-540-37756-5, 978-3-540-37756-6

Digital Library

[77]

Roberto Sebastiani and Silvia Tomasi. 2015. Optimization Modulo Theories with Linear Rational Costs. ACM Trans. Comput. Logic, 16, 2 (2015), Article 12, Feb., 43 pages. issn:1529-3785

Digital Library

[78]

Roberto Sebastiani and Silvia Tomasi. 2015. Optimization modulo theories with linear rational costs. ACM Trans. Comput. Logic, 16, 2 (2015), Article 12, Feb., 43 pages. issn:1529-3785

Digital Library

[79]

Roberto Sebastiani and Patrick Trentin. 2015. OptiMathSAT: A Tool for Optimization Modulo Theories. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Daniel Kroening and Corina S. Pasareanu (Eds.) (Lecture Notes in Computer Science, Vol. 9206). Springer, 447–454.

[80]

Roberto Sebastiani and Patrick Trentin. 2015. Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035. Springer-Verlag, Berlin, Heidelberg. 335–349. isbn:978-3-662-46680-3

Digital Library

[81]

Tushar Sharma, Thomas Reps, and Aditya Thakur. 2013. An Abstract Domain for Bit-Vector Inequalities. University of Wisconsin-Madison Department of Computer Sciences.

[82]

Tushar Sharma and Thomas W. Reps. 2017. Sound Bit-Precise Numerical Domains. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, Ahmed Bouajjani and David Monniaux (Eds.) (Lecture Notes in Computer Science, Vol. 10145). Springer, 500–520.

[83]

Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Andrew Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Krügel, and Giovanni Vigna. 2016. SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis. In IEEE Symposium on Security and Privacy, SP 2016, San Jose, CA, USA, May 22-26, 2016. IEEE Computer Society, 138–157.

[84]

Axel Simon and Andy King. 2007. Taming the Wrapping of Integer Arithmetic. In Static Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings, Hanne Riis Nielson and Gilberto Filé (Eds.) (Lecture Notes in Computer Science, Vol. 4634). Springer, 121–136.

[85]

Gagandeep Singh, Markus Püschel, and Martin Vechev. 2017. Fast Polyhedra Abstract Domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM, New York, NY, USA. 46–59. isbn:978-1-4503-4660-3

Digital Library

[86]

Gagandeep Singh, Markus Püschel, and Martin Vechev. 2017. A Practical Construction for Decomposing Numerical Abstract Domains. Proc. ACM Program. Lang., 2, POPL (2017), Article 55, Dec., 28 pages. issn:2475-1421

[87]

Gagandeep Singh, Markus Püschel, and Martin Vechev. 2017. A Practical Construction for Decomposing Numerical Abstract Domains. Proc. ACM Program. Lang., 2, POPL (2017), Article 55, Dec., 28 pages. issn:2475-1421

[88]

Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2015. Making numerical program analysis fast. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Steve Blackburn (Eds.). ACM, 303–313.

Digital Library

[89]

Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2018. Fast Numerical Program Analysis with Reinforcement Learning. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, Hana Chockler and Georg Weissenbacher (Eds.) (Lecture Notes in Computer Science, Vol. 10981). Springer, 211–229.

[90]

Jia Song and Jim Alves-Foss. 2016. The DARPA Cyber Grand Challenge: A Competitor’s Perspective, Part 2. IEEE Secur. Priv., 14, 1 (2016), 76–81.

Digital Library

[91]

Nick Stephens, John Grosen, Christopher Salls, Andrew Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2016. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In 23rd Annual Network and Distributed System Security Symposium, NDSS 2016, San Diego, California, USA, February 21-24, 2016. The Internet Society.

[92]

Allison Sullivan, Darko Marinov, and Sarfraz Khurshid. 2019. Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method. In Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, Yamine Aït Ameur and Shengchao Qin (Eds.) (Lecture Notes in Computer Science, Vol. 11852). Springer, 336–352.

[93]

Aditya V Thakur, Matt Elder, and Thomas W Reps. 2012. Bilateral Algorithms for Symbolic Abstraction. In Proceedings of the 19th International Conference on Static Analysis (SAS’12). Springer-Verlag, Berlin, Heidelberg. 111–128. isbn:978-3-642-33124-4

Digital Library

[94]

Aditya V. Thakur, Akash Lal, Junghee Lim, and Thomas W. Reps. 2015. PostHat and All That: Automating Abstract Interpretation. Electron. Notes Theor. Comput. Sci., 311 (2015), 15–32.

Digital Library

[95]

Aditya V. Thakur and Thomas W. Reps. 2012. A Method for Symbolic Computation of Abstract Operations. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, P. Madhusudan and Sanjit A. Seshia (Eds.) (Lecture Notes in Computer Science, Vol. 7358). Springer, 174–192.

[96]

Shiyi Wei, Piotr Mardziel, Andrew Ruef, Jeffrey S. Foster, and Michael Hicks. 2018. Evaluating Design Tradeoffs in Numeric Static Analysis for Java. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Amal Ahmed (Ed.) (Lecture Notes in Computer Science, Vol. 10801). Springer, 653–682.

[97]

Christoph M Wintersteiger, Youssef Hamadi, and Leonardo De Moura. 2013. Efficiently solving quantified bit-vector formulas. Form. Methods Syst. Des., 42, 1 (2013), Feb., 3–23. issn:0925-9856

Digital Library

[98]

Bo-Han Wu and Chung-Yang (Ric) Huang. 2013. A robust constraint solving framework for multiple constraint sets in constrained random verification. In The 50th Annual Design Automation Conference 2013, DAC ’13, Austin, TX, USA, May 29 - June 07, 2013. ACM, 119:1–119:7.

Digital Library

[99]

Greta Yorsh, Thomas W. Reps, and Shmuel Sagiv. 2004. Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, Kurt Jensen and Andreas Podelski (Eds.) (Lecture Notes in Computer Science, Vol. 2988). Springer, 530–545.

[100]

Insu Yun, Sangho Lee, Meng Xu, Yeongjin Jang, and Taesoo Kim. 2018. QSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing. In Proceedings of the 27th USENIX Conference on Security Symposium (SEC’18). USENIX Association, Berkeley, CA, USA. 745–761. isbn:978-1-931971-46-1

Cited By

Yan ZZhang XDi P(2024)Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural NetworksProceedings of the ACM on Programming Languages10.1145/36897658:OOPSLA2(1532-1560)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689765
Su ZKamath STirakitsoontorn PChen Y(2024)The Hidden Burden: Encountering and Managing (Unintended) Stigma in Children with Serious IllnessesProceedings of the ACM on Human-Computer Interaction10.1145/36410218:CSCW1(1-35)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1145/3641021
Huang HYao PChiu HGuo YZhang C(2024)Titan : Efficient Multi-target Directed Greybox Fuzzing2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00059(1849-1864)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00059
Show More Cited By

Index Terms

Program analysis via efficient symbolic abstraction
1. Theory of computation
  1. Logic
    1. Automated reasoning
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis

Recommendations

Precise range analysis on large industry code
ESEC/FSE 2013: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering

Abstract interpretation is widely used to perform static code analysis with non-relational (interval) as well as relational (difference-bound matrices, polyhedral) domains. Analysis using non-relational domains is highly scalable but delivers imprecise ...
PostHat and All That

Abstract interpretation provides an elegant formalism for performing program analysis. Unfortunately, designing and implementing a sound, precise, scalable, and extensible abstract interpreter is difficult. In this paper, we describe an approach to ...
Program analysis using empirical abstraction
Abstract
Given a program analysis problem that consists of a program and a property of interest, we use an empirical approach to automatically construct a sequence of abstractions that approach an ideal abstraction suitable for solving that problem. This ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue OOPSLA

October 2021

2001 pages

EISSN:2475-1421

DOI:10.1145/3492349

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 October 2021

Published in PACMPL Volume 5, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
955
Total Downloads

Downloads (Last 12 months)299
Downloads (Last 6 weeks)36

Reflects downloads up to 09 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yan ZZhang XDi P(2024)Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural NetworksProceedings of the ACM on Programming Languages10.1145/36897658:OOPSLA2(1532-1560)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689765
Su ZKamath STirakitsoontorn PChen Y(2024)The Hidden Burden: Encountering and Managing (Unintended) Stigma in Children with Serious IllnessesProceedings of the ACM on Human-Computer Interaction10.1145/36410218:CSCW1(1-35)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1145/3641021
Huang HYao PChiu HGuo YZhang C(2024)Titan : Efficient Multi-target Directed Greybox Fuzzing2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00059(1849-1864)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00059
Tsiskaridze NBarrett CTinelli C(2024)Generalized Optimization Modulo TheoriesAutomated Reasoning10.1007/978-3-031-63498-7_27(458-479)Online publication date: 1-Jul-2024
https://doi.org/10.1007/978-3-031-63498-7_27
Park KD'Antoni LReps T(2023)Synthesizing SpecificationsProceedings of the ACM on Programming Languages10.1145/36228617:OOPSLA2(1787-1816)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622861
Yao PKe JSun JFu HWu RRen K(2023)Demystifying Template-Based Invariant Generation for Bit-Vector Programs2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE56229.2023.00069(673-685)Online publication date: 11-Sep-2023
https://doi.org/10.1109/ASE56229.2023.00069

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents