B. Engelmann and E. Olderog, "A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs" in Proc. Proc. Theory and Practice of Formal Methods, 2016.
@inproceedings{EngelmannOlderog2015,
author = {Bj\"orn Engelmann and Ernst-R\"udiger Olderog},
title = {{A} {S}ound and {C}omplete {H}oare {L}ogic for {D}ynamically-{T}yped, {O}bject-{O}riented {P}rograms},
booktitle = {Proc. Theory and Practice of Formal Methods},
year = {2016},
editor = {Erika {\' A}brah{\' a}m and Marcello Bonsangue and Einar Broch Johnsen},
volume = {9660},
series = {LNCS},
publisher = {Springer},
pages = {173--193},
url = {http://link.springer.com/chapter/10.1007%2F978-3-319-30734-3_13},
optaddress = {Eindhoven, The Netherlands}
}
B. Engelmann, "Formally Verifying Dynamically-typed Programs like Statically-typed Ones -- Another perspective" in Proc. Proceedings of the Young Researchers Conference Frontiers of Formal Methods, 2015.
@inproceedings{Eng2015,
author = {Bj{\"o}rn Engelmann},
title = {Formally Verifying Dynamically-typed Programs like Statically-typed Ones -- Another perspective},
booktitle = {Proceedings of the Young Researchers Conference Frontiers of Formal Methods},
year = {2015},
url = {http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2015/2015-06.pdf}
}
B. Engelmann, E. -R. Olderog, and N. Flick, Closing the Gap -- Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic.
@misc{EOF2015,
author = {Bj{\"o}rn Engelmann and E.-R Olderog and Nils-Erik Flick},
title = {Closing the Gap -- Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic},
month = {January},
year = {2015},
howpublished = {arXiv:1501.02699v1 [cs.PL]},
abstract = {Dynamically typed object-oriented languages enable programmers to write elegant, reusable and extensible programs. However, with the current methodology for program verification, the absence of static type information creates significant overhead. Our proposal is two-fold: First, we propose a layer of abstraction hiding the complexity of dynamic typing when provided with sufficient type information. Since this essentially creates the illusion of verifying a statically-typed program, the effort required is equivalent to the statically-typed case. Second, we show how the required type information can be efficiently derived for all type-safe programs by integrating a type inference algorithm into Hoare logic, yielding a semi-automatic procedure allowing the user to focus on those typing problems really requiring his attention. While applying type inference to dynamically typed programs is a well-established method by now, our approach complements conventional soft typing systems by offering formal proof as a third option besides modifying the program (static typing) and accepting the presence of runtime type errors (dynamic typing).},
url = {http://arxiv.org/abs/1501.02699}
}
N. Flick and B. Engelmann, "Properties of Petri Nets with Context-free Structure Changes" in Proc. Fifth International Workshop on Graph Computation Models, 2014.
@inproceedings{FE2014,
author = {Nils-Erik Flick and Bj{\"o}rn Engelmann},
title = {Properties of Petri Nets with Context-free Structure Changes},
booktitle = {Fifth International Workshop on Graph Computation Models},
year = {2014},
abstract = {Petri nets model systems with distributed state and syn- chronised state changes. Extending them with rewriting rules allows for evolving structure. In this paper, we investigate dynamic properties of simple structure-changing Petri nets. We show undecidability of checking a language-based notion of correctness even for very restricted classes of structure-changing nets. We also introduce a colour-based abstraction and use it to specify, and in special cases decide, reachability properties.},
url = {http://gcm2014.imag.fr/proceedingsGCM2014.pdf}
}
B. Engelmann, "Towards Practical Verification of Dynamically Typed Programs" in Proc. 25th Nordic Workshop on Programming Theory, 2013.
@inproceedings{Eng2013,
author = {Bj{\"o}rn Engelmann},
title = {Towards Practical Verification of Dynamically Typed Programs},
booktitle = {25th Nordic Workshop on Programming Theory},
year = {2013},
abstract = {Dynamically typed languages enable programmers to write elegant, reusable and extendable programs. Recently, some progress has been made regarding their verification. However, the user is currently required to manually show the absence of type errors, a tedious task usually involving large amounts of repetitive work. As most dynamically typed programs only occasionally divert from what would also be possible in statically typed languages, properly designed type inference algorithms should be able to supply the missing type information in most cases. We propose integrating a certified type inference algorithm into an interactive verification environment in order to a) provide a layer of abstraction, allowing the users to verify their programs like in a statically typed language whenever possible and b) use verification results to improve type inference and thus allow type checking of difficult cases.},
pdf = {http://theoretica.informatik.uni-oldenburg.de/~ben/papers/nwpt2013-paper.pdf},
slides = {http://theoretica.informatik.uni-oldenburg.de/~ben/slides/nwpt2013/},
url = {http://theoretica.informatik.uni-oldenburg.de/~ben/papers/nwpt2013-paper.pdf}
}
M. Johns, B. Engelmann, and J. Posegga, "XSSDS: Server-Side Detection of Cross-Site Scripting Attacks" in Proc. ACSAC, 2008.
doi: 10.1109/ACSAC.2008.36
@inproceedings{JEP08,
author = {Martin Johns and Bj{\"o}rn Engelmann and Joachim Posegga},
title = {XSSDS: Server-Side Detection of Cross-Site Scripting Attacks},
booktitle = {ACSAC},
year = {2008},
pages = {335-344},
abstract = {Cross-site Scripting (XSS) has emerged to one of the most prevalent type of security vulnerabilities. While the reason for the vulnerability primarily lies on the serverside, the actual exploitation is within the victim's web browser on the client-side. Therefore, an operator of a web application has only very limited evidence of XSS issues. In this paper, we propose a passive detection system to identify successful XSS attacks. Based on a prototypical implementation, we examine our approach's accuracy and verify its detection capabilities. We compiled a data-set of 500.000 individual HTTP request/response-pairs from 95 popular web applications for this, in combination with both real word and manually crafted XSS-exploits; our detection approach results in a total of zero false negatives for all tests, while maintaining an excellent false positive rate for more than 80\% of the examined web applications.},
bibtex = {jep08.bib},
doi = {10.1109/ACSAC.2008.36},
pdf = {http://www.acsac.org/openconf2008/modules/request.php?module=oc_proceedings&action=view.php&a=Accept&id=104}
B. Engelmann, "Dynamic Web Application Analysis for Cross Site Scripting Detection" Master's Dissertation , Germany, 2007.
@mastersthesis{ Eng07,
author = {Bj{\"o}rn Engelmann},
title = {Dynamic Web Application Analysis for Cross Site Scripting Detection},
type = {Diploma Thesis},
school = {University of Hamburg},
address = {Germany},
year = {2007},
month = {August},
url = {https://www.uni-oldenburg.de/fileadmin/user_upload/f2inform-csd/thesis-engelmann.pdf},
Go to documentB. Engelmann and E. Olderog, "A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs" in Proc. Proc. Theory and Practice of Formal Methods, 2016.