TestEra: A novel framework for automated testing of Java programs We present TestEra, a novel framework for automated testing of Java programs. TestEra automatically generates all non-isomorphic test cases within a given input size and evaluates correctness criteria. As an enabling technology, TestEra uses Alloy, a first-order relational language, and the Alloy Analyzer. Checking a program with TestEra involves modeling the correctness criteria for the program in Alloy and specifying abstraction and concretization translations between instances of Alloy models and Java data structures. TestEra produces concrete Java inputs as counterexamples to violated correctness criteria. The paper discusses TestEra’s analyses of several case studies: methods that manipulate singly linked lists and red-black trees, a naming architecture, and a part of the Alloy Analyzer.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 19 articles )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
  2. Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
  3. Bengolea, Valeria; Aguirre, Nazareno; Marinov, Darko; Frias, Marcelo F.: Using coverage criteria on repOK to reduce bounded-exhaustive test suites (2012)
  4. Hallé, Sylvain; Villemaire, Roger; Cherkaoui, Omar; Deca, Rudy: A logical approach to data-aware automated sequence generation (2012)
  5. Yang, Guowei; Khurshid, Sarfraz; Kim, Miryung: Specification-based test repair using a lightweight formal method (2012)
  6. Aguirre, Nazareno M.; Bengolea, Valeria S.; Frias, Marcelo F.; Galeotti, Juan P.: Incorporating coverage criteria in bounded exhaustive black box test generation of structural inputs (2011)
  7. Angeletti, Damiano; Giunchiglia, Enrico; Narizzano, Massimo; Puddu, Alessandra; Sabina, Salvatore: Using bounded model checking for coverage analysis of safety-critical software in an industrial setting (2010)
  8. Habermehl, Peter; Iosif, Radu; Vojnar, Tomáš: Automata-based verification of programs with tree updates (2010)
  9. Arcuri, Andrea; Yao, Xin: Search based software testing of object-oriented containers (2008)
  10. Zybin, R.S.; Kuliamin, V.V.; Ponomarenko, A.V.; Rubanov, V.V.; Chernov, E.S.: Automation of broad sanity test generation (2008)
  11. Bouillaguet, Charles; Kuncak, Viktor; Wies, Thomas; Zee, Karen; Rinard, Martin: Using first-order theorem provers in the Jahob data structure verification system (2007)
  12. Engel, Christian; Hähnle, Reiner: Generating unit tests from formal proofs (2007)
  13. Simons, Anthony J.H.: Jwalk: a tool for lazy, systematic testing of Java classes by design introspection and user interaction. (2007)
  14. Simons, Anthony J.H.: Jwalk: a tool for lazy, systematic testing of java classes by design introspection and user interaction (2007)
  15. Artho, Cyrille; Barringer, Howard; Goldberg, Allen; Havelund, Klaus; Khurshid, Sarfraz; Lowry, Mike; Pasareanu, Corina; Roşu, Grigore; Sen, Koushik; Visser, Willem; Washington, Rich: Combining test case generation and runtime verification (2005)
  16. Arkoudas, Konstantine; Khurshid, Sarfraz; Marinov, Darko; Rinard, Martin: Integrating model checking and theorem proving for relational reasoning (2004)
  17. Khurshid, Sarfraz; Marinov, Darko: TestEra: specification-based testing of Java programs using sat (2004)
  18. Khurshid, Sarfraz; Marinov, Darko; Shlyakhter, Ilya; Jackson, Daniel: A case for efficient solution enumeration (2004)
  19. Marinov, Darko; Khurshid, Sarfraz: VAlloy -- virtual functions meet a relational language (2002)