Article

CONTESSA: concurrency testing augmented with symbolic analysis

Authors:

Sudipta Kundu,

Malay K. Ganai,

Chao WangAuthors Info & Claims

CAV'10: Proceedings of the 22nd international conference on Computer Aided Verification

Pages 127 - 131

https://doi.org/10.1007/978-3-642-14295-6_13

Published: 15 July 2010 Publication History

Publisher Site

Abstract

Testing of multi-threaded programs poses enormous challenges To improve the coverage of testing, we present a framework named Contessa that augments conventional testing (concrete execution) with symbolic analysis in a scalable and efficient manner to explore both thread interleaving and input data space It is built on partial-order reduction techniques that generate verification conditions with reduced size and search space It also provides a visual support for debugging the witness traces We show its significance in testbeds.

References

[1]

Godefroid, P.: Software Model Checking: The Verisoft approach In: FMSD (2005)

Digital Library

Google Scholar

[2]

Musuvathi, M., Quadeer, S.: CHESS: Systematic stress testing of concurrent software In: Puebla, G (ed.) LOPSTR 2006 LNCS, vol 4407, pp 15-16 Springer, Heidelberg (2007)

Digital Library

Google Scholar

[3]

Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: A Runtime Model Checker for Multithreaded C Programs Technical Report UUCS-08-004, University of Utah (2008)

Google Scholar

[4]

Edelstein, O., Farchi, E., Goldin, E., Nir, Y., Ratsaby, G., Ur, S.: Framework for Testing Multi-threaded Java Programs In: Concurrency and Computation: Practice and Experience (2003)

Google Scholar

[5]

Sen, K.: Race directed random testing of concurrent programs In: PLDI (2008)

Digital Library

Google Scholar

[6]

Farzan, A., Madhusudan, P.: Causal Atomicity In: Ball, T., Jones, R.B (eds.) CAV 2006 LNCS, vol 4144, pp 315-328 Springer, Heidelberg (2006)

Digital Library

Google Scholar

[7]

Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic pruning of concurrent program executions In: ESEC-FSE (2009)

Digital Library

Google Scholar

[8]

Ganai, M.K., Kundu, S.: Reduction of Verification Conditions for Concurrent System using Mutually Atomic Transactions In: Proc of SPINWorkshop (2009)

Digital Library

Google Scholar

[9]

Ganai, M.K., Gupta, A.: Efficient modeling of concurrent systems in bmc In: Havelund, K., Majumdar, R., Palsberg, J (eds.) SPIN 2008 LNCS, vol 5156, pp 114-133 Springer, Heidelberg (2008)

Digital Library

Google Scholar

[10]

SRI Yices: An SMT solver, http://fm.csl.sri.com/yices

Google Scholar

[11]

JPF, http://babelfish.arc.nasa.gov/trac/jpf

Google Scholar

Cited By

View all

Wang YWen MWu RLiu ZTan SZhu ZYu HCheung SAtlee JBultan TWhittle J(2019)Could I have a stack trace to examine the dependency conflict issue?Proceedings of the 41st International Conference on Software Engineering10.1109/ICSE.2019.00068(572-583)Online publication date: 25-May-2019
https://dl.acm.org/doi/10.1109/ICSE.2019.00068
Cheng LYang ZWang CRosu GDi Penta MNguyen T(2017)Systematic reduction of GUI test sequencesProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering10.5555/3155562.3155668(849-860)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.5555/3155562.3155668
Guo SKusano MWang CLo DApel SKhurshid S(2016)Conc-iSE: incremental symbolic execution of concurrent softwareProceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering10.1145/2970276.2970332(531-542)Online publication date: 25-Aug-2016
https://dl.acm.org/doi/10.1145/2970276.2970332
Show More Cited By

CONTESSA: concurrency testing augmented with symbolic analysis
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
2. Theory of computation

Recommendations

Improving the effectiveness of test suite reduction for user-session-based testing of web applications

Context: Test suite reduction is the problem of creating and executing a set of test cases that are smaller in size but equivalent in effectiveness to an original test suite. However, reduced suites can still be large and executing all the tests in a ...
Faster mutation testing inspired by test prioritization and reduction
ISSTA 2013: Proceedings of the 2013 International Symposium on Software Testing and Analysis

Mutation testing is a well-known but costly approach for determining test adequacy. The central idea behind the approach is to generate mutants, which are small syntactic transformations of the program under test, and then to measure for a given test ...
Spartan: a spectral and entropy-based partial-scan and test point insertion algorithm

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CAV'10: Proceedings of the 22nd international conference on Computer Aided Verification

July 2010

673 pages

ISBN:364214294X

Editors:
Tayssir Touili
LIAFA, CNRS and University Paris Diderot, Paris Cedex 13, France
,
Byron Cook
LIAFA, Microsoft Research, Roger Needham Building, J J Thomson Avenue, Cambridge, UK
,
Paul Jackson
School of Informatics, University of Edinburgh, Roger Needham Building, J J Thomson Avenue, Edinburgh, UK

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 15 July 2010

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Wang YWen MWu RLiu ZTan SZhu ZYu HCheung SAtlee JBultan TWhittle J(2019)Could I have a stack trace to examine the dependency conflict issue?Proceedings of the 41st International Conference on Software Engineering10.1109/ICSE.2019.00068(572-583)Online publication date: 25-May-2019
https://dl.acm.org/doi/10.1109/ICSE.2019.00068
Cheng LYang ZWang CRosu GDi Penta MNguyen T(2017)Systematic reduction of GUI test sequencesProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering10.5555/3155562.3155668(849-860)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.5555/3155562.3155668
Guo SKusano MWang CLo DApel SKhurshid S(2016)Conc-iSE: incremental symbolic execution of concurrent softwareProceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering10.1145/2970276.2970332(531-542)Online publication date: 25-Aug-2016
https://dl.acm.org/doi/10.1145/2970276.2970332
Guo SKusano MWang CYang ZGupta ADi Nitto EHarman MHeymans P(2015)Assertion guided symbolic execution of multithreaded programsProceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering10.1145/2786805.2786841(854-865)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2786805.2786841
Zhang MWu YLu SQi SRen JZheng WCheung SOrso AStorey M(2014)AI: a lightweight system for tolerating concurrency bugsProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2635868.2635885(330-340)Online publication date: 11-Nov-2014
https://dl.acm.org/doi/10.1145/2635868.2635885
Wang CHoang K(2014)Precisely Deciding Control State Reachability in Concurrent Traces with Limited ObservabilityProceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 831810.1007/978-3-642-54013-4_21(376-394)Online publication date: 19-Jan-2014
https://dl.acm.org/doi/10.1007/978-3-642-54013-4_21
Ganai MDenney EBultan TZeller A(2013)Efficient data race prediction with incremental reasoning on time-stamped lock historyProceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2013.6693064(37-47)Online publication date: 11-Nov-2013
https://dl.acm.org/doi/10.1109/ASE.2013.6693064
Shirole MKumar R(2012)Testing for concurrency in UML diagramsACM SIGSOFT Software Engineering Notes10.1145/2347696.234771237:5(1-8)Online publication date: 2-Sep-2012
https://dl.acm.org/doi/10.1145/2347696.2347712
West SNanz SMeyer B(2012)Demonic testing of concurrent programsProceedings of the 14th international conference on Formal Engineering Methods: formal methods and software engineering10.1007/978-3-642-34281-3_33(478-493)Online publication date: 12-Nov-2012
https://dl.acm.org/doi/10.1007/978-3-642-34281-3_33
Wang CGanai M(2011)Predicting concurrency failures in the generalized execution traces of x86 executablesProceedings of the Second international conference on Runtime verification10.1007/978-3-642-29860-8_2(4-18)Online publication date: 27-Sep-2011
https://dl.acm.org/doi/10.1007/978-3-642-29860-8_2
Show More Cited By

Abstract

References

Cited By

Recommendations

Improving the effectiveness of test suite reduction for user-session-based testing of web applications

Faster mutation testing inspired by test prioritization and reduction

Spartan: a spectral and entropy-based partial-scan and test point insertion algorithm

Comments

Information

Published In

Sponsors

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Share

Share this Publication link

Share on social media

Affiliations