• Sun Y, Wang C, Fan G, Shi Q and Zhang X. Fast and Precise Static Null Exception Analysis With Synergistic Preprocessing. IEEE Transactions on Software Engineering. 10.1109/TSE.2024.3466551. 50:11. (3022-3036).

    https://ieeexplore.ieee.org/document/10689456/

  • Guo Y, Yao P and Zhang C. Precise Compositional Buffer Overflow Detection via Heap Disjointness. Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis. (63-75).

    https://doi.org/10.1145/3650212.3652110

  • Baek S and Lee S. (2024). CaLLi: OCaml library for static analysis of LLVM bitcode. SoftwareX. 10.1016/j.softx.2024.101810. 27. (101810). Online publication date: 1-Sep-2024.

    https://linkinghub.elsevier.com/retrieve/pii/S235271102400181X

  • Beyer D, Kettl M and Lemberger T. (2024). Decomposing Software Verification using Distributed Summary Synthesis. Proceedings of the ACM on Software Engineering. 1:FSE. (1307-1329). Online publication date: 12-Jul-2024.

    https://doi.org/10.1145/3660766

  • Cheng X, Ren J and Sui Y. (2024). Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point Slicing. Proceedings of the ACM on Software Engineering. 1:FSE. (494-516). Online publication date: 12-Jul-2024.

    https://doi.org/10.1145/3643749

  • Wu R, He Y, Huang J, Wang C, Tang W, Shi Q, Xiao X and Zhang C. LibAlchemy: A Two-Layer Persistent Summary Design for Taming Third-Party Libraries in Static Bug-Finding Systems. Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. (1-13).

    https://doi.org/10.1145/3597503.3639132

  • Zheng M, Shi Q, Liu X, Xu X, Yu L, Liu C, Wei G and Zhang X. (2024). ParDiff: Practical Static Differential Analysis of Network Protocol Parsers. Proceedings of the ACM on Programming Languages. 8:OOPSLA1. (1208-1234). Online publication date: 29-Apr-2024.

    https://doi.org/10.1145/3649854

  • Zhang B, Chen W, Yao P, Wang C, Tang W and Zhang C. SIRO: Empowering Version Compatibility in Intermediate Representations via Program Synthesis. Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3. (882-899).

    https://doi.org/10.1145/3620666.3651366

  • Tang W, Dong D, Li S, Wang C, Yao P, Zhou J and Zhang C. (2024). Octopus: Scaling Value-Flow Analysis via Parallel Collection of Realizable Path Conditions. ACM Transactions on Software Engineering and Methodology. 33:3. (1-33). Online publication date: 31-Mar-2024.

    https://doi.org/10.1145/3632743

  • Guo Y, Zhou J, Yao P, Shi Q and Zhang C. Precise divide-by-zero detection with affirmative evidence. Proceedings of the 44th International Conference on Software Engineering. (1718-1729).

    https://doi.org/10.1145/3510003.3510066

  • Lyu Y, Fang Y, Zhang Y, Sun Q, Ma S, Bertino E, Lu K and Li J. (2022). Goshawk: Hunting Memory Corruptions via Structure-Aware and Object-Centric Memory Operation Synopsis 2022 IEEE Symposium on Security and Privacy (SP). 10.1109/SP46214.2022.9833613. 978-1-6654-1316-9. (2096-2113).

    https://ieeexplore.ieee.org/document/9833613/

  • Borodin A and Dudina I. (2021). Intraprocedural Analysis Based on Symbolic Execution for Bug Detection. Programming and Computer Software. 10.1134/S0361768821080028. 47:8. (858-865). Online publication date: 1-Dec-2021.

    https://link.springer.com/10.1134/S0361768821080028

  • Borodin A, Goremykin A, Vartanov S and Belevantsev A. (2021). Searching for Taint Vulnerabilities with Svace Static Analysis Tool. Programming and Computer Software. 10.1134/S0361768821060037. 47:6. (466-481). Online publication date: 1-Nov-2021.

    https://link.springer.com/10.1134/S0361768821060037

  • Ding A, Murthy P, Garcia L, Sun P, Chan M and Zonouz S. Mini-Me, You Complete Me! Data-Driven Drone Security via DNN-based Approximate Computing. Proceedings of the 24th International Symposium on Research in Attacks, Intrusions and Defenses. (428-441).

    https://doi.org/10.1145/3471621.3471869

  • Cai Y, Yao P and Zhang C. Canary: practical static detection of inter-thread value-flow bugs. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. (1126-1140).

    https://doi.org/10.1145/3453483.3454099

  • Shi Q, Yao P, Wu R and Zhang C. Path-sensitive sparse analysis without path conditions. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. (930-943).

    https://doi.org/10.1145/3453483.3454086

  • Spasić M and Janičić M. (2020). Verification supported refactoring of embedded sql. Software Quality Journal. 10.1007/s11219-020-09517-y.

    http://link.springer.com/10.1007/s11219-020-09517-y

  • Garzella J, Baranowski M, He S and Rakamarić Z. Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification. Verification, Model Checking, and Abstract Interpretation. (90-111).

    https://doi.org/10.1007/978-3-030-39322-9_5

  • Mathur U, Madhusudan P and Viswanathan M. (2020). What’s Decidable About Program Verification Modulo Axioms?. Tools and Algorithms for the Construction and Analysis of Systems. 10.1007/978-3-030-45237-7_10. (158-177).

    http://link.springer.com/10.1007/978-3-030-45237-7_10

  • Baldoni R, Coppa E, D’elia D, Demetrescu C and Finocchi I. (2018). A Survey of Symbolic Execution Techniques. ACM Computing Surveys. 51:3. (1-39). Online publication date: 31-May-2019.

    https://doi.org/10.1145/3182657

  • Xu X, Sui Y, Yan H and Xue J. VFix. Proceedings of the 41st International Conference on Software Engineering. (512-523).

    https://doi.org/10.1109/ICSE.2019.00063

  • Brotzman R, Liu S, Zhang D, Tan G and Kandemir M. (2019). CaSym: Cache Aware Symbolic Execution for Side Channel Detection and Mitigation 2019 IEEE Symposium on Security and Privacy (SP). 10.1109/SP.2019.00022. 978-1-5386-6660-9. (505-521).

    https://ieeexplore.ieee.org/document/8835249/

  • Zuo Z, Thorpe J, Wang Y, Pan Q, Lu S, Wang K, Xu G, Wang L and Li X. Grapple. Proceedings of the Fourteenth EuroSys Conference 2019. (1-17).

    https://doi.org/10.1145/3302424.3303972

  • Candea G and Godefroid P. (2019). Automated Software Test Generation: Some Challenges, Solutions, and Recent Advances. Computing and Software Science. 10.1007/978-3-319-91908-9_24. (505-531).

    http://link.springer.com/10.1007/978-3-319-91908-9_24

  • Bueno D and Sakallah K. (2019). euforia: Complete Software Model Checking with Uninterpreted Functions. Verification, Model Checking, and Abstract Interpretation. 10.1007/978-3-030-11245-5_17. (363-385).

    http://link.springer.com/10.1007/978-3-030-11245-5_17

  • Shi Q, Xiao X, Wu R, Zhou J, Fan G and Zhang C. (2018). Pinpoint: fast and precise sparse value flow analysis for million lines of code. ACM SIGPLAN Notices. 53:4. (693-706). Online publication date: 2-Dec-2018.

    https://doi.org/10.1145/3296979.3192418

  • Bornholt J and Torlak E. (2018). Finding code that explodes under symbolic evaluation. Proceedings of the ACM on Programming Languages. 2:OOPSLA. (1-26). Online publication date: 24-Oct-2018.

    https://doi.org/10.1145/3276519

  • Shi Q, Xiao X, Wu R, Zhou J, Fan G and Zhang C. Pinpoint: fast and precise sparse value flow analysis for million lines of code. Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. (693-706).

    https://doi.org/10.1145/3192366.3192418

  • Liang H, Liu S, Zhang Y and Wang M. (2017). Improving the precision of static analysis: Symbolic execution based on GCC abstract syntax tree 2017 18th IEEE/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing (SNPD). 10.1109/SNPD.2017.8022752. 978-1-5090-5504-3. (395-400).

    http://ieeexplore.ieee.org/document/8022752/

  • Liu Y, Zhou X, Gong W, Long L, Li Y, Li X, Dai Y and Yang H. (2017). A Survey of Search Strategies in the Dynamic Symbolic Execution. ITM Web of Conferences. 10.1051/itmconf/20171203025. 12. (03025).

    http://www.itm-conferences.org/10.1051/itmconf/20171203025

  • Sui Y, Ye D, Su Y and Xue J. Eliminating Redundant Bounds Checks in Dynamic Buffer Overflow Detection Using Weakest Preconditions. IEEE Transactions on Reliability. 10.1109/TR.2016.2570538. 65:4. (1682-1699).

    http://ieeexplore.ieee.org/document/7515160/

  • Zekany S, Rings D, Harada N, Laurenzano M, Tang L and Mars J. Crystalball. The 49th Annual IEEE/ACM International Symposium on Microarchitecture. (1-12).

    /doi/10.5555/3195638.3195667

  • Zekany S, Rings D, Harada N, Laurenzano M, Tang L and Mars J. (2016). CrystalBall: Statically analyzing runtime behavior via deep sequence learning 2016 49th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO). 10.1109/MICRO.2016.7783727. 978-1-5090-3508-3. (1-12).

    http://ieeexplore.ieee.org/document/7783727/

  • Avgerinos T, Rebert A, Cha S and Brumley D. (2016). Enhancing symbolic execution with veritesting. Communications of the ACM. 59:6. (93-100). Online publication date: 23-May-2016.

    https://doi.org/10.1145/2927924

  • Pernsteiner S, Loncaric C, Torlak E, Tatlock Z, Wang X, Ernst M and Jacky J. (2016). Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. Computer Aided Verification. 10.1007/978-3-319-41540-6_2. (23-41).

    http://link.springer.com/10.1007/978-3-319-41540-6_2

  • Mosleh M, Alhussein M, Baba M, Malek S and ab Hamid S. (2016). Reviewing and Classification of Software Model Checking Tools. Advanced Computer and Communication Engineering Technology. 10.1007/978-3-319-24584-3_23. (279-294).

    http://link.springer.com/10.1007/978-3-319-24584-3_23

  • Ma S, Jiao M, Zhang S, Zhao W and Wang D. Practical null pointer dereference detection via value-dependence analysis. Proceedings of the 2015 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). (70-77).

    https://doi.org/10.1109/ISSREW.2015.7392049

  • Lal A and Qadeer S. (2015). DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs. ACM SIGPLAN Notices. 50:6. (280-290). Online publication date: 7-Aug-2015.

    https://doi.org/10.1145/2813885.2737987

  • Kasikci B, Zamfir C and Candea G. (2015). Automated Classification of Data Races Under Both Strong and Weak Memory Models. ACM Transactions on Programming Languages and Systems. 37:3. (1-44). Online publication date: 18-Jun-2015.

    https://doi.org/10.1145/2734118

  • Lal A and Qadeer S. DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs. Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. (280-290).

    https://doi.org/10.1145/2737924.2737987

  • Zhang Y, Chen Z, Wang J, Dong W and Liu Z. Regular property guided dynamic symbolic execution. Proceedings of the 37th International Conference on Software Engineering - Volume 1. (643-653).

    /doi/10.5555/2818754.2818833

  • Zhang Y, Chen Z, Wang J, Dong W and Liu Z. (2015). Regular Property Guided Dynamic Symbolic Execution 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering (ICSE). 10.1109/ICSE.2015.80. 978-1-4799-1934-5. (643-653).

    http://ieeexplore.ieee.org/document/7194613/

  • Reungsinkonkarn A and Apirukvorapinit P. Bug Detection Using Particle Swarm Optimization with Search Space Reduction. Proceedings of the 2015 6th International Conference on Intelligent Systems, Modelling and Simulation. (53-57).

    https://doi.org/10.1109/ISMS.2015.20

  • Chen N and Kim S. STAR: Stack Trace Based Automatic Crash Reproduction via Symbolic Execution. IEEE Transactions on Software Engineering. 10.1109/TSE.2014.2363469. 41:2. (198-220).

    http://ieeexplore.ieee.org/document/6926857/

  • Wang Q, Jin D and Gong Y. A Memory Model Based on Three-Valued Matrix for Static Defect Detection. Proceedings of the 2014 IEEE International Symposium on Software Reliability Engineering Workshops. (251-256).

    https://doi.org/10.1109/ISSREW.2014.75

  • Ye D, Su Y, Sui Y and Xue J. WPBOUND. Proceedings of the 2014 IEEE 25th International Symposium on Software Reliability Engineering. (88-99).

    https://doi.org/10.1109/ISSRE.2014.20

  • Li Y, Cheung S, Zhang X and Liu Y. (2014). Scaling Up Symbolic Analysis by Removing Z-Equivalent States. ACM Transactions on Software Engineering and Methodology. 23:4. (1-32). Online publication date: 5-Sep-2014.

    https://doi.org/10.1145/2652484

  • Rakamarić Z and Emmi M. SMACK. Proceedings of the 16th International Conference on Computer Aided Verification - Volume 8559. (106-113).

    https://doi.org/10.1007/978-3-319-08867-9_7

  • Shaw A, Doggett D and Hafiz M. Automatically Fixing C Buffer Overflows Using Program Transformations. Proceedings of the 2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks. (124-135).

    https://doi.org/10.1109/DSN.2014.25

  • Torlak E and Bodik R. A lightweight symbolic virtual machine for solver-aided host languages. Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. (530-541).

    https://doi.org/10.1145/2594291.2594340

  • Torlak E and Bodik R. (2014). A lightweight symbolic virtual machine for solver-aided host languages. ACM SIGPLAN Notices. 49:6. (530-541). Online publication date: 5-Jun-2014.

    https://doi.org/10.1145/2666356.2594340

  • Shaw A. Program transformations to fix C buffer overflows. Companion Proceedings of the 36th International Conference on Software Engineering. (733-735).

    https://doi.org/10.1145/2591062.2591199

  • Le W and Pattison S. Patch verification via multiversion interprocedural control flow graphs. Proceedings of the 36th International Conference on Software Engineering. (1047-1058).

    https://doi.org/10.1145/2568225.2568304

  • Avgerinos T, Rebert A, Cha S and Brumley D. Enhancing symbolic execution with veritesting. Proceedings of the 36th International Conference on Software Engineering. (1083-1094).

    https://doi.org/10.1145/2568225.2568293

  • Wang Q, Jin D and Gong Y. Null Dereference Detection via a Backward Analysis. Proceedings of the 2013 20th Asia-Pacific Software Engineering Conference (APSEC) - Volume 01. (553-558).

    https://doi.org/10.1109/APSEC.2013.80

  • Cho C, D'Silva V and Song D. BLITZ. Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering. (136-146).

    https://doi.org/10.1109/ASE.2013.6693074

  • An equivalence checker for hardware-dependent embedded system software. Proceedings of the Eleventh ACM/IEEE International Conference on Formal Methods and Models for Codesign. (119-128).

    /doi/10.5555/3041405.3041491

  • Schiffel U. Safety Transformations. Proceedings of the 32nd International Conference on Computer Safety, Reliability, and Security - Volume 8153. (190-201).

    https://doi.org/10.1007/978-3-642-40793-2_18

  • Le W and Soffa M. (2013). Marple. ACM Transactions on Software Engineering and Methodology. 22:3. (1-38). Online publication date: 1-Jul-2013.

    https://doi.org/10.1145/2491509.2491512

  • Medeiros I, Neves N and Correia M. (2013). Securing energy metering software with automatic source code correction 2013 IEEE 11th International Conference on Industrial Informatics (INDIN). 10.1109/INDIN.2013.6622969. 978-1-4799-0752-6. (701-706).

    http://ieeexplore.ieee.org/document/6622969/

  • Zahur S and Evans D. Circuit Structures for Improving Efficiency of Security and Privacy Tools. Proceedings of the 2013 IEEE Symposium on Security and Privacy. (493-507).

    https://doi.org/10.1109/SP.2013.40

  • Serpeloni F, Moraes R and Bonacin R. Ontology Mapping Validation. Web Portal Design, Implementation, Integration, and Optimization. 10.4018/978-1-4666-2779-6.ch010. (111-121).

    http://services.igi-global.com/resolvedoi/resolve.aspx?doi=10.4018/978-1-4666-2779-6.ch010

  • Schmidt B, Villarraga C, Bormann J, Stoffel D, Wedler M and Kunz W. (2013). A computational model for SAT-based verification of hardware-dependent low-level embedded system software 2013 18th Asia and South Pacific Design Automation Conference (ASP-DAC 2013). 10.1109/ASPDAC.2013.6509684. 978-1-4673-3030-5. (711-716).

    http://ieeexplore.ieee.org/document/6509684/

  • Chen N and Kim S. Puzzle-based automatic testing: bringing humans into the loop by solving puzzles. Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering. (140-149).

    https://doi.org/10.1145/2351676.2351697

  • Kuznetsov V, Kinder J, Bucur S and Candea G. (2012). Efficient state merging in symbolic execution. ACM SIGPLAN Notices. 47:6. (193-204). Online publication date: 6-Aug-2012.

    https://doi.org/10.1145/2345156.2254088

  • Lal A, Qadeer S and Lahiri S. A solver for reachability modulo theories. Proceedings of the 24th international conference on Computer Aided Verification. (427-443).

    https://doi.org/10.1007/978-3-642-31424-7_32

  • Dong L, Dong W and Chen L. Invalid Pointer Dereferences Detection for CPS Software Based on Extended Pointer Structures. Proceedings of the 2012 IEEE Sixth International Conference on Software Security and Reliability Companion. (144-151).

    https://doi.org/10.1109/SERE-C.2012.30

  • Kuznetsov V, Kinder J, Bucur S and Candea G. Efficient state merging in symbolic execution. Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. (193-204).

    https://doi.org/10.1145/2254064.2254088

  • Vujošević-Janičić M and Kuncak V. Development and evaluation of LAV. Proceedings of the 4th international conference on Verified Software: theories, tools, experiments. (98-113).

    https://doi.org/10.1007/978-3-642-27705-4_9

  • Merz F, Falke S and Sinz C. LLBMC. Proceedings of the 4th international conference on Verified Software: theories, tools, experiments. (146-161).

    https://doi.org/10.1007/978-3-642-27705-4_12

  • Sery O, Fedyukovich G and Sharygina N. Interpolation-Based function summaries in bounded model checking. Proceedings of the 7th international Haifa Verification conference on Hardware and Software: verification and testing. (160-175).

    https://doi.org/10.1007/978-3-642-34188-5_15

  • Le W and Soffa M. Generating analyses for detecting faults in path segments. Proceedings of the 2011 International Symposium on Software Testing and Analysis. (320-330).

    https://doi.org/10.1145/2001420.2001459

  • Rubio-González C and Liblit B. Defective error/pointer interactions in the Linux kernel. Proceedings of the 2011 International Symposium on Software Testing and Analysis. (111-121).

    https://doi.org/10.1145/2001420.2001434

  • Serpeloni F, Moraes R and Bonacin R. (2011). Ontology Mapping Validation. International Journal of Web Portals. 3:3. (1-11). Online publication date: 1-Jul-2011.

    https://doi.org/10.4018/jwp.2011070101

  • Katebi H, Sakallah K and Marques-Silva J. Empirical study of the anatomy of modern sat solvers. Proceedings of the 14th international conference on Theory and application of satisfiability testing. (343-356).

    /doi/10.5555/2023474.2023510

  • Ďurfina L, Křoustek J, Zemek P, Kolář D, Hruška T, Masařík K and Meduna A. (2011). Design of a Retargetable Decompiler for a Static Platform-Independent Malware Analysis. Information Security and Assurance. 10.1007/978-3-642-23141-4_8. (72-86).

    http://link.springer.com/10.1007/978-3-642-23141-4_8

  • Katebi H, Sakallah K and Marques-Silva J. (2011). Empirical Study of the Anatomy of Modern Sat Solvers. Theory and Applications of Satisfiability Testing - SAT 2011. 10.1007/978-3-642-21581-0_27. (343-356).

    http://link.springer.com/10.1007/978-3-642-21581-0_27

  • Li L, Cifuentes C and Keynes N. Practical and effective symbolic analysis for buffer overflow detection. Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering. (317-326).

    https://doi.org/10.1145/1882291.1882338

  • Beyer D, Keremoglu M and Wendler P. Predicate abstraction with adjustable-block encoding. Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design. (189-198).

    /doi/10.5555/1998496.1998532

  • Ghafari N, Hu A and Rakamarić Z. Context-bounded translations for concurrent software. Proceedings of the 17th international SPIN conference on Model checking software. (227-244).

    /doi/10.5555/1928137.1928160

  • Dillig I, Dillig T and Aiken A. Small formulas for large programs. Proceedings of the 17th international conference on Static analysis. (236-252).

    /doi/10.5555/1882094.1882109

  • Santelices R and Harrold M. Exploiting program dependencies for scalable multiple-path symbolic execution. Proceedings of the 19th international symposium on Software testing and analysis. (195-206).

    https://doi.org/10.1145/1831708.1831733

  • Tompkins D and Hoos H. Dynamic scoring functions with variable expressions. Proceedings of the 13th international conference on Theory and Applications of Satisfiability Testing. (278-292).

    https://doi.org/10.1007/978-3-642-14186-7_23

  • Serpeloni F, Moraes R and Bonacin R. (2010). A semi-automated approach to validate ontology mappings 2010 10th Annual International Conference on New Technologies of Distributed Systems (NOTERE). 10.1109/NOTERE.2010.5536604. 978-1-4244-7067-9. (309-313).

    http://ieeexplore.ieee.org/document/5536604/

  • Cordeiro L, Fischer B and Marques-Silva J. Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking. Proceedings of the 2010 17th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems. (160-169).

    https://doi.org/10.1109/ECBS.2010.24

  • Ghafari N, Hu A and Rakamarić Z. (2010). Context-Bounded Translations for Concurrent Software: An Empirical Evaluation. Model Checking Software. 10.1007/978-3-642-16164-3_17. (227-244).

    http://link.springer.com/10.1007/978-3-642-16164-3_17

  • Dillig I, Dillig T and Aiken A. (2010). Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis. Static Analysis. 10.1007/978-3-642-15769-1_15. (236-252).

    http://link.springer.com/10.1007/978-3-642-15769-1_15

  • Cordeiro L, Fischer B and Marques-Silva J. SMT-Based Bounded Model Checking for Embedded ANSI-C Software. Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering. (137-148).

    https://doi.org/10.1109/ASE.2009.63

  • Kroening D, Sharygina N, Tonetta S, Tsitovich A and Wintersteiger C. Loopfrog. Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering. (668-670).

    https://doi.org/10.1109/ASE.2009.35

  • Beyer D, Cimatti A, Griggio A, Keremoglu M, Univers S and Sebastiani R. (2009). Software model checking via large-block encoding 2009 Formal Methods in Computer-Aided Design (FMCAD). 10.1109/FMCAD.2009.5351147. 978-1-4244-4966-8. (25-32).

    http://ieeexplore.ieee.org/document/5351147/

  • Babić D and Hu A. (2009). Approximating the safely reusable set of learned facts. International Journal on Software Tools for Technology Transfer (STTT). 11:4. (325-338). Online publication date: 1-Oct-2009.

    /doi/10.5555/3220925.3221264

  • Jhala R and Majumdar R. (2009). Software model checking. ACM Computing Surveys. 41:4. (1-54). Online publication date: 1-Oct-2009.

    https://doi.org/10.1145/1592434.1592438

  • Babić D and Hu A. (2009). Approximating the safely reusable set of learned facts. International Journal on Software Tools for Technology Transfer. 10.1007/s10009-009-0117-2. 11:4. (325-338). Online publication date: 1-Oct-2009.

    http://link.springer.com/10.1007/s10009-009-0117-2

  • Kuliamin V. (2009). Integration of verification methods for program systems. Programming and Computing Software. 35:4. (212-222). Online publication date: 1-Jul-2009.

    https://doi.org/10.1134/S0361768809040057

  • Hu A. (2009). Automatic formal verification of software: Fundamental concepts 2009 International Conference on Communications, Circuits and Systems (ICCCAS). 10.1109/ICCCAS.2009.5250313. 978-1-4244-4886-9. (1155-1159).

    http://ieeexplore.ieee.org/document/5250313/

  • Pipatsrisawat K and Darwiche A. Width-Based Restart Policies for Clause-Learning Satisfiability Solvers. Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing. (341-355).

    https://doi.org/10.1007/978-3-642-02777-2_32

  • Chandra S, Fink S and Sridharan M. Snugglebug. Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation. (363-374).

    https://doi.org/10.1145/1542476.1542517

  • Chandra S, Fink S and Sridharan M. (2009). Snugglebug. ACM SIGPLAN Notices. 44:6. (363-374). Online publication date: 28-May-2009.

    https://doi.org/10.1145/1543135.1542517

  • Nanda M and Sinha S. Accurate Interprocedural Null-Dereference Analysis for Java. Proceedings of the 31st International Conference on Software Engineering. (133-143).

    https://doi.org/10.1109/ICSE.2009.5070515

  • Chatterjee S, Lahiri S, Qadeer S and Rakamarić Z. (2009). A low-level memory model and an accompanying reachability predicate. International Journal on Software Tools for Technology Transfer (STTT). 11:2. (105-116). Online publication date: 1-Apr-2009.

    /doi/10.5555/3220882.3220989

  • Chatterjee S, Lahiri S, Qadeer S and Rakamarić Z. (2009). A low-level memory model and an accompanying reachability predicate. International Journal on Software Tools for Technology Transfer. 10.1007/s10009-009-0098-1. 11:2. (105-116). Online publication date: 1-Apr-2009.

    http://link.springer.com/10.1007/s10009-009-0098-1

  • Sinha N. Symbolic program analysis using term rewriting and generalization. Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design. (1-9).

    /doi/10.5555/1517424.1517443

  • Sinha N. (2008). Symbolic Program Analysis Using Term Rewriting and Generalization 2008 Formal Methods in Computer-Aided Design (FMCAD). 10.1109/FMCAD.2008.ECP.23. 978-1-4244-2735-2. (1-9).

    http://ieeexplore.ieee.org/document/4689182/

  • Kroening D, Sharygina N, Tonetta S, Tsitovich A and Wintersteiger C. Loop Summarization Using Abstract Transformers. Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis. (111-125).

    https://doi.org/10.1007/978-3-540-88387-6_10

  • Rakamaric Z and Hu A. Automatic Inference of Frame Axioms Using Static Analysis. Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering. (89-98).

    https://doi.org/10.1109/ASE.2008.19

  • Ma X, Wang J and Dong W. (2008). Computing Must and May Alias to Detect Null Pointer Dereference. Leveraging Applications of Formal Methods, Verification and Validation. 10.1007/978-3-540-88479-8_18. (252-261).

    http://link.springer.com/10.1007/978-3-540-88479-8_18