2013
|
Beckert, Bernhard; Bruns, Daniel Dynamic Logic with Trace Semantics Inproceedings Bonacina, Maria Paola (Ed.): 24th International Conference on Automated Deduction (CADE-24), pp. 315–329, Springer-Verlag, 2013, ISBN: 978-3-642-38573-5. Abstract | BibTeX | Links: @inproceedings{BeckertBruns13,
title = {Dynamic Logic with Trace Semantics},
author = {Bernhard Beckert and Daniel Bruns},
editor = {Maria Paola Bonacina},
url = {http://link.springer.com/chapter/10.1007/978-3-642-38574-2_22},
doi = {10.1007/978-3-642-38574-2_22},
isbn = {978-3-642-38573-5},
year = {2013},
date = {2013-01-01},
booktitle = {24th International Conference on Automated Deduction (CADE-24)},
volume = {7898},
pages = {315--329},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
abstract = {Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic~(DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for proving functional and information-flow properties in concurrent programs, among other applications.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic~(DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for proving functional and information-flow properties in concurrent programs, among other applications. |
Gladisch, Christoph; Tyszberowicz, Shmuel Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking Inproceedings de Moura, Leonardo; Iyoda, Juliano (Ed.): Brazilian Symposium on Formal Methods (SBMF), Springer, 2013. BibTeX @inproceedings{gladischTyszberowicz2013,
title = {Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking},
author = {Christoph Gladisch and Shmuel Tyszberowicz},
editor = {Leonardo de Moura and Juliano Iyoda},
year = {2013},
date = {2013-01-01},
booktitle = {Brazilian Symposium on Formal Methods (SBMF)},
volume = {8195},
publisher = {Springer},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Kirsten, Michael Proving Well-Definedness of JML Specifications with KeY Masters Thesis ITI Schmitt, Karlsruhe Institute of Technology, 2013. Abstract | BibTeX @mastersthesis{KirstenStA2013,
title = {Proving Well-Definedness of JML Specifications with KeY},
author = {Michael Kirsten},
year = {2013},
date = {2013-01-01},
school = {ITI Schmitt, Karlsruhe Institute of Technology},
abstract = {Specification methods in formal program verification enable the enhancement of source
code with formal annotations as to formally specify the behaviour of a program. This is
a popular way in order to subsequently prove software to be reliable and meet certain
requirements, which is crucial for many applications and gains even more importance in
modern society. The annotations can be taken as a contract, which then can be verified
guaranteeing the specified program element \textendash as a receiver \textendash to fulfil this contract with
its caller. However, these functional contracts can be problematic for partial functions,
e.g. a division, as certain cases may be undefined, as in this example a division by zero.
Modern programming languages such as Java handle undefined behaviour by casting an exception.
There are several approaches to handle a potential undefinedness of specifications. In
this thesis, we chose one which automatically generates formal proof obligations ensuring
that undefined specification expressions will not be evaluated.
Within this work, we elaborate on so-called Well-Definedness Checks dealing with undefinedness
occurring in specifications of the modelling language JML/JML* in the
KeY System, which is a formal software development tool providing mechanisms to
deductively prove the before mentioned contracts. Advantages and delimitations are
discussed and, furthermore, precise definitions as well as a fully functional implementation
within KeY are given. Our work covers the major part of the specification elements
currently supported by KeY, on the higher level including class invariants, model fields,
method contracts, loop statements and block contracts. The process of checking the
well-definedness of a specification forms a preliminary step before the actual proof and
rejects undefined specifications. We further contribute by giving a choice between two
different semantics, both bearing different advantages and disadvantages. The thesis also
includes an extensive case study analysing many examples and measuring the performance
of the implemented Well-Definedness Checks.},
type = {Studienarbeit},
keywords = {},
pubstate = {published},
tppubtype = {mastersthesis}
}
Specification methods in formal program verification enable the enhancement of source
code with formal annotations as to formally specify the behaviour of a program. This is
a popular way in order to subsequently prove software to be reliable and meet certain
requirements, which is crucial for many applications and gains even more importance in
modern society. The annotations can be taken as a contract, which then can be verified
guaranteeing the specified program element – as a receiver – to fulfil this contract with
its caller. However, these functional contracts can be problematic for partial functions,
e.g. a division, as certain cases may be undefined, as in this example a division by zero.
Modern programming languages such as Java handle undefined behaviour by casting an exception.
There are several approaches to handle a potential undefinedness of specifications. In
this thesis, we chose one which automatically generates formal proof obligations ensuring
that undefined specification expressions will not be evaluated.
Within this work, we elaborate on so-called Well-Definedness Checks dealing with undefinedness
occurring in specifications of the modelling language JML/JML* in the
KeY System, which is a formal software development tool providing mechanisms to
deductively prove the before mentioned contracts. Advantages and delimitations are
discussed and, furthermore, precise definitions as well as a fully functional implementation
within KeY are given. Our work covers the major part of the specification elements
currently supported by KeY, on the higher level including class invariants, model fields,
method contracts, loop statements and block contracts. The process of checking the
well-definedness of a specification forms a preliminary step before the actual proof and
rejects undefined specifications. We further contribute by giving a choice between two
different semantics, both bearing different advantages and disadvantages. The thesis also
includes an extensive case study analysing many examples and measuring the performance
of the implemented Well-Definedness Checks. |
2012
|
Ulbrich, Mattias; Geilmann, Ulrich; Ghazi, Aboubakr Achraf El; Taghdiri, Mana A Proof Assistant for Alloy Specifications Inproceedings 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 422-436, 2012. BibTeX @inproceedings{ulbrich-geilmann-elghazi-taghdiri-tacas2012,
title = {A Proof Assistant for Alloy Specifications},
author = {Mattias Ulbrich and Ulrich Geilmann and Aboubakr Achraf El Ghazi and Mana Taghdiri},
year = {2012},
date = {2012-03-01},
booktitle = {18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
pages = {422-436},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Beckert, Bernhard; Bruns, Daniel Formal Semantics of Model Fields in Annotation-based Specifications Inproceedings Glimm, Birte; Krüger, Antonio (Ed.): KI 2012: Advances in Artificial Intelligence, pp. 13–24, Springer-Verlag, 2012, ISBN: 978-3-642-33346-0. Abstract | BibTeX | Links: @inproceedings{BeckertBruns12,
title = {Formal Semantics of Model Fields in Annotation-based Specifications},
author = {Bernhard Beckert and Daniel Bruns},
editor = {Birte Glimm and Antonio Kr\"{u}ger},
url = {http://link.springer.com/chapter/10.1007/978-3-642-33347-7_2},
isbn = {978-3-642-33346-0},
year = {2012},
date = {2012-01-01},
booktitle = {KI 2012: Advances in Artificial Intelligence},
volume = {7526},
pages = {13--24},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
abstract = {It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification and verification, model fields are a common means for those goals. However, it remains a challenge to provide a well-founded formal semantics for the general case in which the abstraction relation defining a model field is non-functional. In this paper, we discuss and compare several possibilities for defining model field semantics, and we give a complete formal semantics for the general case. Our analysis and the proposed semantics is based on a generalization of Hilbert's $varepsilon$~terms.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification and verification, model fields are a common means for those goals. However, it remains a challenge to provide a well-founded formal semantics for the general case in which the abstraction relation defining a model field is non-functional. In this paper, we discuss and compare several possibilities for defining model field semantics, and we give a complete formal semantics for the general case. Our analysis and the proposed semantics is based on a generalization of Hilbert's $varepsilon$~terms. |
Beckert, Bernhard; Bruns, Daniel Dynamic Trace Logic: Definition and Proofs Technical Report Department of Informatics, Karlsruhe Institute of Technology (2012,10), 2012, ISSN: 2190-4782, (A revised version replacing an unsound rule is available at
http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf). Abstract | BibTeX | Links: @techreport{BeckertBruns12a,
title = {Dynamic Trace Logic: Definition and Proofs},
author = {Bernhard Beckert and Daniel Bruns},
url = {http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf,
http://digbib.ubka.uni-karlsruhe.de/volltexte/1000028184},
issn = {2190-4782},
year = {2012},
date = {2012-01-01},
number = {2012,10},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
abstract = {Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic~(DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for functional verification of concurrent programs and for proving information-flow properties among other applications.},
note = {A revised version replacing an unsound rule is available at
http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic~(DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for functional verification of concurrent programs and for proving information-flow properties among other applications. |
Bruns, Daniel Eine formale Semantik für die Java Modeling Language Journal Article Informatik-Spektrum, 35 (1), pp. 45–49, 2012. BibTeX | Links: @article{Bruns12,
title = {Eine formale Semantik f\"{u}r die Java Modeling Language},
author = {Daniel Bruns},
url = {http://www.springerlink.com/content/b503j663353x482w/},
doi = {10.1007/s00287-011-0532-0},
year = {2012},
date = {2012-01-01},
journal = {Informatik-Spektrum},
volume = {35},
number = {1},
pages = {45--49},
publisher = {Springer-Verlag},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
|
Beckert, Bernhard; Bruns, Daniel; Küsters, Ralf; Scheben, Christoph; Schmitt, Peter H; Truderung, Tomasz The KeY Approach for the Cryptographic Verification of Java Programs: A Case Study Technical Report Department of Informatics, Karlsruhe Institute of Technology (2012,8), 2012. Abstract | BibTeX | Links: @techreport{BeckertBrunsKuestersEtAl12,
title = {The KeY Approach for the Cryptographic Verification of Java Programs: A Case Study},
author = {Bernhard Beckert and Daniel Bruns and Ralf K\"{u}sters and Christoph Scheben and Peter H. Schmitt and Tomasz Truderung},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000027497},
year = {2012},
date = {2012-01-01},
number = {2012,8},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
abstract = {In this paper, we report on an ongoing case study in which we use the KeY tool, a theorem prover for checking functional correctness and noninterference properties of Java programs, to establish computational indistinguishability for a simple Java program that involves clients sending encrypted messages over an untrusted network to a server. The analysis uses a general framework, recently proposed by K"usters et al., which enables program analysis tools, such as KeY, that can check (standard) noninterference properties for Java programs to establish computational indistinguishability properties.},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
In this paper, we report on an ongoing case study in which we use the KeY tool, a theorem prover for checking functional correctness and noninterference properties of Java programs, to establish computational indistinguishability for a simple Java program that involves clients sending encrypted messages over an untrusted network to a server. The analysis uses a general framework, recently proposed by K"usters et al., which enables program analysis tools, such as KeY, that can check (standard) noninterference properties for Java programs to establish computational indistinguishability properties. |
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). BibTeX | Links: @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}
}
|
Thüm, Thomas; Schaefer, Ina; Apel, Sven; Hentschel, Martin Family-Based Deductive Verification of Software Product Lines Inproceedings Proceedings of the 11th International Conference on Generative Programming and Component Engineering, pp. 11-20, ACM, Dresden, Germany, 2012, ISBN: 978-1-4503-1129-8. Abstract | BibTeX @inproceedings{ TUD-CS-2012-0355,
title = {Family-Based Deductive Verification of Software Product Lines},
author = {Thomas Th\"{u}m and Ina Schaefer and Sven Apel and Martin Hentschel},
isbn = {978-1-4503-1129-8},
year = {2012},
date = {2012-01-01},
booktitle = {Proceedings of the 11th International Conference on Generative Programming and Component Engineering},
pages = {11-20},
publisher = {ACM},
address = {Dresden, Germany},
series = {GPCE '12},
abstract = {A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially if human effort is required (e.g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used of-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85 %.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially if human effort is required (e.g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used of-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85 %. |
2011
|
Ulbrich, Mattias; Geilmann, Ulrich; Ghazi, Aboubakr Achraf El; Taghdiri, Mana On Proving Alloy Specifications using KeY Technical Report Karlsruhe Institute of Technology (2011-37), 2011. BibTeX @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 International Journal of System Assurance Engineering and Management, 2 (2), pp. 97–113, 2011, ISSN: 0976-4348. Abstract | BibTeX | Links: @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 Inproceedings Beckert, Bernhard; Marché, Claude (Ed.): Revised Selected Papers, International Conference on Formal
Verification of Object-Oriented Software (FoVeOOS 2010), pp. 138–152, Springer, 2011. BibTeX @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 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. BibTeX | Links: @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
|
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. BibTeX | Links: @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 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}
}
|
2005
|
Darvas, Ádám; Hähnle, Reiner; Sands, Dave A Theorem Proving Approach to Analysis of Secure Information Flow Inproceedings Hutter, Dieter; Ullmann, Markus (Ed.): Proc. 2nd International Conference on Security in Pervasive Computing, pp. 193–209, Springer-Verlag, 2005. BibTeX | Links: @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 Inproceedings Gorrieri, Roberto (Ed.): Workshop on Issues in the Theory of Security, WITS, IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS 2003. BibTeX @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}
}
|