2021
|
Lanzinger, Florian; Weigl, Alexander; Ulbrich, Mattias; Dietl, Werner Scalability and Precision by Combining Expressive Type Systems and Deductive Verification Journal Article In: Proceedings of the ACM on programming languages, vol. 5, no. OOPSLA, pp. Article no: 143, 2021, ISSN: 2475-1421, (46.23.01; LK 01). @article{LanzingerWeiglUlbrich2021_1000139256,
title = {Scalability and Precision by Combining Expressive Type Systems and Deductive Verification},
author = {Florian Lanzinger and Alexander Weigl and Mattias Ulbrich and Werner Dietl},
doi = {10.1145/3485520},
issn = {2475-1421},
year = {2021},
date = {2021-10-01},
journal = {Proceedings of the ACM on programming languages},
volume = {5},
number = {OOPSLA},
pages = {Article no: 143},
publisher = {Association for Computing Machinery (ACM)},
note = {46.23.01; LK 01},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
|
Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang Deductive Verification of Floating-Point Java Programs in KeY Inproceedings In: Groote, Jan Friso; Larsen, Kim Guldstrand (Ed.): 27th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS 2021) held as part
of ETAPS 2021: European Joint Conferences on Theory and Practice
of Software, pp. 242–261, Springer, 2021. @inproceedings{AbbasiSchifflEtAl2021,
title = {Deductive Verification of Floating-Point Java Programs in KeY},
author = {Rosa Abbasi and Jonas Schiffl and Eva Darulova and Mattias Ulbrich and Wolfgang Ahrendt},
editor = {Jan Friso Groote and Kim Guldstrand Larsen},
doi = {10.1007/978-3-030-72013-1_13},
year = {2021},
date = {2021-03-01},
booktitle = {27th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS 2021) held as part
of ETAPS 2021: European Joint Conferences on Theory and Practice
of Software},
volume = {12652},
pages = {242--261},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
abstract = {Deductive verification has been successful in verifying interesting
properties of real-world programs. One notable gap is the limited support
for floating-point reasoning. This is unfortunate, as floating-point
arithmetic is particularly unintuitive to reason about due to rounding as
well as the presence of the special values infinity and `Not a Number' (NaN).
In this paper, we present the first floating-point support in a deductive
verification tool for the Java programming language. Our support in the KeY verifier handles
arithmetic via floating-point decision procedures inside SMT solvers
and transcendental functions via axiomatization.
We evaluate this integration on new benchmarks, and show that this approach
is powerful enough to prove the absence of floating-point special
values---often a prerequisite for further reasoning about numerical
computations---as well as certain functional properties for realistic benchmarks.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Deductive verification has been successful in verifying interesting
properties of real-world programs. One notable gap is the limited support
for floating-point reasoning. This is unfortunate, as floating-point
arithmetic is particularly unintuitive to reason about due to rounding as
well as the presence of the special values infinity and `Not a Number' (NaN).
In this paper, we present the first floating-point support in a deductive
verification tool for the Java programming language. Our support in the KeY verifier handles
arithmetic via floating-point decision procedures inside SMT solvers
and transcendental functions via axiomatization.
We evaluate this integration on new benchmarks, and show that this approach
is powerful enough to prove the absence of floating-point special
values---often a prerequisite for further reasoning about numerical
computations---as well as certain functional properties for realistic benchmarks. |
Pfeifer, Wolfram; Schiffl, Jonas; Ulbrich, Mattias Reconstructing Z3 proofs in KeY: There and back again Inproceedings In: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs : 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021, Online, 13 July 2021 - null, pp. 24–31, Association for Computing Machinery (ACM), 2021, ISBN: 978-1-4503-8543-5. @inproceedings{PfeiferSchifflUlbrich2021,
title = {Reconstructing Z3 proofs in KeY: There and back again},
author = {Wolfram Pfeifer and
Jonas Schiffl and
Mattias Ulbrich},
doi = {10.1145/3464971.3468421},
isbn = {978-1-4503-8543-5},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs : 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021, Online, 13 July 2021 - null},
pages = {24--31},
publisher = {Association for Computing Machinery (ACM)},
series = {ACM Conferences},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2020
|
Steinhöfel, Dominic Abstract Execution: Automatically Proving Infinitely Many Programs PhD Thesis Darmstadt University of Technology, Germany, 2020. @phdthesis{DBLP:phd/dnb/Steinhofel20,
title = {Abstract Execution: Automatically Proving Infinitely Many Programs},
author = {Dominic Steinh\"{o}fel},
url = {http://tuprints.ulb.tu-darmstadt.de/8540/},
year = {2020},
date = {2020-01-01},
school = {Darmstadt University of Technology, Germany},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}
|
Hähnle, Reiner; Tabar, Asmae Heydari; Mazaheri, Arya; Norouzi, Mohammad; Steinhöfel, Dominic; Wolf, Felix Safer Parallelization Inproceedings In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation:
Engineering Principles - 9th International Symposium on Leveraging
Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October
20-30, 2020, Proceedings, Part II, pp. 117–137, Springer, 2020. @inproceedings{DBLP:conf/isola/HahnleTMNS020,
title = {Safer Parallelization},
author = {Reiner H\"{a}hnle and Asmae Heydari Tabar and Arya Mazaheri and Mohammad Norouzi and Dominic Steinh\"{o}fel and Felix Wolf},
editor = {Tiziana Margaria and Bernhard Steffen},
url = {https://doi.org/10.1007/978-3-030-61470-6_8},
doi = {10.1007/978-3-030-61470-6_8},
year = {2020},
date = {2020-01-01},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation:
Engineering Principles - 9th International Symposium on Leveraging
Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October
20-30, 2020, Proceedings, Part II},
volume = {12477},
pages = {117--137},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Ahrendt, Wolfgang; Bubel, Richard Functional Verification of Smart Contracts via Strong Data Integrity Inproceedings In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation:
Applications - 9th International Symposium on Leveraging Applications
of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020,
Proceedings, Part III, pp. 9–24, Springer, 2020. @inproceedings{DBLP:conf/isola/AhrendtB20,
title = {Functional Verification of Smart Contracts via Strong Data Integrity},
author = {Wolfgang Ahrendt and Richard Bubel},
editor = {Tiziana Margaria and Bernhard Steffen},
url = {https://doi.org/10.1007/978-3-030-61467-6_2},
doi = {10.1007/978-3-030-61467-6_2},
year = {2020},
date = {2020-01-01},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation:
Applications - 9th International Symposium on Leveraging Applications
of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020,
Proceedings, Part III},
volume = {12478},
pages = {9--24},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2019
|
Hentschel, Martin; Bubel, Richard; Hähnle, Reiner The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more Journal Article In: International Journal on Software Tools for Technology Transfer, 2019, ISSN: 1433-2787. @article{Hentschel2018,
title = {The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more},
author = {Martin Hentschel and Richard Bubel and Reiner H\"{a}hnle},
url = {https://doi.org/10.1007/s10009-018-0490-9},
doi = {10.1007/s10009-018-0490-9},
issn = {1433-2787},
year = {2019},
date = {2019-09-01},
journal = {International Journal on Software Tools for Technology Transfer},
abstract = {The Symbolic Execution Debugger (SED), is an extension of the debug platform for interactive debuggers based on symbolic execution. The SED comes with a static symbolic execution engine for sequential programs, but any third-party symbolic execution engine can be integrated into the SED. An interactive debugger based on symbolic execution allows one like a traditional debugger to locate defects in the source code. The difference is that all feasible execution paths are explored at once, and thus there is no need to know input values resulting in an execution that exhibits the failure. In addition, such a debugger can be used in code reviews and to guide and present results of an analysis based on symbolic execution such as, in our case, correctness proofs. Experimental evaluations proved that the SED increases the effectiveness of code reviews and proof understanding tasks.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The Symbolic Execution Debugger (SED), is an extension of the debug platform for interactive debuggers based on symbolic execution. The SED comes with a static symbolic execution engine for sequential programs, but any third-party symbolic execution engine can be integrated into the SED. An interactive debugger based on symbolic execution allows one like a traditional debugger to locate defects in the source code. The difference is that all feasible execution paths are explored at once, and thus there is no need to know input values resulting in an execution that exhibits the failure. In addition, such a debugger can be used in code reviews and to guide and present results of an analysis based on symbolic execution such as, in our case, correctness proofs. Experimental evaluations proved that the SED increases the effectiveness of code reviews and proof understanding tasks. |
Ahrendt, Wolfgang; Bubel, Richard; Ellul, Joshua; Pace, Gordon J; Pardo, Raul; Rebiscoul, Vincent; Schneider, Gerardo Verification of Smart Contract Business Logic - Exploiting a Java
Source Code Verifier Inproceedings In: Hojjat, Hossein; Massink, Mieke (Ed.): Fundamentals of Software Engineering - 8th International Conference,
FSEN 2019, Tehran, Iran, May 1-3, 2019, Revised Selected Papers, pp. 228–243, Springer, 2019. @inproceedings{DBLP:conf/fsen/AhrendtBEPPRS19,
title = {Verification of Smart Contract Business Logic - Exploiting a Java
Source Code Verifier},
author = {Wolfgang Ahrendt and Richard Bubel and Joshua Ellul and Gordon J Pace and Raul Pardo and Vincent Rebiscoul and Gerardo Schneider},
editor = {Hossein Hojjat and Mieke Massink},
url = {https://doi.org/10.1007/978-3-030-31517-7_16},
doi = {10.1007/978-3-030-31517-7_16},
year = {2019},
date = {2019-01-01},
booktitle = {Fundamentals of Software Engineering - 8th International Conference,
FSEN 2019, Tehran, Iran, May 1-3, 2019, Revised Selected Papers},
volume = {11761},
pages = {228--243},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Steinhöfel, Dominic; Hähnle, Reiner Abstract Execution Inproceedings In: ter Beek, Maurice H; McIver, Annabelle; é, Jos (Ed.): Formal Methods - The Next 30 Years - Third World Congress, FM 2019,
Porto, Portugal, October 7-11, 2019, Proceedings, pp. 319–336, Springer, 2019. @inproceedings{DBLP:conf/fm/SteinhofelH19,
title = {Abstract Execution},
author = {Dominic Steinh\"{o}fel and Reiner H\"{a}hnle},
editor = {Maurice H ter Beek and Annabelle McIver and Jos \'{e}},
url = {https://doi.org/10.1007/978-3-030-30942-8_20},
doi = {10.1007/978-3-030-30942-8_20},
year = {2019},
date = {2019-01-01},
booktitle = {Formal Methods - The Next 30 Years - Third World Congress, FM 2019,
Porto, Portugal, October 7-11, 2019, Proceedings},
volume = {11800},
pages = {319--336},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Steinhöfel, Dominic; Hähnle, Reiner The Trace Modality Inproceedings In: Baltag, Alexandru; Barbosa, Luis S (Ed.): 2nd Workshop on Dynamic Logic: New Trends and Applications, Springer, Porto, Portugal, 2019, (Accepted, in print.). @inproceedings{dali2019,
title = {The Trace Modality},
author = {Dominic Steinh\"{o}fel and Reiner H\"{a}hnle},
editor = {Alexandru Baltag and Luis S Barbosa},
year = {2019},
date = {2019-01-01},
booktitle = {2nd Workshop on Dynamic Logic: New Trends and Applications},
publisher = {Springer},
address = {Porto, Portugal},
series = {Lecture Notes in Computer Science},
note = {Accepted, in print.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Bubel, Richard; Hähnle, Reiner; Tabar, Asmae Heydari A Program Logic For Dependence Analysis Inproceedings In: Ahrendt, Wolfgang; Tarifa, Silvia Lizeth Tapia (Ed.): Integrated Formal Methods, 15th International Conference,
iFM, Bergen, Norway, Springer, 2019. @inproceedings{BHT19,
title = {A Program Logic For Dependence Analysis},
author = {Richard Bubel and Reiner H\"{a}hnle and Asmae Heydari Tabar},
editor = {Wolfgang Ahrendt and Silvia Lizeth Tapia Tarifa},
year = {2019},
date = {2019-01-01},
booktitle = {Integrated Formal Methods, 15th International Conference,
iFM, Bergen, Norway},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Grebing, Sarah Caecilia User Interaction in Deductive Interactive Program Verification PhD Thesis Karlsruhe Institute of Technology, 2019. @phdthesis{Grebing19,
title = {User Interaction in Deductive Interactive Program Verification},
author = {Sarah Caecilia Grebing},
doi = {10.5445/IR/1000099121},
year = {2019},
date = {2019-01-01},
school = {Karlsruhe Institute of Technology},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}
|
Grebing, Sarah; Klamroth, Jonas; Ulbrich, Mattias Seamless Interactive Program Verification Inproceedings In: 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019), Springer Publishing, New York City, USA, 2019, (To appear). @inproceedings{GrebingKlamrothUlbrich19,
title = {Seamless Interactive Program Verification},
author = {Sarah Grebing and Jonas Klamroth and Mattias Ulbrich},
year = {2019},
date = {2019-01-01},
booktitle = {11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019)},
publisher = {Springer Publishing},
address = {New York City, USA},
series = {LNCS},
note = {To appear},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2018
|
Beckert, Bernhard; Herda, Mihai; Kobischke, Stefan; Ulbrich, Mattias Towards a Notion of Coverage for Incomplete Program-Correctness Proofs Inproceedings In: Margaria, Tiziana; Steffen, Bernhard (Ed.): 8th International Symposium on Leveraging Applications of Formal Methods,
Verification and Validation (ISoLA 2018), pp. 53–63, Springer, 2018. @inproceedings{BeckertHerdaEtAl18,
title = {Towards a Notion of Coverage for Incomplete Program-Correctness Proofs},
author = {Bernhard Beckert and Mihai Herda and Stefan Kobischke and Mattias Ulbrich},
editor = {Tiziana Margaria and Bernhard Steffen},
url = {https://doi.org/10.1007/978-3-030-03421-4_4},
doi = {10.1007/978-3-030-03421-4_4},
year = {2018},
date = {2018-11-01},
booktitle = {8th International Symposium on Leveraging Applications of Formal Methods,
Verification and Validation (ISoLA 2018)},
volume = {11245},
pages = {53--63},
publisher = {Springer},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Steinhöfel, Dominic; Hähnle, Reiner Modular, Correct Compilation with Automatic Soundness Proofs Inproceedings In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation. Modeling, pp. 424–447, Springer International Publishing, Cham, 2018, ISSN: 0302-9743. @inproceedings{steinhoefel-haehnle-2018,
title = {Modular, Correct Compilation with Automatic Soundness Proofs},
author = {Dominic Steinh\"{o}fel and Reiner H\"{a}hnle},
editor = {Tiziana Margaria and Bernhard Steffen},
url = {https://link.springer.com/chapter/10.1007%2F978-3-030-03418-4_25},
doi = {10.1007/978-3-030-03418-4_25},
issn = {0302-9743},
year = {2018},
date = {2018-01-01},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Modeling},
volume = {11244},
pages = {424--447},
publisher = {Springer International Publishing},
address = {Cham},
series = {Lecture Notes in Computer Science},
abstract = {Formal verification of compiler correctness requires substantial effort. A particular challenge is lack of modularity and automation. Any change or update to the compiler can render existing proofs obsolete and cause considerable manual proof effort. We propose a framework for automatically proving the correctness of compilation rules based on simultaneous symbolic execution for the source and target language. The correctness of the whole system follows from the correctness of each compilation rule. To support a new source or target language it is sufficient to formalize that language in terms of symbolic execution, while the corresponding formalization of its counterpart can be re-used. The correctness of translation rules can be checked automatically. Our approach is based on a reduction of correctness assertions to formulas in a program logic capable of symbolic execution of abstract programs. We instantiate the framework for compilation from Java to LLVM IR and provide a symbolic execution system for a subset of LLVM IR.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Formal verification of compiler correctness requires substantial effort. A particular challenge is lack of modularity and automation. Any change or update to the compiler can render existing proofs obsolete and cause considerable manual proof effort. We propose a framework for automatically proving the correctness of compilation rules based on simultaneous symbolic execution for the source and target language. The correctness of the whole system follows from the correctness of each compilation rule. To support a new source or target language it is sufficient to formalize that language in terms of symbolic execution, while the corresponding formalization of its counterpart can be re-used. The correctness of translation rules can be checked automatically. Our approach is based on a reduction of correctness assertions to formulas in a program logic capable of symbolic execution of abstract programs. We instantiate the framework for compilation from Java to LLVM IR and provide a symbolic execution system for a subset of LLVM IR. |
Schiffl, Jonas Specification and Verification of Hyperledger Fabric Chaincode Masters Thesis Karlsruhe Institute of Technology, Karlsruhe, Germany, 2018. @mastersthesis{SchifflMSc2018,
title = {Specification and Verification of Hyperledger Fabric Chaincode},
author = {Jonas Schiffl},
year = {2018},
date = {2018-01-01},
address = {Karlsruhe, Germany},
school = {Karlsruhe Institute of Technology},
keywords = {},
pubstate = {published},
tppubtype = {mastersthesis}
}
|
Beckert, Bernhard; Bischof, Simon; Herda, Mihai; Kirsten, Michael; Büning, Marko Kleine Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control Inproceedings In: Sun, Jing; Sun, Meng (Ed.): 20th International Conference on Formal Engineering
Methods - Formal Methods and Software Engineering
(ICFEM 2018), pp. 284–300, Springer, Gold Coast, QLD, Australia, 2018. @inproceedings{BeckertBischofEA2018,
title = {Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control},
author = {Bernhard Beckert and Simon Bischof and Mihai Herda and Michael Kirsten and Marko Kleine B\"{u}ning},
editor = {Jing Sun and Meng Sun},
doi = {10.1007/978-3-030-02450-5_17},
year = {2018},
date = {2018-01-01},
booktitle = {20th International Conference on Formal Engineering
Methods - Formal Methods and Software Engineering
(ICFEM 2018)},
volume = {11232},
pages = {284--300},
publisher = {Springer},
address = {Gold Coast, QLD, Australia},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Greiner, Simon A Framework for Non-Interference in Component-Based
Systems PhD Thesis Karlsruhe Institute of Technology, 2018. @phdthesis{Greiner2018PhD,
title = {A Framework for Non-Interference in Component-Based
Systems},
author = {Simon Greiner},
doi = {10.5445/IR/1000082042},
year = {2018},
date = {2018-01-01},
school = {Karlsruhe Institute of Technology},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}
|
Grebing, Sarah; Luong, An Thuy Tien; Weigl, Alexander Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons
Learned Inproceedings In: Jamnik, Mateja; Lüth, Christoph (Ed.): 13th International Workshop on User Interfaces for Theorem Provers (UITP 2018), 2018, (To appear, %snip pdf=https://formal.iti.kit.edu/~grebing/pub/uitp2018.pdf). @inproceedings{uitp2018,
title = {Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons
Learned},
author = {Sarah Grebing and An Thuy Tien Luong and Alexander Weigl},
editor = {Mateja Jamnik and Christoph L\"{u}th},
year = {2018},
date = {2018-01-01},
booktitle = {13th International Workshop on User Interfaces for Theorem Provers (UITP 2018)},
note = {To appear, %snip pdf=https://formal.iti.kit.edu/~grebing/pub/uitp2018.pdf},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2017
|
E., Max; Hecker, Martin; Greiner, Simon; Bao, Kaibin; Yurchenko, Kateryna Model-Driven Specification and Analysis of Confidentiality in Component-Based Systems Technical Report Department of Informatics, Karlsruhe Institute of Technology Karlsruhe, no. 2017,12, 2017, ISSN: 2190-4782. @techreport{Kramer2017,
title = {Model-Driven Specification and Analysis of Confidentiality in Component-Based Systems},
author = {Max E. and Martin Hecker and Simon Greiner and Kaibin Bao and Kateryna Yurchenko},
doi = {10.5445/IR/1000076957},
issn = {2190-4782},
year = {2017},
date = {2017-12-01},
number = {2017,12},
address = {Karlsruhe},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
|
Schmitt, Peter H. A Mechanizable First-Order Theory of Ordinals Inproceedings In: Schmidt, Renate A.; Nalon, Claudia (Ed.): Automated Reasoning with Analytic Tableaux and Related Methods - 26th
International Conference, {TABLEAUX} 2017, Brasilia, Brazil,
September 25-28, 2017, Proceedings, pp. 331–346, Springer, 2017, ISBN: 978-3-319-66901-4. @inproceedings{Schmitt2017,
title = {A Mechanizable First-Order Theory of Ordinals},
author = {Peter H. Schmitt},
editor = {Renate A. Schmidt and Claudia Nalon},
url = {https://www.key-project.org/papers/ordinal-numbers},
doi = {10.1007/978-3-319-66902-1_20},
isbn = {978-3-319-66901-4},
year = {2017},
date = {2017-09-06},
urldate = {2017-09-06},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 26th
International Conference, {TABLEAUX} 2017, Brasilia, Brazil,
September 25-28, 2017, Proceedings},
volume = {10501},
pages = {331--346},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
abstract = {We present a first-order theory of ordinals without resorting to set theory. The theory is implemented in the
KeY program verification system which is in turn used to prove termination of a Java program computing
the Goodstein sequences.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We present a first-order theory of ordinals without resorting to set theory. The theory is implemented in the
KeY program verification system which is in turn used to prove termination of a Java program computing
the Goodstein sequences. |
Beckert, Bernhard; Schiffl, Jonas; Schmitt, Peter H.; Ulbrich, Mattias Proving JDK's Dual Pivot Quicksort Correct Inproceedings In: 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), 2017, (To appear ). @inproceedings{BeckertEtAl2017a,
title = {Proving JDK's Dual Pivot Quicksort Correct},
author = {Bernhard Beckert and Jonas Schiffl and Peter H. Schmitt and Mattias Ulbrich},
url = {https://formal.iti.kit.edu/biblio/?lang=en\&key=BeckertEtAl2017a},
year = {2017},
date = {2017-07-22},
booktitle = {9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017)},
note = {To appear },
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
de Gouw, Stijn; de Boer, Frank S; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic Verifying OpenJDK's Sort Method for Generic Collections Journal Article In: Journal of Automated Reasoning, 2017, ISSN: 1573-0670. @article{deGouw2017,
title = {Verifying OpenJDK's Sort Method for Generic Collections},
author = {Stijn de Gouw and Frank S de Boer and Richard Bubel and Reiner H\"{a}hnle and Jurriaan Rot and Dominic Steinh\"{o}fel},
url = {https://doi.org/10.1007/s10817-017-9426-4},
doi = {10.1007/s10817-017-9426-4},
issn = {1573-0670},
year = {2017},
date = {2017-01-01},
journal = {Journal of Automated Reasoning},
abstract = {TimSort is the main sorting algorithm provided by the Java standard library and many other programming frameworks. Our original goal was functional verification of TimSort with mechanical proofs. However, during our verification attempt we discovered a bug which causes the implementation to crash by an uncaught exception. In this paper, we identify conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise performance. We formally specify the new version and verify termination and the absence of exceptions including the bug. This verification is carried out mechanically with KeY, a state-of-the-art interactive verification tool for Java. We provide a detailed description and analysis of the proofs. The complexity of the proofs required extensions and new capabilities in KeY, including symbolic state merging.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
TimSort is the main sorting algorithm provided by the Java standard library and many other programming frameworks. Our original goal was functional verification of TimSort with mechanical proofs. However, during our verification attempt we discovered a bug which causes the implementation to crash by an uncaught exception. In this paper, we identify conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise performance. We formally specify the new version and verify termination and the absence of exceptions including the bug. This verification is carried out mechanically with KeY, a state-of-the-art interactive verification tool for Java. We provide a detailed description and analysis of the proofs. The complexity of the proofs required extensions and new capabilities in KeY, including symbolic state merging. |
Do, Quoc Huy; Bubel, Richard; Hähnle, Reiner Inferring Secrets by Guided Experiments Inproceedings In: Hung, Dang Van; Kapur, Deepak (Ed.): Theoretical Aspects of Computing -- ICTAC 2017: 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings, pp. 269–287, Springer International Publishing, Cham, 2017. @inproceedings{Do2017,
title = {Inferring Secrets by Guided Experiments},
author = {Quoc Huy Do and Richard Bubel and Reiner H\"{a}hnle},
editor = {Dang Van Hung and Deepak Kapur},
url = {https://doi.org/10.1007/978-3-319-67729-3_16},
doi = {10.1007/978-3-319-67729-3_16},
year = {2017},
date = {2017-01-01},
booktitle = {Theoretical Aspects of Computing -- ICTAC 2017: 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings},
pages = {269--287},
publisher = {Springer International Publishing},
address = {Cham},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Steinhöfel, Dominic; Wasser, Nathan A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows Inproceedings In: Polikarpova, Nadia; Schneider, Steve (Ed.): Integrated Formal Methods - 13th International Conference, IFM 2017,
Turin, Italy, September 20-22, 2017, Proceedings, pp. 279–294, Springer, 2017. @inproceedings{DBLP:conf/ifm/SteinhofelW17,
title = {A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows},
author = {Dominic Steinh\"{o}fel and Nathan Wasser},
editor = {Nadia Polikarpova and Steve Schneider},
url = {https://doi.org/10.1007/978-3-319-66845-1_18},
doi = {10.1007/978-3-319-66845-1_18},
year = {2017},
date = {2017-01-01},
booktitle = {Integrated Formal Methods - 13th International Conference, IFM 2017,
Turin, Italy, September 20-22, 2017, Proceedings},
volume = {10510},
pages = {279--294},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|