Editorial for the special issue of STVR on tests and proofs volume 2: tests and proofs for improving the generation time and quality of test data suites (2014)

In our continued effort to reduce the backlog of accepted papers at STVR, this issue has six papers. The first four make up volume 2 of the special issue on tests and proofs, and the last two are regular papers. I introduce the two regular papers here, and the special issue editors introduce the special issue papers below. "A model-free and state-cover testing scheme for semaphore-based and shared-memory concurrent programs," by Gwan-Hwan Hwang, Che-Sheng Lin, Teng-Shuo Lee, and Chi Wu-Lee, addresses the testing of concurrent programs. If the number of synchronization sequences is finite, their approach tests all of them, If the number of synchronization sequences is infinite, their approach applies state-cover testing. (Recommended by Marc Roper.) "Exploring the missing link: An empirical study of software fixes," by Maggie Hamill and Katerina Goseva-Popstojanova, gives data from a study of fixes to software faults. They used a safety-critical NASA program and report, among other findings, that a significant percentage of fixes required changes to multiple modules. (Recommended by Jane Hayes.) I would also like to take this opportunity to thank the special issue editors, Achim Brucker and Jacques Julliand, for their incredible hard work and dedication in putting this special issue together. The increasing use of IT systems in security or safety critical areas as well as the growing system complexity creates challenges for both formal verification and testing. It might initially appear that these are competing techniques: it can be argued that once a program is proven to be correct, there is no need for additional tests. Similarly, if it is not feasible to produce a formal proof, then one cannot do better than testing your program thoroughly. As a consequence of this perception, proofs and tests have been pursued by distinct communities using rather different techniques and tools. Despite this historical separation of work on testing and proof, research in these areas has led to the discovery of common issues and to the realisation that each may need the other. The emergence of model checking was one of the first signs that contradictions contribute to testing, but in the past few years an increasing number of researchers have encountered the need to combine proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer. This special issue of STVR tries to bring together researchers and practitioners working in the converging fields of testing and proving. We received 16 submissions for this special issue. Reviewing followed the same process as for regular papers. Each paper was reviewed by at least three reviewers, and after a rigorous selection process requiring a total of 33 revisions and 75 reviews, seven papers remain for publication. These papers are spread across two special issues of STVR and discuss two different aspects of tests and proofs: model-based testing, and approaches for improving the quality of generated test data. This is the second volume of the Special Issue on Tests and Proofs. The four papers in this issue discuss techniques for improving the generation time and quality of test data sets. The first paper, “Bridging the Gap Between Easy Generation and Efficient Verification of Unsatisfiability Proofs” by Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler proposes a new format for refutation proofs of SAT solvers that allows for clause deletion during proof checking. Among others, the work of the authors facilitates unsatisfiability checking and makes it possible to efficiently integrate results of a SAT solver in a logical safe way into proof techniques. The second paper, “Automated Test Case Generation for FBD Programs Implementing Reactor Protection System Software” by Eunkyoung Jee, Donghwan Shin, Sungdeok Cha, Jang-Soo Lee and Doo-Hwan Bae presents an approach that uses SAT solvers during test case generation to improve its efficiency and its reliability. In particular, the authors present an approach for automatically generating test cases that check correctness relative to functional block diagrams, a formalism used in implementing safety critical systems. The third paper, “RepOK-Based Reduction of Bounded-Exhaustive Testing” by Valeria Bengolea, Nazareno Aguirre, Darko Marinov, and Marcelo Frias, presents techniques for reducing the time for bounded-exhaustive testing, by either reducing the generation time or reducing the obtained bounded-exhaustive suites, e.g., by removing those tests that are equivalent to some tests already present in the suite. The fourth paper, “A Random Testing Approach Using Pushdown Automata” by Aloïs Dreyfus, Pierre-Cyrille Héam, Olga Kouchnarenko, and Catherine Masson, addresses the problem that generating test cases from abstract models may result in tests that are not concretisable, i.e., do not correspond to an actual execution of the system under test. The pushdown automata-based approach of the authors has, compared to approaches from the literature, a much higher ability to generate concretisable test cases. All the contributions presented in this issue and the previous special issue on Tests and Proofs reveal the broad and dynamic community that works on the intersection of tests and proofs. This was only possible through the combined efforts of all authors and reviewers, and we wish to thank them all for their time and energy. The following persons were reviewers: Paul Ammann, Lukas Brügger, Fabian Büttner, Cristian Cadar, George Candea, John Derrick, Catherine Dubois, Alessandro Fantechi, Vijay Ganesh, Angelo Gargantini, Ryszard Janicki, Thierry Jéron, Tomoji Kishi, Nils Klarlund, Nikolai Kosmatov, Moez Krichen, Pascale Le Gall, Bruno Legeard, Zdenek Letko, Xuandong Li, Karl Meinke, Magnus Myreen, Joseph Near, Virginia Papailiopoulou, Jan Peleska, Dennis Peters, Alexander Pretschner, Antoine Rollet, Kristin Y. Rozier, Andy Schurr, Thomas Sewell, Tomohiko Takagi, Andreas Teucke, T.H. Tse, Mark Utting, Machiel van der Bijl, Luca Viganò, Birgit Vogel-Heuser, TjarkWeber, StephanWeissleder, Tim A.C.Willemse, Christoph Wintersteiger, Burkhart Wolff, Dianxiang Xu, and Steve Zdancewic. Last but not least, the STVR chief editors, Robert Hierons and Jeff Offutt, provided expert guidance and important advice throughout the process.