Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Innovations in Systems and Software Engineering
Erschienen in: Innovations in Systems and Software Engineering 3-4/2019

09.04.2019 | S.I.: NFM2018

A synergistic approach to improving symbolic execution using test ranges

verfasst von: Guowei Yang, Rui Qiu, Sarfraz Khurshid, Corina S. Păsăreanu, Junye Wen

Erschienen in: Innovations in Systems and Software Engineering | Ausgabe 3-4/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Symbolic execution is a systematic technique for checking programs, which has received a lot of research attention during the last decade. In principle, symbolic execution provides a powerful analysis for bug finding. In practice however, the technique remains computationally expensive and hard to scale. This paper introduces SynergiSE, a novel synergistic approach to improving symbolic execution by tackling a key bottleneck to its wider adoption: costly and incomplete constraint solving. To mitigate the cost, SynergiSE introduces a succinct encoding of constraint solving results, thereby enabling symbolic execution to be distributed among different workers while sharing and reusing constraint solving results among them without having to communicate databases of constraint solving results. To mitigate the incompleteness, SynergiSE introduces an integration of complementary approaches for testing, e.g., search-based test generation, with symbolic execution, thereby enabling symbolic execution and other techniques to apply in tandem, say to create higher-quality tests. Experimental results using a suite of Java programs show that SynergiSE presents a promising approach for improving symbolic execution.
Vorheriger Artikel Property specification patterns at work: verification and inconsistency explanation
Nächster Artikel A QCA design and energy analysis of binary semaphore with a comprehensive case study

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Literatur
1.
Albert E, Gómez-Zamalloa M, Rojas JM, Puebla G (2011) Compositional clp-based test data generation for imperative languages. In: Proceedings of the 20th international conference on logic-based program synthesis and transformation, LOPSTR’11. Springer, Berlin, pp 99–116
2.
Anand S, Burke EK, Chen TY, Clark J, Cohen MB, Grieskamp W, Harman M, Harrold MJ, Mcminn P (2013) An orchestrated survey of methodologies for automated software test case generation. J Syst Softw 86(8):1978–2001CrossRef
3.
Baars AI, Harman M, Hassoun Y, Lakhotia K, McMinn P, Tonella P, Vos TEJ (2011) Symbolic search-based testing. In: 26th IEEE/ACM international conference on automated software engineering (ASE 2011), Lawrence, KS, USA, November 6–10, 2011, pp 53–62
4.
Balasubramanian D, Păsăreanu CS, Whalen MW, Karsai G, Lowry M (2011) Polyglot: modeling and analysis for multiple statechart formalisms. In: Proceedings of the 2011 international symposium on software testing and analysis, ISSTA’11. ACM, New York, pp 45–55
5.
Beyer D, Henzinger TA, Keremoglu ME, Wendler P (2012) Conditional model checking: a technique to pass information between verifiers. In: Proceedings of the ACM SIGSOFT 20th international symposium on the foundations of software engineering, FSE’12. ACM, New York, pp 57:1–57:11
6.
Beyer D, Lemberger T (2018) CPA-SymExec: efficient symbolic execution in CPAchecker. In: Proceedings of the 33rd ACM/IEEE international conference on automated software engineering, ASE 2018. ACM, New York, pp 900–903
7.
Boyapati C, Khurshid S, Marinov D (2002) Korat: automated testing based on java predicates. In: Proceedings of the 2002 ACM SIGSOFT international symposium on software testing and analysis, ISSTA’02. ACM, New York, pp 123–133
8.
Bucur S, Ureche V, Zamfir C, Candea G (2011) Parallel symbolic execution for automated real-world software testing. In: Proceedings of the sixth conference on computer systems, EuroSys’11. ACM, New York, pp 183–198
9.
Burnim J, Juvekar S, Sen K (2009) Wise: automated test generation for worst-case complexity. In: Proceedings of the 31st international conference on software engineering, ICSE’09. IEEE Computer Society, Washington, DC, pp 463–473
10.
Cadar C, Dunbar D, Engler D (2008) Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX conference on operating systems design and implementation, OSDI’08. USENIX Association, Berkeley, pp 209–224
11.
Castaño R, Braberman V, Garbervetsky D, Uchitel S (2017) Model checker execution reports. In: Proceedings of the 32nd IEEE/ACM international conference on automated software engineering, ASE 2017. IEEE Press, Piscataway, pp 200–205
12.
Chen J, Hu W, Zhang L, Hao D, Khurshid S, Zhang L (2018) Learning to accelerate symbolic execution via code transformation. In: Proceedings of the 32nd European conference on object-oriented programming, ECOOP 2018, Amsterdam, Netherlands, pp 6:1–6:27
13.
Clarke LA (1976) A program testing system. In: Proceedings of the 1976 annual conference, ACM’76. ACM, New York, pp 488–491
14.
Dini N (2016) MKorat: a novel approach for memoizing the Korat search and some potential applications. Master’s thesis, University of Texas at Austin
15.
Dini N, Yelen C, Khurshid S (2017) Optimizing parallel korat using invalid ranges. In: Proceedings of the 24th ACM SIGSOFT international SPIN symposium on model checking of software, Santa Barbara, CA, USA, July 10–14, 2017, pp 182–191
16.
Dong S, Olivo O, Zhang L, Khurshid S (2015) Studying the influence of standard compiler optimizations on symbolic execution. In: 26th IEEE international symposium on software reliability engineering, ISSRE 2015, Gaithersbury, MD, USA, November 2–5, 2015. IEEE Computer Society, pp 205–215
17.
Dustmann OS, Wehrle K, Cadar C (2018) Parti: a multi-interval theory solver for symbolic execution. In: Proceedings of the 33rd ACM/IEEE international conference on automated software engineering, ASE 2018. ACM, New York, pp 430–440
18.
Eclat: automatic generation and classification of test inputs. In: Proceedings of the 19th European conference on object-oriented programming, ECOOP’05, 2005. Springer, Berlin, pp 504–527
19.
Forum MP (1994) Mpi: a message-passing interface standard. Technical report, Knoxville, TN, USA
20.
Fraser G, Arcuri A (2011) Evolutionary generation of whole test suites. In: Proceedings of the 2011 11th international conference on quality software, QSIC’11. IEEE Computer Society, Washington, DC, pp 31–40
21.
Godefroid P (2007) Compositional dynamic test generation. In: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL’07. ACM, New York, pp 47–54
22.
Godefroid P, Klarlund N, Sen K (2005) DART: directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN conference on programming language design and implementation, PLDI’05. ACM, New York, pp 213–223
23.
Inkumsah K, Xie T (2007) Evacon: a framework for integrating evolutionary and concolic testing for object-oriented programs. In: 22nd IEEE/ACM international conference on automated software engineering (ASE 2007), November 5–9, 2007. Atlanta, Georgia, USA, pp 425–428
24.
Inkumsah K, Xie T (2008) Improving structural testing of object-oriented programs via integrating evolutionary testing and symbolic execution. In: Proceedings of the 2008 23rd IEEE/ACM international conference on automated software engineering, ASE’08. IEEE Computer Society, Washington, DC, pp 297–306
25.
Jia X, Ghezzi C, Ying S (2015) Enhancing reuse of constraint solutions to improve symbolic execution. In: Proceedings of the 2015 international symposium on software testing and analysis, ISSTA 2015. ACM, New York, pp 177–187
26.
Jia Y, Harman M (2011) An analysis and survey of the development of mutation testing. IEEE Trans Softw Eng 37(5):649–678CrossRef
27.
Joshi A, Heimdahl MPE (2005) Model-based safety analysis of simulink models using scade design verifier. In: Proceedings of the 24th international conference on computer safety, reliability, and security, SAFECOMP’05. Springer, Berlin, pp 122–135
28.
Khurshid S, Păsăreanu CS, Visser W (2003) Generalized symbolic execution for model checking and testing. In: Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems, TACAS’03. Springer, Berlin, pp 553–568
29.
Kim M, Kim Y, Rothermel G (2012) A scalable distributed concolic testing approach: an empirical evaluation. In: Proceedings of the 2012 IEEE fifth international conference on software testing, verification and validation, ICST ’12. IEEE Computer Society, Washington, DC, pp 340–349
30.
31.
Köroglu Y, Sen A (2016) Design of a modified concolic testing algorithm with smaller constraints. In: Proceedings of the 7th workshop on constraint solvers in testing, verification, and analysis co-located with the international symposium on software testing and analysis (ISSTA 2016), Saarbrücken, Germany, July 17th, 2016, pp 3–14
32.
Köroglu Y, Sen A (2016) Design of a modified concolic testing algorithm with smaller constraints. In: International workshop on constraints in software testing, verification and analysis 2016, CSTVA@ISSTA
33.
Lakhotia K, McMinn P, Harman M (2010) An empirical investigation into branch coverage for C programs using CUTE and AUSTIN. J Syst Softw 83(12):2379–2391CrossRef
34.
Lauterburg S, Sobeih A, Marinov D, Viswanathan M (2008) Incremental state-space exploration for programs with dynamically allocated data. In: 30th international conference on software engineering (ICSE 2008), Leipzig, Germany, May 10–18, 2008, pp 291–300
35.
Li G, Andreasen E, Ghosh I (2014) SymJS: automatic symbolic testing of javascript web applications. In: Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, FSE 2014. ACM, New York, pp 449–459
36.
Liew D, Cadar C, Donaldson AF (2016) Symbooglix: a symbolic execution engine for boogie programs. In: 2016 IEEE international conference on software testing, verification and validation, ICST 2016, Chicago, IL, USA, April 11–15, 2016, pp 45–56
37.
Ma K-K, Phang KY, Foster JS, Hicks M (2011) Directed symbolic execution. In: Proceedings of the 18th international conference on static analysis, SAS’11. Springer, Berlin, pp 95–111
38.
Misailovic S, Milicevic A, Petrovic N, Khurshid S, Marinov D (2007) Parallel test generation and execution with Korat. In: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering, ESEC-FSE’07. ACM, New York, pp 135–144
39.
Pacheco C, Lahiri SK, Ernst MD, Ball T (2007) Feedback-directed random test generation. In: Proceedings of the 29th international conference on software engineering, ICSE’07. IEEE Computer Society, Washington, DC, pp 75–84
40.
Pasareanu CS, Visser W, Bushnell DH, Geldenhuys J, Mehlitz PC, Rungta N (2013) Symbolic pathfinder: integrating symbolic execution with model checking for java bytecode analysis. Autom Softw Eng 20(3):391–425CrossRef
41.
Person S, Yang G, Rungta N, Khurshid S (2011) Directed incremental symbolic execution. In: Proceedings of the 32nd ACM SIGPLAN conference on programming language design and implementation, PLDI’11. ACM, New York, pp 504–515
42.
Păsăreanu CS, Mehlitz PC, Bushnell DH, Gundy-Burlet K, Lowry M, Person S, Pape M (2008) Combining unit-level symbolic execution and system-level concrete execution for testing Nasa software. In: Proceedings of the 2008 international symposium on software testing and analysis, ISSTA’08. ACM, New York, pp 15–26
43.
Păsăreanu CS, Rungta N (2010) Symbolic pathfinder: symbolic execution of java bytecode. In: Proceedings of the IEEE/ACM international conference on automated software engineering, ASE’10. ACM, New York, pp 179–180
44.
Qiu R (2016) Scaling and certifying symbolic execution, Ph.D. dissertation, University of Texas at Austin
45.
Qiu R, Khurshid S, Păsăreanu CS, Wen J, Yang G (2018) Using test ranges to improve symbolic execution. In: Dutle A, Muñoz C, Narkawicz A (eds) NASA formal methods. Springer, Cham, pp 416–434
46.
Qiu R, Khurshid S, Păsăreanu CS, Yang G (2017) A synergistic approach for distributed symbolic execution using test ranges. In: Proceedings of the 39th international conference on software engineering, ICSE 2017, Buenos Aires, Argentina, May 20–28, 2017—companion volume, pp 130–132
47.
Qiu R, Yang G, Păsăreanu CS, Khurshid S (2015) Compositional symbolic execution with memoized replay. In: Proceedings of the 37th international conference on software engineering, vol 1, ICSE’15. IEEE Press, Piscataway, pp 632–642
48.
Rojas JM, Păsăreanu CS (2013) Compositional symbolic execution through program specialization. In: BYTECODE’13, ETAPS’13
49.
50.
Sen K, Agha G (2006) CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Computer aided verification. Springer, Berlin, pp 419–423
51.
Sen K, Marinov D, Agha G (2005) CUTE: a concolic unit testing engine for C. In: Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on foundations of software engineering, ESEC/FSE-13. ACM, New York, pp 263–272
52.
Shafi A, Carpenter B, Baker M (2009) Nested parallelism for multi-core HPC systems using Java. J Parallel Distrib Comput 69(6):532–545CrossRef
53.
Siddiqui JH, Khurshid S (2010) Parsym: parallel symbolic execution. In: 2010 2nd international conference on software technology and engineering, vol 1, pp V1-405–V1-409
54.
Siddiqui JH, Khurshid S (2012) Scaling symbolic execution using ranged analysis. In: Proceedings of the ACM international conference on object oriented programming systems languages and applications, OOPSLA’12. ACM, New York, pp 523–536
55.
56.
Slabý J, Strejček J, Trtík M (2012) Checking properties described by state machines: on synergy of instrumentation, slicing, and symbolic execution. In: Stoelinga M, Pinger R (eds) Formal methods for industrial critical systems. Springer, Berlin, pp 207–221CrossRef
57.
Souza M, Borges M, d’Amorim M, Păsăreanu CS (2011) CORAL: solving complex constraints for symbolic PathFinder. In: Proceedings of the third international conference on NASA formal methods, NFM’11. Springer, Heidelberg, pp 359–374
58.
Staats M, Pǎsǎreanu C (2010) Parallel symbolic execution for structural test generation. In: Proceedings of the 19th international symposium on software testing and analysis, ISSTA’10. ACM, New York, pp 183–194
59.
60.
61.
Visser W, Geldenhuys J, Dwyer MB (2012) Green: reducing, reusing and recycling constraints in program analysis. In: Proceedings of the ACM SIGSOFT 20th international symposium on the foundations of software engineering, FSE’12. ACM, New York, pp 58:1–58:11
62.
Wagner J, Kuznetsov V, Candea G (2013) -OVERIFY: optimizing programs for fast verification. In: Presented as part of the 14th workshop on hot topics in operating systems, Santa Ana Pueblo, NM, USENIX
63.
Wang R, Ning P, Xie T, Chen Q (2013) MetaSymploit: day-one defense against script-based attacks with security-enhanced symbolic analysis. In: Proceedings of the USENIX security symposium
64.
Wen J, Yang G (2018) Parallel property checking with symbolic execution. In: The 30th international conference on software engineering and knowledge engineering, Hotel Pullman, Redwood City, California, USA, July 1–3, 2018, pp 554–553
65.
Wen J, Yang G (2019) Parallel property checking with staged symbolic execution. In: Proceedings of the 34th annual ACM symposium on applied computing, SAC 2019, Limassol, Cyprus, April 08–12, 2019. (to appear)
66.
Yang G, Dwyer MB, Rothermel G (2009) Regression model checking. In: 25th IEEE international conference on software maintenance (ICSM 2009), September 20–26, 2009. Edmonton, Alberta, Canada, pp 115–124
67.
Yang G, Khurshid S, Person S, Rungta N (2014) Property differencing for incremental checking. In: Proceedings of the 36th international conference on software engineering, ICSE 2014. ACM, New York, pp 1059–1070
68.
Yang G, Person S, Rungta N, Khurshid S (2014) Directed incremental symbolic execution. ACM Trans Softw Eng Methodol 24(1):3:1–3:42CrossRef
69.
Yang G, Păsăreanu CS, Khurshid S (2012) Memoized symbolic execution. In: Proceedings of the 2012 international symposium on software testing and analysis, ISSTA 2012. ACM, New York, pp 144–154
Metadaten
Titel
A synergistic approach to improving symbolic execution using test ranges
verfasst von
Guowei Yang
Rui Qiu
Sarfraz Khurshid
Corina S. Păsăreanu
Junye Wen
Publikationsdatum
09.04.2019
Verlag
Springer London
Erschienen in
Innovations in Systems and Software Engineering / Ausgabe 3-4/2019
Print ISSN: 1614-5046
Elektronische ISSN: 1614-5054
DOI
https://doi.org/10.1007/s11334-019-00331-9

Weitere Artikel der Ausgabe 3-4/2019

Innovations in Systems and Software Engineering 3-4/2019 Zur Ausgabe

S.I. : CSI2017

A QCA design and energy analysis of binary semaphore with a comprehensive case study

Editorial

Selected extended papers of NFM 2018

S.I.: NFM2018

Certified normalization of generalized traces

S.I. : NFM2018

Model-based testing of stochastically timed systems

S.I. : NFM2018

Formal modeling and analysis of safety-critical human multitasking

S.I. : NFM2018

Optimal compression of combinatorial state spaces

Premium Partner

    Bildnachweise