Program Verification

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@inproceedings{scheurer.hahnle.ea_general-lattice-model_16,

title = {A General Lattice Model for Merging Symbolic Execution Branches},

author = {Dominic Scheurer and Reiner H\"{a}hnle and Richard Bubel},

editor = {Kazuhiro Ogata and Mark Lawford and Shaoying Liu},

url = {http://link.springer.com/chapter/10.1007/978-3-319-47846-3_5

/wp-content/uploads/2016/12/SHB-General_Lattice_Model-2016.pdf},

doi = {10.1007/978-3-319-47846-3_5},

year  = {2016},

date = {2016-01-01},

booktitle = {Formal Methods and Software Engineering - 18th International Conference 

 on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 

 14-18, 2016, Proceedings},

volume = {10009},

pages = {57--73},

publisher = {Springer International Publishing},

series = {LNCS},

abstract = {Symbolic execution is a software analysis technique that has been used with success in the past years in program testing and verification. A main bottleneck of symbolic execution is the path explosion problem: the number of paths in a symbolic execution tree is exponential in the number of static branches of the executed program. Here we put forward an abstraction-based framework for state merging in symbolic execution. We show that it subsumes existing approaches and prove soundness. The method was implemented in the verification system KeY. Our empirical evaluation shows that reductions in proof size of up to 80 % are possible by state merging when applied to complex verification problems; new proofs become feasible that were out of reach so far.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}