2022
|
Klamroth, Jonas; Lanzinger, Florian; Pfeifer, Wolfram; Ulbrich, Mattias The Karlsruhe Java Verification Suite Book Chapter In: Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Johnsen, Einar Broch (Ed.): The Logic of Software. A Tasting Menu of Formal Methods:
Essays Dedicated to Reiner Hähnle on the Occasion of
His 60th Birthday, pp. 290–312, Springer International Publishing, 2022, ISBN: 978-3-031-08166-8. @inbook{KlamrothEtAl2022,
title = {The Karlsruhe Java Verification Suite},
author = {Jonas Klamroth and Florian Lanzinger and Wolfram Pfeifer and Mattias Ulbrich},
editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Einar Broch Johnsen},
url = {https://doi.org/10.1007/978-3-031-08166-8_14},
doi = {10.1007/978-3-031-08166-8_14},
isbn = {978-3-031-08166-8},
year = {2022},
date = {2022-07-01},
booktitle = {The Logic of Software. A Tasting Menu of Formal Methods:
Essays Dedicated to Reiner H\"{a}hnle on the Occasion of
His 60th Birthday},
pages = {290--312},
publisher = {Springer International Publishing},
keywords = {},
pubstate = {published},
tppubtype = {inbook}
}
|
Boer, Martin; Gouw, Stijn; Klamroth, Jonas; Jung, Christian; Ulbrich, Mattias; Weigl, Alexander Formal Specification and Verification of JDK’s Identity Hash Map Implementation Proceedings Article In: Beek, Maurice H.; Monahan, Rosemary (Ed.): 17th International Conference on integrated Formal Methods (iFM 2022), pp. 45–62, Springer, 2022, ISBN: 978-3-031-07727-2. @inproceedings{BoerGouwKlamroth2022_1000148092,
title = {Formal Specification and Verification of JDK’s Identity Hash Map Implementation},
author = {Martin Boer and Stijn Gouw and Jonas Klamroth and Christian Jung and Mattias Ulbrich and Alexander Weigl},
editor = {Maurice H. Beek and Rosemary Monahan},
doi = {10.1007/978-3-031-07727-2_4},
isbn = {978-3-031-07727-2},
year = {2022},
date = {2022-06-01},
booktitle = {17th International Conference on integrated Formal Methods (iFM 2022)},
volume = {13274},
pages = {45--62},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Krämer, Jonas; Blatter, Lionel; Darulova, Eva; Ulbrich, Mattias Inferring Interval-Valued Floating-Point Preconditions Proceedings Article In: Fisman, Dana; Rosu, Grigore (Ed.): 28th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS 2022),
held as part of ETAPS 2022: European Joint Conferences
on Theory and Practice of Software, pp. 303–321, Springer, 2022. @inproceedings{KramerBDDUlbrich22,
title = {Inferring Interval-Valued Floating-Point Preconditions},
author = {Jonas Kr\"{a}mer and Lionel Blatter and Eva Darulova and Mattias Ulbrich},
editor = {Dana Fisman and Grigore Rosu},
url = {https://doi.org/10.1007/978-3-030-99524-9_16},
doi = {10.1007/978-3-030-99524-9_16},
year = {2022},
date = {2022-04-01},
booktitle = {28th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS 2022),
held as part of ETAPS 2022: European Joint Conferences
on Theory and Practice of Software},
volume = {13243},
pages = {303--321},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Grätz, Lukas; Hähnle, Reiner; Bubel, Richard Finding Semantic Bugs Fast Proceedings Article In: Johnsen, Einar Broch; Wimmer, Manuel (Ed.): Fundamental Approaches to Software Engineering - 25th International
Conference, FASE 2022, Held as Part of the European Joint Conferences
on Theory and Practice of Software, ETAPS 2022, Munich, Germany,
April 2-7, 2022, Proceedings, pp. 145–154, Springer, 2022. @inproceedings{DBLP:conf/fase/GratzHB22,
title = {Finding Semantic Bugs Fast},
author = {Lukas Gr\"{a}tz and Reiner H\"{a}hnle and Richard Bubel},
editor = {Einar Broch Johnsen and Manuel Wimmer},
url = {https://doi.org/10.1007/978-3-030-99429-7_8},
doi = {10.1007/978-3-030-99429-7_8},
year = {2022},
date = {2022-01-01},
booktitle = {Fundamental Approaches to Software Engineering - 25th International
Conference, FASE 2022, Held as Part of the European Joint Conferences
on Theory and Practice of Software, ETAPS 2022, Munich, Germany,
April 2-7, 2022, Proceedings},
volume = {13241},
pages = {145--154},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Tabar, Asmae Heydari; Bubel, Richard; Hähnle, Reiner Automatic Loop Invariant Generation for Data Dependence Analysis Proceedings Article In: 10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE@ICSE 2022, Pittsburgh, PA, USA, May 22-23,
2022, pp. 34–45, ACM, 2022. @inproceedings{DBLP:conf/icse-formalise/TabarBH22,
title = {Automatic Loop Invariant Generation for Data Dependence Analysis},
author = {Asmae Heydari Tabar and Richard Bubel and Reiner H\"{a}hnle},
url = {https://doi.org/10.1145/3524482.3527649},
doi = {10.1145/3524482.3527649},
year = {2022},
date = {2022-01-01},
urldate = {2022-01-01},
booktitle = {10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE@ICSE 2022, Pittsburgh, PA, USA, May 22-23,
2022},
pages = {34--45},
publisher = {ACM},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Ulbrich, Mattias Towards a Usable and Sustainable Deductive Verification Tool Proceedings Article In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation.
Software Engineering - 11th International Symposium, ISoLA 2022, Rhodes,
Greece, October 22-30, 2022, Proceedings, Part II, pp. 281–300, Springer, 2022. @inproceedings{DBLP:conf/isola/BeckertBHU22,
title = {Towards a Usable and Sustainable Deductive Verification Tool},
author = {Bernhard Beckert and Richard Bubel and Reiner H\"{a}hnle and Mattias Ulbrich},
editor = {Tiziana Margaria and Bernhard Steffen},
url = {https://doi.org/10.1007/978-3-031-19756-7_16},
doi = {10.1007/978-3-031-19756-7_16},
year = {2022},
date = {2022-01-01},
urldate = {2022-01-01},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation.
Software Engineering - 11th International Symposium, ISoLA 2022, Rhodes,
Greece, October 22-30, 2022, Proceedings, Part II},
volume = {13702},
pages = {281--300},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Hähnle, Reiner Dijkstra's Legacy on Program Verification Book Section In: Apt, Krzysztof R.; Hoare, Tony (Ed.): Edsger Wybe Dijkstra: His Life, Work, and Legacy, pp. 105–140, ACM / Morgan & Claypool, 2022. @incollection{DBLP:books/mc/22/Hahnle22,
title = {Dijkstra's Legacy on Program Verification},
author = {Reiner H\"{a}hnle},
editor = {Krzysztof R. Apt and Tony Hoare},
url = {https://doi.org/10.1145/3544585.3544593},
doi = {10.1145/3544585.3544593},
year = {2022},
date = {2022-01-01},
urldate = {2022-01-01},
booktitle = {Edsger Wybe Dijkstra: His Life, Work, and Legacy},
pages = {105--140},
publisher = {ACM / Morgan \& Claypool},
keywords = {},
pubstate = {published},
tppubtype = {incollection}
}
|
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 Proceedings Article 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 Proceedings Article 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}
}
|
Scaletta, Marco; Hähnle, Reiner; Steinhöfel, Dominic; Bubel, Richard Delta-based verification of software product families Proceedings Article In: Tilevich, Eli; Roover, Coen De (Ed.): GPCE '21: Concepts and Experiences, Chicago, IL, USA, October 17
- 18, 2021, pp. 69–82, ACM, 2021. @inproceedings{DBLP:conf/gpce/ScalettaHSB21,
title = {Delta-based verification of software product families},
author = {Marco Scaletta and Reiner H\"{a}hnle and Dominic Steinh\"{o}fel and Richard Bubel},
editor = {Eli Tilevich and Coen De Roover},
url = {https://doi.org/10.1145/3486609.3487200},
doi = {10.1145/3486609.3487200},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {GPCE '21: Concepts and Experiences, Chicago, IL, USA, October 17
- 18, 2021},
pages = {69--82},
publisher = {ACM},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
Albert, Elvira; Hähnle, Reiner; Merayo, Alicia; Steinhöfel, Dominic Certified Abstract Cost Analysis Proceedings Article In: Guerra, Esther; Stoelinga, Mariëlle (Ed.): Fundamental Approaches to Software Engineering - 24th International
Conference, FASE 2021, Held as Part of the European Joint Conferences
on Theory and Practice of Software, ETAPS 2021, Luxembourg City,
Luxembourg, March 27 - April 1, 2021, Proceedings, pp. 24–45, Springer, 2021. @inproceedings{DBLP:conf/fase/AlbertHMS21,
title = {Certified Abstract Cost Analysis},
author = {Elvira Albert and Reiner H\"{a}hnle and Alicia Merayo and Dominic Steinh\"{o}fel},
editor = {Esther Guerra and Mari\"{e}lle Stoelinga},
url = {https://doi.org/10.1007/978-3-030-71500-7_2},
doi = {10.1007/978-3-030-71500-7_2},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {Fundamental Approaches to Software Engineering - 24th International
Conference, FASE 2021, Held as Part of the European Joint Conferences
on Theory and Practice of Software, ETAPS 2021, Luxembourg City,
Luxembourg, March 27 - April 1, 2021, Proceedings},
volume = {12649},
pages = {24--45},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
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 Proceedings Article 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 Proceedings Article 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 Proceedings Article 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 Proceedings Article 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 Proceedings Article 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 Proceedings Article 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 Proceedings Article 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 Proceedings Article 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 Proceedings Article 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}
}
|