2016
|
Do, Quoc Huy; Kamburjan, Eduard; Wasser, Nathan Towards Fully Automatic Logic-Based Information Flow Analysis: An Electronic-Voting Case Study Inproceedings Proceedings of the 5th International Conference on Principles of Security and Trust - Volume 9635, pp. 97–115, Springer-Verlag New York, Inc., New York, NY, USA, 2016, ISBN: 978-3-662-49634-3. Links | BibTeX @inproceedings{DoKW16,
title = {Towards Fully Automatic Logic-Based Information Flow Analysis: An Electronic-Voting Case Study},
author = {Quoc Huy Do and Eduard Kamburjan and Nathan Wasser},
url = {http://dx.doi.org/10.1007/978-3-662-49635-0_6},
doi = {10.1007/978-3-662-49635-0_6},
isbn = {978-3-662-49634-3},
year = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the 5th International Conference on Principles of Security and Trust - Volume 9635},
pages = {97--115},
publisher = {Springer-Verlag New York, Inc.},
address = {New York, NY, USA},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2015
|
Do, Quoc Huy; Bubel, Richard; Hähnle, Reiner Exploit Generation for Information Flow Leaks in Object-Oriented Programs Inproceedings ICT Systems Security and Privacy Protection - 30th IFIP TC 11
International Conference, SEC 2015, Hamburg, Germany, May 26-28,
2015, Proceedings, pp. 401–415, 2015. Links | BibTeX @inproceedings{DoBH15,
title = {Exploit Generation for Information Flow Leaks in Object-Oriented Programs},
author = {Quoc Huy Do and Richard Bubel and Reiner H\"{a}hnle},
url = {http://dx.doi.org/10.1007/978-3-319-18467-8_27},
doi = {10.1007/978-3-319-18467-8_27},
year = {2015},
date = {2015-01-01},
booktitle = {ICT Systems Security and Privacy Protection - 30th IFIP TC 11
International Conference, SEC 2015, Hamburg, Germany, May 26-28,
2015, Proceedings},
pages = {401--415},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2014
|
Ahrendt, Wolfgang; Beckert, Bernhard; Bruns, Daniel; Bubel, Richard; Gladisch, Christoph; Grebing, Sarah; Hähnle, Reiner; Hentschel, Martin; Herda, Mihai; Klebanov, Vladimir; Mostowski, Wojciech; Scheben, Christoph; Schmitt, Peter H; Ulbrich, Mattias The KeY Platform for Verification and Analysis of Java Programs Inproceedings Giannakopoulou, Dimitra; Kroening, Daniel (Ed.): Verified Software: Theories, Tools, and Experiments (VSTTE 2014), pp. 1–17, Springer-Verlag, 2014, ISBN: 978-3-642-54107-0. Abstract | Links | BibTeX @inproceedings{AhrendtBeckertBrunsEtAl14,
title = {The KeY Platform for Verification and Analysis of Java Programs},
author = {Wolfgang Ahrendt and Bernhard Beckert and Daniel Bruns and Richard Bubel and
Christoph Gladisch and Sarah Grebing and Reiner H\"{a}hnle and Martin Hentschel and
Mihai Herda and Vladimir Klebanov and Wojciech Mostowski and Christoph Scheben and
Peter H. Schmitt and Mattias Ulbrich},
editor = {Dimitra Giannakopoulou and Daniel Kroening},
url = {http://link.springer.com/chapter/10.1007/978-3-319-12154-3_4},
doi = {10.1007/978-3-319-12154-3_4},
isbn = {978-3-642-54107-0},
year = {2014},
date = {2014-01-01},
booktitle = {Verified Software: Theories, Tools, and Experiments (VSTTE 2014)},
number = {8471},
pages = {1--17},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
abstract = {The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flow security, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flow security, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim. |
2012
|
Gladisch, Christoph Model generation for quantified formulas with application to test data generation Journal Article International Journal on Software Tools for Technology Transfer (STTT), pp. 1-21, 2012, ISSN: 1433-2779, (10.1007/s10009-012-0227-0). Links | BibTeX @article{springerlink:10.1007/s10009-012-0227-0,
title = {Model generation for quantified formulas with application to test data generation},
author = {Christoph Gladisch},
url = {http://dx.doi.org/10.1007/s10009-012-0227-0},
issn = {1433-2779},
year = {2012},
date = {2012-01-01},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
pages = {1-21},
publisher = {Springer Berlin / Heidelberg},
note = {10.1007/s10009-012-0227-0},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
|
2011
|
Beckert, Bernhard; Gladisch, Christoph; Tyszberowicz, Shmuel; Yehudai, Amiram KeYGenU: Combining Verification-Based and Capture and Replay Techniques for Regression Unit Testing Journal Article International Journal of System Assurance Engineering and Management, 2 (2), pp. 97–113, 2011, ISSN: 0976-4348. Abstract | Links | BibTeX @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. |
2010
|
Gladisch, Christoph Test Data Generation for Programs with Quantified First-Order
Logic Specifications Inproceedings ICTSS, pp. 158-173, 2010. BibTeX @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 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. Links | BibTeX @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 Inproceedings 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. BibTeX @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
|
Engel, Christian; Hähnle, Reiner Generating Unit Tests from Formal Proofs Inproceedings Gurevich, Yuri; Meyer, Bertrand (Ed.): Proceedings, 1st International Conference on Tests And Proofs (TAP), Zurich, Switzerland, Springer, 2007. BibTeX @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}
}
|
Beckert, Bernhard; Gladisch, Christoph White-box Testing by Combining Deduction-based Specification Extraction and Black-box Testing Inproceedings 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. Links | BibTeX @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}
}
|