More Web Proxy on the site http://driver.im/

research-article

Verification-aided regression testing

Authors:

Fabrizio Pastore,

Leonardo Mariani,

Antti E. J. Hyvärinen,

Grigory Fedyukovich,

Natasha Sharygina,

Stephan Sehestedt,

Ali MuhammadAuthors Info & Claims

ISSTA 2014: Proceedings of the 2014 International Symposium on Software Testing and Analysis

Pages 37 - 48

https://doi.org/10.1145/2610384.2610387

Published: 21 July 2014 Publication History

Abstract

In this paper we present Verification-Aided Regression Testing (VART), a novel extension of regression testing that uses model checking to increase the fault revealing capability of existing test suites. The key idea in VART is to extend the use of test case executions from the conventional direct fault discovery to the generation of behavioral properties specific to the upgrade, by (i) automatically producing properties that are proved to hold for the base version of a program, (ii) automatically identifying and checking on the upgraded program only the properties that, according to the developers’ intention, must be preserved by the upgrade, and (iii) reporting the faults and the corresponding counter-examples that are not revealed by the regression tests. Our empirical study on both open source and industrial software systems shows that VART automatically produces properties that increase the effectiveness of testing by automatically detecting faults unnoticed by the existing regression test suites.

References

[1]

Coreutils. http://www.gnu.org/software/coreutils/.

[2]

Diff utils. http://www.gnu.org/software/diffutils/.

[3]

GDB. http://sources.redhat.com/gdb/.

[4]

Grep. http://www.gnu.org/software/grep/.

[5]

Software-artifact infrastructure repository. http://sir.unl.edu.

[6]

F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharygina. Lazy abstraction with interpolants for arrays. In proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, volume 7180 of LNCS. Springer, 2012.

Digital Library

[7]

R. Arnold and S. Bohner. Software Change Impact Analysis. Wiley-IEEE Computer Society Press, 1996.

Digital Library

[8]

D. Beyer, A. J. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar. Generating tests from counterexamples. In proceedings of the International Conference on Software Engineering, 2004.

Digital Library

[9]

D. Beyer, T. A. Henzinger., R. Jhala, and R. Majumdar. The software model checker Blast: Applications to software engineering. International Journal on Software Tools for Technology Transfer, 9:505–525, 2007.

Digital Library

[10]

D. Beyer and M. E. Keremoglu. CPAchecker: A Tool for Configurable Software Verification. In proceedings of the International Conference on Computer Aided Verification, LNCS, pages 184–190, 2011.

Digital Library

[11]

A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y. Zhu. Symbolic Model Checking Using SAT Procedures instead of BDDs. In proceedings of the annual Design Automation Conference, 1999.

Digital Library

[12]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In proceedings of the International Conference Tools and Algorithms for Construction and Analysis of Systems, volume 1579 of LNCS, pages 193–207. Springer, 1999.

Digital Library

[13]

A. R. Bradley. SAT-based model checking without unrolling. In proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretatio, volume 6538 of LNCS, pages 70–87. Springer, 2011.

Digital Library

[14]

S. Chaki, E. M. Clarke, A. Groce, J. Ouaknine, O. Strichman, and K. Yorav. Eﬃcient verification of sequential and concurrent C programs. Formal Methods in System Design, 25(2–3):129–166, 2004.

Digital Library

[15]

Y. Chen, D. Rosemblum, and K. Vo. TestTube: A system for selective regression testing. In proceedings of the International Conference on Software Engineering, 1994.

Digital Library

[16]

E. Clarke and A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, 1981.

Digital Library

[17]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In proceedings of the International Conference Tools and Algorithms for Construction and Analysis of Systems.

[18]

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. SATABS: SAT-based Predicate Abstraction for ANSI-C. In proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS, 2005.

Digital Library

[19]

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.

Digital Library

[20]

J. Cobb, J. Jones., G. Kapfhammer, and M. J. Harrold. Dynamic invariant detection for relational databases. In proceedings of the Ninth International Workshop on Dynamic Analysis, 2011.

Digital Library

[21]

C. Csallner, Y. Smaragdakis, and T. Xie. DSD-crasher: A hybrid analysis tool for bug finding. ACM Transactions on Software Engineering and Methodologies, 17(2):8:1–8:37, May 2008.

Digital Library

[22]

B. Daniel, V. Jagannath, D. Dig, and D. Marinov. On test repair using symbolic execution. In proceedings of the International Conference on Automated Software Engineering, 2009.

[23]

N. Eén and N. Sörensson. An extensible SAT-solver. In proceedings of the International Conference on Theory and Applications of Satisfiability Testing, volume 2919 of LNCS, pages 502–518. Springer, 2004.

[24]

S. Elbaum, A. Malishevsky, and G. Rothermel. Test case prioritization: A family of empirical studies. IEEE Transactions on Software Engineering, 28(2):159–182, Feb. 2002.

Digital Library

[25]

M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering, 27(2):99–123, 2001.

Digital Library

[26]

G. Fedyukovich, O. Sery, and N. Sharygina. eVolCheck: Incremental Upgrade Checker for C. In proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 7795 of LNCS, 2013.

Digital Library

[27]

C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for ESC/Java. In proceedings of the International Symposium of Formal Methods Europe, 2001.

Digital Library

[28]

M. Gabel and Z. Su. Testing mined specifications. In proceedings of the International Symposium on the Foundations of Software Engineering, 2012.

Digital Library

[29]

B. Godlin and O. Strichman. Regression verification: proving the equivalence of similar programs. Software Testing, Verification & Reliability, 23(3):241––258, 2013.

[30]

S. V. Group. The cbmc homepage. http://www.cprover.org/cbmc/.

[31]

R. H. Hardin, R. P. Kurshan, K. L. McMillan, J. A. Reeds, and N. J. A. Sloane. Eﬃcient regression verification. In proceedings on the International Workshop on Event Systems, 1996.

[32]

W. Jin, A. Orso, and T. Xie. Automated behavioral regression testing. In proceedings of the Third International Conference on Software Testing, Verification and Validation (ICST), 2010.

Digital Library

[33]

S. Joshi, S. Lahiri, and A. Lal. Underspecified harnesses and interleaved bugs. In proceedings of the annual Symposium on Principles of Programming Languages, 2012.

Digital Library

[34]

A. Komuravelli, A. Gurfinkel, S. Chaki, and E. M. Clarke. Automatic abstraction in SMT-based unbounded software model checking. In proceedings of the International Conference on Computer Aided Verification, 2013.

Digital Library

[35]

S. K. Lahiri, K. McMillan, R. Sharma, and C. Hawblitzel. Differential assertion checking. In Foundations of Software Engineering, 2013.

Digital Library

[36]

H. Leung and L. White. Insights into regression testing. In proceedings of the International Conference on Software Maintenance, 1989.

[37]

Y. S. Mahajan, Z. Fu, and S. Malik. Zchaff2004: An eﬃcient SAT solver. In proceedings of the International Conference on Theory and Applications of Satisfiability Testing, Revised Selected Papers, volume 3542 of LNCS, pages 360–375. Springer, 2005.

Digital Library

[38]

L. Mariani, S. Papagiannakis, and M. Pezzé. Compatibility and regression testing of COTS-component-based software. In proceedings of the International Conference on Software Engineering, 2007.

Digital Library

[39]

L. Mariani, F. Pastore, and M. Pezzé. Dynamic analysis for diagnosing integration faults. IEEE Transactions on Software Engineering, 37(4):486–508, 2011.

Digital Library

[40]

K. McMillan. Symbolic Model Checking. An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, 1992.

Digital Library

[41]

K. L. McMillan. Lazy abstraction with interpolants. In proceedings of the International Conference on Computer Aided Verification, volume 4144 of LNCS, pages 123–136. Springer, 2006.

Digital Library

[42]

M. Mirzaaghaei, F. Pastore, and M. Pezzé. Supporting test suite evolution through test case adaptation. In proceedings of the International Conference on Software Testing, Verification, and Validation, 2012.

Digital Library

[43]

T. Nguyen, D. Kapur, W. Weimer, and S. Forrest. Using dynamic analysis to discover polynomial and array invariants. In proceedings of the International Conference on Software Engineering, 2012.

Digital Library

[44]

J. W. Nimmer and M. D. Ernst. Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. Electronic Notes on Theoretical Computer Science, 55(2):255–276, 2001.

[45]

J. W. Nimmer and M. D. Ernst. Automatic generation of program specifications. In proceedings of the International Symposium on Software Testing and Analysis, 2002.

Digital Library

[46]

F. Pastore, L. Mariani, and G. Fraser. Crowdoracles: Can the crowd solve the oracle problem. In proceedings of the International Conference on Software Testing, Verification and Validation (ICST), 2013.

Digital Library

[47]

F. Pastore, L. Mariani, and A. Goﬃ. RADAR: a tool for debugging regression problems in C/C++ software. In proceedings of the International Conference on Software Engineering - Tool Demo Track, 2013.

Digital Library

[48]

F. Pastore, L. Mariani, A. Goﬃ, M. Oriol, and M. Wahler. Dynamic analysis of upgrades in C/C++ software. In proceedings of the International Symposium on Software Reliability Engineering, 2012.

Digital Library

[49]

S. Person, M. Dwyer, S. Elbaum, and C. Pˇ asˇ areanu. Differential symbolic execution. In proceedings of the International Symposium on Foundations of Software Engineering, 2008.

Digital Library

[50]

M. Pradel, C. Jaspan, J. Aldrich, and T. R. Gross. Statically checking api protocol conformance with mined multi-object specifications. In proceedings of the International Conference on Software Engineering, 2012.

Digital Library

[51]

G. Rothermel and M. Harrold. A safe, eﬃcient regression test selection technique. ACM Transactions on Software Engineering and Methodologies, 6(2):173–210, Apr. 1997.

Digital Library

[52]

D. Schuler, V. Dallmeier, and A. Zeller. Eﬃcient mutation testing by checking invariant violations. In proceedings of the International Symposium on Software Testing and Analysis, 2009.

Digital Library

[53]

O. Sery, G. Fedyukovich, and N. Sharygina. FunFrog: Bounded model checking with interpolation-based function summarization. In proceedings of the International Symposium on Automated Technology for Verification and Analysis, volume 7561 of LNCS, pages 203–207. Springer, 2012.

Digital Library

[54]

O. Sery, G. Fedyukovich, and N. Sharygina. Incremental upgrade checking by means of interpolation-based function summaries. In proceedings of the International Conference on Formal Methods in Computer-Aided Design. IEEE, 2012.

[55]

Y. Shimomura. The present status and future prospects of the iter project. Journal of Nuclear Materials, 329-333(1):5–11, 2004.

[56]

J. Silva. A vocabulary of program slicing-based techniques. ACM Computing Survey, 44(3):12:1–12:41, 2012.

Digital Library

[57]

J. P. M. Silva and K. A. Sakallah. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506–521, 1999.

Digital Library

[58]

A. L. Souter and L. Pollock. The construction of contextual def-use associations for object-oriented systems. IEEE Transactions on Software Engineering, 29(11):1005–1018, Nov. 2003.

Digital Library

[59]

K. R. Walcott, M. L. Soffa, G. M. Kapfhammer, and R. S. Roos. Timeaware test suite pioritization. In proceedings of the International Symposium on Software Testing and Analysis, 2006.

Digital Library

[60]

A. Wasylkowski and A. Zeller. Mining temporal specifications from object usage. In proceedings of the International Conference on Automated Software Engineering, 2009.

Digital Library

[61]

A. Wasylkowski, A. Zeller, and C. Lindig. Detecting object usage anomalies. In proceedings of the joint meeting of the European Software Engineering Conference and the International Symposium on Foundations of Software Engineering, 2007.

Digital Library

[62]

T. Xie and D. Notkin. Tool-assisted unit test generation and selection based on operational abstractions. Automated Software Engineering Journal, 13(3):345–371, July 2006.

Digital Library

[63]

G. Yang, S. Khurshid, S. Person, and N. Rungta. Property differencing for incremental checking. In proceedings of the International Conference on Software Engineering, 2014.

Digital Library

[64]

J. Yi, D. Qi, S. Tan, and A. Roychoudhury. Expressing and checking intended changes via software change contracts. In proceedings of the International Symposium on Software Testing and Analysis, 2013.

Digital Library

[65]

H. Zhu, P. Hall, and J. May. Software unit test coverage and adequacy. ACM Computing Surveys, 29(4):366–427, Dec. 1997.

Digital Library

Cited By

Hui MWang LLi HYang RSong YZhuang HCui DLi Q(2025)Unveiling the microservices testing methods, challenges, solutions, and solutions gaps: A systematic mapping studyJournal of Systems and Software10.1016/j.jss.2024.112232220(112232)Online publication date: Feb-2025
https://doi.org/10.1016/j.jss.2024.112232
Ngo CPastore FBriand L(2022)Automated, Cost-effective, and Update-driven App TestingACM Transactions on Software Engineering and Methodology10.1145/350229731:4(1-51)Online publication date: 12-Jul-2022
https://dl.acm.org/doi/10.1145/3502297
He FYu QCai L(2022)Efficient Summary Reuse for Software Regression VerificationIEEE Transactions on Software Engineering10.1109/TSE.2020.302147748:4(1417-1431)Online publication date: 1-Apr-2022
https://doi.org/10.1109/TSE.2020.3021477
Show More Cited By

Index Terms

Verification-aided regression testing

Recommendations

Dependent-test-aware regression testing techniques
ISSTA 2020: Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis

Developers typically rely on regression testing techniques to ensure that their changes do not break existing functionality. Unfortunately, these techniques suffer from flaky tests, which can both pass and fail when run multiple times on the same ...
Regression testing of GUIs
ESEC/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering

Although graphical user interfaces (GUIs) constitute a large part of the software being developed today and are typically created using rapid prototyping, there are no effective regression testing techniques for GUIs. The needs of GUI regression testing ...
On test suite composition and cost-effective regression testing

Regression testing is an expensive testing process used to revalidate software as it evolves. Various methodologies for improving regression testing processes have been explored, but the cost-effectiveness of these methodologies has been shown to vary ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA 2014: Proceedings of the 2014 International Symposium on Software Testing and Analysis

July 2014

460 pages

ISBN:9781450326452

DOI:10.1145/2610384

General Chair:
Corina S. Păsăreanu
NASA Ames, USA
,
Program Chair:
Darko Marinov
University of Illinois at Urbana-Champaign, USA

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 July 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ISSTA '14

Sponsor:

SIGSOFT

ISSTA '14: International Symposium on Software Testing and Analysis

July 21 - 25, 2014

CA, San Jose, USA

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
319
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)1

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hui MWang LLi HYang RSong YZhuang HCui DLi Q(2025)Unveiling the microservices testing methods, challenges, solutions, and solutions gaps: A systematic mapping studyJournal of Systems and Software10.1016/j.jss.2024.112232220(112232)Online publication date: Feb-2025
https://doi.org/10.1016/j.jss.2024.112232
Ngo CPastore FBriand L(2022)Automated, Cost-effective, and Update-driven App TestingACM Transactions on Software Engineering and Methodology10.1145/350229731:4(1-51)Online publication date: 12-Jul-2022
https://dl.acm.org/doi/10.1145/3502297
He FYu QCai L(2022)Efficient Summary Reuse for Software Regression VerificationIEEE Transactions on Software Engineering10.1109/TSE.2020.302147748:4(1417-1431)Online publication date: 1-Apr-2022
https://doi.org/10.1109/TSE.2020.3021477
Pastore FMicucci DGuzman MMariani L(2022)TkT: Automatic Inference of Timed and Extended Pushdown AutomataIEEE Transactions on Software Engineering10.1109/TSE.2020.299852748:2(617-636)Online publication date: 1-Feb-2022
https://doi.org/10.1109/TSE.2020.2998527
Rutledge ROrso A(2022)Automating Differential Testing with Overapproximate Symbolic Execution2022 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST53961.2022.00035(256-266)Online publication date: Apr-2022
https://doi.org/10.1109/ICST53961.2022.00035
Wang HLin YYang ZSun JLiu YDong JZheng QLiu T(2021)Explaining Regressions via Alignment Slicing and MendingIEEE Transactions on Software Engineering10.1109/TSE.2019.294956847:11(2421-2437)Online publication date: 1-Nov-2021
https://doi.org/10.1109/TSE.2019.2949568
Bartocci EManjunath NMariani LMateis CNičković D(2021)CPSDebug: Automatic failure explanation in CPS modelsInternational Journal on Software Tools for Technology Transfer10.1007/s10009-020-00599-4Online publication date: 8-Jan-2021
https://doi.org/10.1007/s10009-020-00599-4
Vassilev MVassilev VPenev A(2020)IDD – A Platform Enabling Differential DebuggingCybernetics and Information Technologies10.2478/cait-2020-000420:1(53-67)Online publication date: 27-Mar-2020
https://doi.org/10.2478/cait-2020-0004
He FHan J(2020)Termination analysis for evolving programs: an incremental approach by reusing certified modulesProceedings of the ACM on Programming Languages10.1145/34282674:OOPSLA(1-27)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428267
Bartocci EManjunath NMariani LMateis CNičković DPastore FKhurshid SPăsăreanu C(2020)CPSDebug: a tool for explanation of failures in cyber-physical systemsProceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3395363.3404369(569-572)Online publication date: 18-Jul-2020
https://dl.acm.org/doi/10.1145/3395363.3404369
Show More Cited By

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents