2011
|
Ulbrich, Mattias; Geilmann, Ulrich; Ghazi, Aboubakr Achraf El; Taghdiri, Mana On Proving Alloy Specifications using KeY Technical Report Karlsruhe Institute of Technology no. 2011-37, 2011. @techreport{ulbrich-geilmann-elghazi-taghdiri-techrep2011,
title = {On Proving Alloy Specifications using KeY},
author = {Mattias Ulbrich and Ulrich Geilmann and Aboubakr Achraf El Ghazi and Mana Taghdiri},
year = {2011},
date = {2011-01-01},
number = {2011-37},
institution = {Karlsruhe Institute of Technology},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
|
Beckert, Bernhard; Gladisch, Christoph; Tyszberowicz, Shmuel; Yehudai, Amiram KeYGenU: Combining Verification-Based and Capture and Replay Techniques for Regression Unit Testing Journal Article In: International Journal of System Assurance Engineering and Management, vol. 2, no. 2, pp. 97–113, 2011, ISSN: 0976-4348. @article{Beckert2011,
title = {KeYGenU: Combining Verification-Based and Capture and Replay Techniques for Regression Unit Testing},
author = { Bernhard Beckert and Christoph Gladisch and Shmuel Tyszberowicz and Amiram Yehudai},
url = {http://dx.doi.org/10.1007/s13198-011-0068-3},
doi = {10.1007/s13198-011-0068-3},
issn = {0976-4348},
year = {2011},
date = {2011-01-01},
journal = {International Journal of System Assurance Engineering and Management},
volume = {2},
number = {2},
pages = {97--113},
abstract = {Unit testing plays a major role in the software development process. Two essential criteria to achieve effective unit testing are: (1) testing each unit in isolation from other parts of the program and (2) achieving high code coverage. The former requires a lot of extra work such as writing drivers and stubs, whereas the latter is difficult to achieve when manually writing the tests. When changing existing code it is advocated to run the unit tests to avoid regression bugs. However, in many cases legacy software has no unit tests. Writing those tests from scratch is a hard and tedious process, which might not be cost-effective. This paper presents a tool chain approach that combines verification-based testing (VBT) and capture and replay (CaR) test generation methods. We have built a concrete tool chain, KeYGenU, which consists of two existing tools---KeY and GenUTest. The KeY system is a deductive verification and test-generation tool. GenUTest automatically generates JUnit tests for a correctly working software. This combination provides isolated unit test suites with high code-coverage. The generated tests can also be used for regression testing.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Unit testing plays a major role in the software development process. Two essential criteria to achieve effective unit testing are: (1) testing each unit in isolation from other parts of the program and (2) achieving high code coverage. The former requires a lot of extra work such as writing drivers and stubs, whereas the latter is difficult to achieve when manually writing the tests. When changing existing code it is advocated to run the unit tests to avoid regression bugs. However, in many cases legacy software has no unit tests. Writing those tests from scratch is a hard and tedious process, which might not be cost-effective. This paper presents a tool chain approach that combines verification-based testing (VBT) and capture and replay (CaR) test generation methods. We have built a concrete tool chain, KeYGenU, which consists of two existing tools---KeY and GenUTest. The KeY system is a deductive verification and test-generation tool. GenUTest automatically generates JUnit tests for a correctly working software. This combination provides isolated unit test suites with high code-coverage. The generated tests can also be used for regression testing. |
Schmitt, Peter H.; Ulbrich, Mattias; Weiß, Benjamin Dynamic Frames in Java Dynamic Logic Proceedings Article In: Beckert, Bernhard; Marché, Claude (Ed.): Revised Selected Papers, International Conference on Formal
Verification of Object-Oriented Software (FoVeOOS 2010), pp. 138–152, Springer, 2011. @inproceedings{SchmittEtAl2011,
title = {Dynamic Frames in Java Dynamic Logic},
author = {Peter H. Schmitt and Mattias Ulbrich and Benjamin Wei\ss
},
editor = {Bernhard Beckert and Claude March\'{e}
},
year = {2011},
date = {2011-01-01},
booktitle = {Revised Selected Papers, International Conference on Formal
Verification of Object-Oriented Software (FoVeOOS 2010)},
volume = {6528},
pages = {138--152},
publisher = {Springer},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2010
|
Gladisch, Christoph Test Data Generation for Programs with Quantified First-Order
Logic Specifications Proceedings Article In: ICTSS, pp. 158-173, 2010. @inproceedings{DBLP:conf/pts/Gladisch10,
title = {Test Data Generation for Programs with Quantified First-Order
Logic Specifications},
author = {Christoph Gladisch},
year = {2010},
date = {2010-01-01},
booktitle = {ICTSS},
pages = {158-173},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Gladisch, Christoph; Tyszberowicz, Shmuel; Beckert, Bernhard; Yehudai, Amiram Generating Regression Unit Tests Using a Combination of Verification and Capture & Replay Book Chapter In: Fraser, Gordon; Gargantini, Angelo (Ed.): Tests and Proofs: 4th International Conference, TAP 2010, M'alaga, Spain, July 1-2, 2010. Proceedings, pp. 61–76, Springer Berlin Heidelberg, Berlin, Heidelberg, 2010, ISBN: 978-3-642-13977-2. @inbook{Gladisch2010,
title = {Generating Regression Unit Tests Using a Combination of Verification and Capture \& Replay},
author = {Christoph Gladisch and Shmuel Tyszberowicz and Bernhard Beckert and Amiram Yehudai},
editor = {Fraser, Gordon and Gargantini, Angelo},
url = {http://dx.doi.org/10.1007/978-3-642-13977-2_7},
doi = {10.1007/978-3-642-13977-2_7},
isbn = {978-3-642-13977-2},
year = {2010},
date = {2010-01-01},
booktitle = {Tests and Proofs: 4th International Conference, TAP 2010, M'alaga, Spain, July 1-2, 2010. Proceedings},
pages = {61--76},
publisher = {Springer Berlin Heidelberg},
address = {Berlin, Heidelberg},
keywords = {},
pubstate = {published},
tppubtype = {inbook}
}
|
2008
|
Gladisch, Christoph Verification-based Testing for Full Feasible Branch Coverage Proceedings Article In: Cerone, Antonio (Ed.): Proc. 6th IEEE Int. Conf. Software Engineering and Formal Methods (SEFM'08), IEEE Computer Society Press, 2008, ISBN: 978-0-7695-3437-4. @inproceedings{gladischSEFM2008,
title = {Verification-based Testing for Full Feasible Branch Coverage},
author = {Christoph Gladisch},
editor = {Antonio Cerone},
isbn = {978-0-7695-3437-4},
year = {2008},
date = {2008-00-00},
booktitle = {Proc. 6th IEEE Int. Conf. Software Engineering and Formal Methods (SEFM'08)},
publisher = {IEEE Computer Society Press},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2007
|
Beckert, Bernhard; Gladisch, Christoph White-box Testing by Combining Deduction-based Specification Extraction and Black-box Testing Proceedings Article In: Proceedings of the 1st International Conference on Tests and Proofs, pp. 207–216, Springer-Verlag, Zurich, Switzerland, 2007, ISBN: 3-540-73769-3, 978-3-540-73769-8. @inproceedings{Beckert:2007:WTC:1776119.1776131,
title = {White-box Testing by Combining Deduction-based Specification Extraction and Black-box Testing},
author = {Bernhard Beckert and Christoph Gladisch},
url = {http://dl.acm.org/citation.cfm?id=1776119.1776131},
isbn = {3-540-73769-3, 978-3-540-73769-8},
year = {2007},
date = {2007-01-01},
booktitle = {Proceedings of the 1st International Conference on Tests and Proofs},
pages = {207--216},
publisher = {Springer-Verlag},
address = {Zurich, Switzerland},
series = {TAP'07},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Engel, Christian; Hähnle, Reiner Generating Unit Tests from Formal Proofs Proceedings Article In: Gurevich, Yuri; Meyer, Bertrand (Ed.): Proceedings, 1st International Conference on Tests And Proofs (TAP), Zurich, Switzerland, Springer, 2007. @inproceedings{engelHaehnle07,
title = {Generating Unit Tests from Formal Proofs},
author = {Christian Engel and Reiner H\"{a}hnle},
editor = {Yuri Gurevich and Bertrand Meyer},
year = {2007},
date = {2007-01-01},
booktitle = {Proceedings, 1st International Conference on Tests And Proofs (TAP), Zurich, Switzerland},
volume = {4454},
publisher = {Springer},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2005
|
Darvas, Ádám; Hähnle, Reiner; Sands, Dave A Theorem Proving Approach to Analysis of Secure Information Flow Proceedings Article In: Hutter, Dieter; Ullmann, Markus (Ed.): Proc. 2nd International Conference on Security in Pervasive Computing, pp. 193–209, Springer-Verlag, 2005. @inproceedings{DHS05,
title = {A Theorem Proving Approach to Analysis of Secure Information Flow},
author = {\'{A}d\'{a}m Darvas and Reiner H\"{a}hnle and Dave Sands},
editor = {Dieter Hutter and Markus Ullmann},
url = {http://www.springerlink.com/link.asp?id=rdqa8ejctda3yw64},
year = {2005},
date = {2005-01-01},
booktitle = {Proc. 2nd International Conference on Security in Pervasive Computing},
volume = {3450},
pages = {193--209},
publisher = {Springer-Verlag},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2003
|
Darvas, Ádám; Hähnle, Reiner; Sands, Dave A Theorem Proving Approach to Analysis of Secure Information Flow Proceedings Article In: Gorrieri, Roberto (Ed.): Workshop on Issues in the Theory of Security, WITS, IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS 2003. @inproceedings{DHS03,
title = {A Theorem Proving Approach to Analysis of Secure Information Flow},
author = {\'{A}d\'{a}m Darvas and Reiner H\"{a}hnle and Dave
Sands},
editor = {Roberto Gorrieri},
year = {2003},
date = {2003-01-01},
booktitle = {Workshop on Issues in the Theory of Security, WITS},
organization = {IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|