2019
|
Steinhöfel, Dominic; Hähnle, Reiner Abstract Execution Inproceedings ter Beek, Maurice H; McIver, Anabelle; Oliveira, José N (Ed.): Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, pp. 319–336, Springer, Cham, 2019, ISBN: 978-3-030-30941-1. Abstract | BibTeX | Links: @inproceedings{steinhoefel.haehnle-19,
title = {Abstract Execution},
author = {Dominic Steinh\"{o}fel and Reiner H\"{a}hnle},
editor = {Maurice H ter Beek and Anabelle McIver and Jos\'{e} N Oliveira},
url = {https://www.key-project.org/wp-content/uploads/2019/12/AbstractExecution.pdf, Self-Archived Version},
doi = {10.1007/978-3-030-30942-8_20},
isbn = {978-3-030-30941-1},
year = {2019},
date = {2019-09-23},
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},
address = {Cham},
series = {Lecture Notes in Computer Science},
crossref = {DBLP:conf/fm/2019},
abstract = {We propose a new static software analysis principle called Abstract Execution, generalizing Symbolic Execution: While the latter analyzes all possible execution paths of a specific program, Abstract Execution analyzes a partially unspecified program by permitting abstract symbols representing unknown contexts. For each abstract symbol, we faithfully represent each possible concrete execution resulting from its substitution with concrete code. There is a wide range of applications of Abstract Execution, especially for verifying relational properties of schematic programs. We implemented Abstract Execution in a deductive verification framework and proved correctness of eight well-known statement-level refactoring rules, including two with loops. For each refactoring we characterize the preconditions that make it semantics- preserving. Most preconditions are not mentioned in the literature.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We propose a new static software analysis principle called Abstract Execution, generalizing Symbolic Execution: While the latter analyzes all possible execution paths of a specific program, Abstract Execution analyzes a partially unspecified program by permitting abstract symbols representing unknown contexts. For each abstract symbol, we faithfully represent each possible concrete execution resulting from its substitution with concrete code. There is a wide range of applications of Abstract Execution, especially for verifying relational properties of schematic programs. We implemented Abstract Execution in a deductive verification framework and proved correctness of eight well-known statement-level refactoring rules, including two with loops. For each refactoring we characterize the preconditions that make it semantics- preserving. Most preconditions are not mentioned in the literature. |
Hentschel, Martin; Bubel, Richard; Hähnle, Reiner The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more Journal Article International Journal on Software Tools for Technology Transfer, 2019, ISSN: 1433-2787. Abstract | BibTeX | Links: @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 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. BibTeX | Links: @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 The Trace Modality Inproceedings Forthcoming Baltag, Alexandru; Barbosa, Luis S (Ed.): 2nd Workshop on Dynamic Logic: New Trends and Applications, Springer, Porto, Portugal, Forthcoming, (Accepted, in print.). BibTeX @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 = {forthcoming},
tppubtype = {inproceedings}
}
|
Bubel, Richard; Hähnle, Reiner; Tabar, Asmae Heydari A Program Logic For Dependence Analysis Inproceedings Forthcoming Ahrendt, Wolfgang; Tarifa, Silvia Lizeth Tapia (Ed.): Integrated Formal Methods, 15th International Conference,
iFM, Bergen, Norway, Springer, Forthcoming. BibTeX @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 = {forthcoming},
tppubtype = {inproceedings}
}
|
Grebing, Sarah Caecilia User Interaction in Deductive Interactive Program Verification PhD Thesis Karlsruhe Institute of Technology, 2019. BibTeX | Links: @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 Forthcoming 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019), Springer Publishing, New York City, USA, Forthcoming, (To appear). BibTeX @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 = {forthcoming},
tppubtype = {inproceedings}
}
|
2018
|
Beckert, Bernhard; Herda, Mihai; Kobischke, Stefan; Ulbrich, Mattias Towards a Notion of Coverage for Incomplete Program-Correctness Proofs Inproceedings Margaria, Tiziana; Steffen, Bernhard (Ed.): 8th International Symposium on Leveraging Applications of Formal Methods,
Verification and Validation (ISoLA 2018), pp. 53–63, Springer, 2018. BibTeX | Links: @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 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. Abstract | BibTeX | Links: @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://www.key-project.org/wp-content/uploads/2019/12/ModularCorrectCompilationWithAutomaticSoundnessProofs.pdf, Self-Archived Version},
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, 2018. BibTeX @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 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. BibTeX | Links: @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. BibTeX | Links: @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 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). BibTeX @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, (2017,12), 2017, ISSN: 2190-4782. BibTeX | Links: @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 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. Abstract | BibTeX | Links: @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 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), 2017, (To appear ). BibTeX | Links: @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 Journal of Automated Reasoning, 2017, ISSN: 1573-0670, (Open Access). Abstract | BibTeX | Links: @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},
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.},
note = {Open Access},
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 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. BibTeX | Links: @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 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. BibTeX | Links: @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://www.key-project.org/wp-content/uploads/2019/12/LoopScopeInvariantRule.pdf, Self-Archived Version},
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}
}
|
Beckert, Bernhard; Grebing, Sarah; Ulbrich, Mattias An Interaction Concept for Program Verification
Systems with Explicit Proof Object Inproceedings Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017), pp. 163–178, Springer International Publishing, Cham, 2017, ISBN: 978-3-319-70389-3. BibTeX | Links: @inproceedings{BeckertGrebingUlbrich2017,
title = {An Interaction Concept for Program Verification
Systems with Explicit Proof Object},
author = {Bernhard Beckert and Sarah Grebing and Mattias Ulbrich},
doi = {10.1007/978-3-319-70389-3_11},
isbn = {978-3-319-70389-3},
year = {2017},
date = {2017-01-01},
booktitle = {Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017)},
volume = {10629},
pages = {163--178},
publisher = {Springer International Publishing},
address = {Cham},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
|
2016
|
Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Schmitt, Peter H; Ulbrich, Mattias (Ed.) Deductive Software Verification - The KeY Book - From Theory to Practice Book Springer, 2016, ISBN: 978-3-319-49811-9. BibTeX | Links: @book{KeYBook2016,
title = {Deductive Software Verification - The KeY Book - From Theory to Practice},
editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H\"{a}hnle and Peter H. Schmitt and Mattias Ulbrich},
url = {http://dx.doi.org/10.1007/978-3-319-49812-6},
doi = {10.1007/978-3-319-49812-6},
isbn = {978-3-319-49811-9},
year = {2016},
date = {2016-12-16},
volume = {10001},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {book}
}
|
Hentschel, Martin; Hähnle, Reiner; Bubel, Richard An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier Inproceedings Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 403-413, ACM, Singapore, Singapore, 2016, ISBN: 978-1-4503-3845-5. Abstract | BibTeX @inproceedings{HentschelHB16ASE16a,
title = {An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier},
author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel},
isbn = {978-1-4503-3845-5},
year = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering},
pages = {403-413},
publisher = {ACM},
address = {Singapore, Singapore},
series = {ASE 2016},
abstract = {Theorem provers have highly complex interfaces, but there are not many systematic studies of their usability and effectiveness. Specifically, for interactive theorem provers the ability to quickly comprehend intermediate proof situations is of pivotal importance. In this paper we present the (as far as we know) first empirical study that systematically compares the effectiveness of different user interfaces of an interactive theorem prover. We juxtapose two different user interfaces of the interactive verifier KeY: the traditional one which focuses on proof objects and a more recent one that provides a view akin to an interactive debugger. We carefully designed a controlled experiment where users were given various proof understanding tasks that had to be solved with alternating interfaces. We provide statistical evidence that the conjectured higher effectivity of the debugger-like interface is not just a hunch.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Theorem provers have highly complex interfaces, but there are not many systematic studies of their usability and effectiveness. Specifically, for interactive theorem provers the ability to quickly comprehend intermediate proof situations is of pivotal importance. In this paper we present the (as far as we know) first empirical study that systematically compares the effectiveness of different user interfaces of an interactive theorem prover. We juxtapose two different user interfaces of the interactive verifier KeY: the traditional one which focuses on proof objects and a more recent one that provides a view akin to an interactive debugger. We carefully designed a controlled experiment where users were given various proof understanding tasks that had to be solved with alternating interfaces. We provide statistical evidence that the conjectured higher effectivity of the debugger-like interface is not just a hunch. |
Hentschel, Martin; Hähnle, Reiner; Bubel, Richard The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts Inproceedings Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 846–851, ACM, Singapore, Singapore, 2016, ISBN: 978-1-4503-3845-5. Abstract | BibTeX @inproceedings{ HentschelHB16ASE16b,
title = {The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts},
author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel},
isbn = {978-1-4503-3845-5},
year = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering},
pages = {846--851},
publisher = {ACM},
address = {Singapore, Singapore},
series = {ASE 2016},
abstract = {The Symbolic Execution Debugger (SED) is an extension of the Eclipse debug platform for interactive symbolic execution. Like a traditional debugger, the SED can be used to locate the origin of a defect and to increase program understanding. However, as it is based on symbolic execution, all execution paths are explored simultaneously. We demonstrate an extension of the SED called Interactive Verification Debugger (IVD) for inspection and understanding of formal verification attempts. By a number of novel views, the IVD allows to quickly comprehend interactive proof situations and to debug the reasons for a proof attempt that got stuck. It is possible to perform interactive proofs completely from within the IVD. It can be experimentally demonstrated that the IVD is more effective in understanding proof attempts than a conventional prover user interface. A screencast explaining proof attempt inspection with the IVD is available at youtu.be/8e-q9Jf1h_w.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The Symbolic Execution Debugger (SED) is an extension of the Eclipse debug platform for interactive symbolic execution. Like a traditional debugger, the SED can be used to locate the origin of a defect and to increase program understanding. However, as it is based on symbolic execution, all execution paths are explored simultaneously. We demonstrate an extension of the SED called Interactive Verification Debugger (IVD) for inspection and understanding of formal verification attempts. By a number of novel views, the IVD allows to quickly comprehend interactive proof situations and to debug the reasons for a proof attempt that got stuck. It is possible to perform interactive proofs completely from within the IVD. It can be experimentally demonstrated that the IVD is more effective in understanding proof attempts than a conventional prover user interface. A screencast explaining proof attempt inspection with the IVD is available at youtu.be/8e-q9Jf1h_w. |
Hentschel, Martin Integrating Symbolic Execution, Debugging and Verification PhD Thesis Technische Universität Darmstadt, 2016. Abstract | BibTeX @phdthesis{ TUD-CS-2016-0099,
title = {Integrating Symbolic Execution, Debugging and Verification},
author = {Martin Hentschel},
year = {2016},
date = {2016-01-01},
school = {Technische Universit\"{a}t Darmstadt},
abstract = {In modern software development, almost all activities are centered around an integrated development environment (IDE). Besides the main use cases to write, execute and debug source code, an IDE serves also as front-end for other tools involved in the development process such as a version control system or an application lifecycle management. Independent from the applied development process, the techniques to ensure correct software are always the same. The general goal is to find defects as soon as possible, because the sooner a defect is found, the easier and cheaper it is to fix. In the first place, the programming language helps to prevent some kinds of defects. Once something is written, it is effective to review it not only to find defects, but also to increase its quality. Also tools which statically analyze the source code help to find defects automatically. In addition, testing is used to ensure that selected usage scenarios behave as expected. However, a test can only show the presence of a failure and not its absence. To ensure that a program is correct, it needs to be proven that the program complies to a formal specification describing the desired behavior. This is done by formal verification tools. Finally, whenever a failure is observed, debugging takes place to locate the defect. This thesis extends the software development tool suite by an interactive debugger based on symbolic execution, a technique to explore all feasible execution paths up to a given depth simultaneously. Such a tool can not only be used for classical debugging activities, but also during code reviews or in order to present results of an analysis based on symbolic execution. The contribution is an extension of symbolic execution to explore the full program behavior even in presence of loops and recursive method calls. This is achieved by integrating specifications in form of loop invariants and methods contracts into a symbolic execution engine. How such a symbolic execution engine based on verification proofs can be realized is presented as well. In addition, the presented Symbolic Execution Debugger (SED) makes the Eclipse platform ready for debuggers based on symbolic execution. Its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all program execution paths are explored simultaneously. To support program comprehension, program execution paths as well as intermediate states are visualized. By default, the SED comes with a symbolic execution engine implemented on top of the KeY verification system. Statistical evidence that the SED increases effectiveness of code reviews is gained from a controlled experiment. Another novelty of the SED is that arbitrary verification proofs can be inspected. Whereas traditional user interfaces of verification tools present proof states in a mathematical fashion, the SED analyzes the full proof and presents different aspects of it using specialized views. A controlled experiment gives statistical evidence that proof understanding tasks are more effective using the SED by comparing its user interface with the original one of KeY. The SED allows one to interact with the underlying prover by adapting code and specifications in an auto-active flavor, which creates the need to manage proofs directly within an IDE. A presented concept achieves this, by integrating a semi-automatic verification tool into an IDE. It includes several optimizations to reduce the overall proof time and can be realized without changing the verification tool. An optimal user experience is achieved only if all aspects of verification are directly supported within the IDE. Thus a thorough integration of KeY into Eclipse is presented, which for instance includes in addition to the proof management capabilities to edit JML specifications and to setup the needed infrastructure for verification with KeY. Altogether, a platform for tools based on symbolic execution and related to verification is presented, which offers a seamless integration into an IDE and furthers a usage in combination. Furthermore, many aspects, like the way the SED presents proof attempts to users, help to reduce the barrier of using formal methods.},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}
In modern software development, almost all activities are centered around an integrated development environment (IDE). Besides the main use cases to write, execute and debug source code, an IDE serves also as front-end for other tools involved in the development process such as a version control system or an application lifecycle management. Independent from the applied development process, the techniques to ensure correct software are always the same. The general goal is to find defects as soon as possible, because the sooner a defect is found, the easier and cheaper it is to fix. In the first place, the programming language helps to prevent some kinds of defects. Once something is written, it is effective to review it not only to find defects, but also to increase its quality. Also tools which statically analyze the source code help to find defects automatically. In addition, testing is used to ensure that selected usage scenarios behave as expected. However, a test can only show the presence of a failure and not its absence. To ensure that a program is correct, it needs to be proven that the program complies to a formal specification describing the desired behavior. This is done by formal verification tools. Finally, whenever a failure is observed, debugging takes place to locate the defect. This thesis extends the software development tool suite by an interactive debugger based on symbolic execution, a technique to explore all feasible execution paths up to a given depth simultaneously. Such a tool can not only be used for classical debugging activities, but also during code reviews or in order to present results of an analysis based on symbolic execution. The contribution is an extension of symbolic execution to explore the full program behavior even in presence of loops and recursive method calls. This is achieved by integrating specifications in form of loop invariants and methods contracts into a symbolic execution engine. How such a symbolic execution engine based on verification proofs can be realized is presented as well. In addition, the presented Symbolic Execution Debugger (SED) makes the Eclipse platform ready for debuggers based on symbolic execution. Its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all program execution paths are explored simultaneously. To support program comprehension, program execution paths as well as intermediate states are visualized. By default, the SED comes with a symbolic execution engine implemented on top of the KeY verification system. Statistical evidence that the SED increases effectiveness of code reviews is gained from a controlled experiment. Another novelty of the SED is that arbitrary verification proofs can be inspected. Whereas traditional user interfaces of verification tools present proof states in a mathematical fashion, the SED analyzes the full proof and presents different aspects of it using specialized views. A controlled experiment gives statistical evidence that proof understanding tasks are more effective using the SED by comparing its user interface with the original one of KeY. The SED allows one to interact with the underlying prover by adapting code and specifications in an auto-active flavor, which creates the need to manage proofs directly within an IDE. A presented concept achieves this, by integrating a semi-automatic verification tool into an IDE. It includes several optimizations to reduce the overall proof time and can be realized without changing the verification tool. An optimal user experience is achieved only if all aspects of verification are directly supported within the IDE. Thus a thorough integration of KeY into Eclipse is presented, which for instance includes in addition to the proof management capabilities to edit JML specifications and to setup the needed infrastructure for verification with KeY. Altogether, a platform for tools based on symbolic execution and related to verification is presented, which offers a seamless integration into an IDE and furthers a usage in combination. Furthermore, many aspects, like the way the SED presents proof attempts to users, help to reduce the barrier of using formal methods. |
Thüm, Thomas; Winkelmann, Tim; Schröter, Reimar; Hentschel, Martin; Krüger, Stefan Variability Hiding in Contracts for Dependent Software Product Lines Inproceedings Proceedings of the Tenth International Workshop on Variability Modelling of Software-intensive Systems, pp. 97–104, ACM, Salvador, Brazil, 2016, ISBN: 978-1-4503-4019-9. Abstract | BibTeX @inproceedings{ThumWSHK16,
title = {Variability Hiding in Contracts for Dependent Software Product Lines},
author = {Thomas Th\"{u}m and Tim Winkelmann and Reimar Schr\"{o}ter and Martin Hentschel and Stefan Kr\"{u}ger},
isbn = {978-1-4503-4019-9},
year = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the Tenth International Workshop on Variability Modelling of Software-intensive Systems},
pages = {97--104},
publisher = {ACM},
address = {Salvador, Brazil},
series = {VaMoS '16},
abstract = {Software product lines are used to efficiently develop and verify similar software products. While they focus on reuse of artifacts between products, a product line may also be reused itself in other product lines. A challenge with such dependent product lines is evolution; every change in a product line may influence all dependent product lines. With variability hiding, we aim to hide certain features and their artifacts in dependent product lines. In prior work, we focused on feature models and implementation artifacts. We build on this by discussing how variability hiding can be extended to specifications in terms of method contracts. We illustrate variability hiding in contracts by means of a running example and share our insights with preliminary experiments on the benefits for formal verification. In particular, we find that not every change in a certain product line requires a re-verification of other dependent product lines.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Software product lines are used to efficiently develop and verify similar software products. While they focus on reuse of artifacts between products, a product line may also be reused itself in other product lines. A challenge with such dependent product lines is evolution; every change in a product line may influence all dependent product lines. With variability hiding, we aim to hide certain features and their artifacts in dependent product lines. In prior work, we focused on feature models and implementation artifacts. We build on this by discussing how variability hiding can be extended to specifications in terms of method contracts. We illustrate variability hiding in contracts by means of a running example and share our insights with preliminary experiments on the benefits for formal verification. In particular, we find that not every change in a certain product line requires a re-verification of other dependent product lines. |