@techreport{GrahlGreiner15,
author = {Grahl, Daniel and Greiner, Simon},
title = {Non-Interference with What-Declassification in
Component-Based Systems},
year = 2015,
month = nov,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2015,10},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000050422},
urn = {urn:nbn:de:swb:90-504229},
issn = {2190-4782},
language = {english},
license = {https://creativecommons.org/licenses/by-nc-nd/3.0/},
abstract = {Component-based design is a method for modular design of
systems. The structure of component-based systems follows
specific rules and single components make assumptions on
the environment that they run in. In this paper, we provide
a noninterference property for component-based systems that
allows for a precise specification of what-declassification
of information and takes assumptions on the environment
into consideration in order to allow a modular, precise and
re-usable information-flow analysis. For precise analysis,
components can be analyzed by separately analysing services
provided by a component, and from our compositionality
theorem non-interference of components follows.}
}
@phdthesis{Grahl15,
author = {Daniel Grahl},
title = {Deductive Verification of Concurrent Programs and its
Application to Secure Information Flow for {Java}},
school = {Karlsruhe Institute of Technology},
year = 2015,
month = {29~} # oct,
url = {https://digbib.bibliothek.kit.edu/volltexte/1000050695},
urn = {urn:nbn:de:swb:90-506951},
doi = {10.5445/IR/1000050695},
license = {https://creativecommons.org/licenses/by-sa/4.0},
abstract = {The goal of this thesis is to develop a rigorous analysis
technique for proving functional and relational correctness
of shared-memory multi-threaded object-oriented software
systems---such as programs written in the Java
language---based on formal program semantics and deductive
verification. This work contains the first approach towards
a semantically precise information flow anlaysis for
concurrent programs.}
}
@article{BrunsMostowskiUlbrich15,
author = {Bruns, Daniel and Mostowski, Wojciech and Ulbrich,
Mattias},
title = {Implementation-level Verification of Algorithms with
{\KeY}},
year = 2015,
month = nov,
volume = 17,
number = 6,
pages = {729--744},
journal = {Software Tools for Technology Transfer},
publisher = {Springer},
language = {english},
issn = {1433-2779},
abstract = {We give an account on the authors' experience and results
from the software verification competition held at the
Formal Methods~2012 conference. Competitions like this are
meant to provide a benchmark for verification systems. It
consisted of three algorithms which the authors have
implemented in Java, specified with the Java Modeling
Language, and verified using the \KeY\ system. Building on
our solutions, we argue that verification systems which
target implementations in real-world programming languages
are required to have powerful capabilities for abstraction.
Regarding the \KeY\ tool, we explain features which, driven
by the competition, have been freshly implemented to
accommodate for these demands.},
doi = {10.1007/s10009-013-0293-y},
url = {https://link.springer.com/article/10.1007/s10009-013-0293-y}
}
@inproceedings{KuestersTruderungBeckertEtAl15,
author = {Ralf K{\"u}sters and Tomasz Truderung and Bernhard Beckert
and Daniel Bruns and Michael Kirsten and Martin Mohr},
title = {A Hybrid Approach for Proving Noninterference of {Java}
Programs},
booktitle = {28th IEEE Computer Security Foundations Symposium (CSF)},
editor = {C{\'e}dric Fournet and Michael Hicks and Luca Vigan{\`o}},
doi = {10.1109/CSF.2015.28},
url = {https://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7243741},
isbn = {978-1-4673-7538-2},
pages = {305--319},
year = 2015,
language = {english},
abstract = {Several tools and approaches for proving noninterference
properties for Java and other languages exist. Some of them
have a high degree of automation or are even fully
automatic, but overapproximate the actual information flow,
and hence, may produce false positives. Other tools, such
as those based on theorem proving, are precise, but may
need interaction, and hence, analysis is time-consuming.
In this paper, we propose a hybrid approach that aims at
obtaining the best of both approaches: We want to use fully
automatic analysis as much as possible and only at places
in a program where, due to overapproximation, the automatic
approaches fail, we resort to more precise, but interactive
analysis, where the latter involves only the verification
of specific functional properties in certain parts of the
program, rather than checking more intricate
noninterference properties for the whole program.
To illustrate the hybrid approach, in a case study we use
the hybrid approach---along with the fully automatic tool
Joana for checking noninterference properties for Java
programs and the theorem prover \KeY for the verification
of Java programs---and the CVJ framework proposed by
K\"usters, Truderung, and Graf to establish cryptographic
privacy properties for a non-trivial Java program, namely
an e-voting system. The CVJ framework allows one to
establish cryptographic indistinguishability properties for
Java programs by checking (standard) noninterference
properties for such programs.}
}
@inproceedings{BrunsDoGreinerEtAl15,
author = {Daniel Bruns and Huy Quoc Do and Simon Greiner and Mihai
Herda and Martin Mohr and Enrico Scapin and Tomasz
Truderung and Bernhard Beckert and Ralf K{\"u}sters and
Heiko Mantel and Richard Gay},
title = {Poster: {Security} in E-Voting},
booktitle = {36th IEEE Symposium on Security and Privacy, Poster
Session},
editor = {Sophie Engle},
language = {english},
year = 2015,
month = {18~} # may
}
@techreport{Bruns15,
author = {Bruns, Daniel},
title = {Deductive Verification of Concurrent Programs},
year = 2015,
month = feb,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2015,3},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000045641},
urn = {urn:nbn:de:swb:90-456415},
issn = {2190-4782},
language = {english},
license = {https://creativecommons.org/licenses/by-nc-nd/3.0/},
abstract = {Verification of concurrent programs still poses one of the
major challenges in computer science. Several techniques to
tackle this problem have been proposed. However, they often
do not scale. We present an adaptation of the rely\slash
guarantee methodology in dynamic logic. Rely\slash
guarantee uses functional specification to symbolically
describe the behavior of concurrently running threads:
while each thread \emph{guarantees} adherence to a
specified property at any point in time, all other threads
can \emph{rely} on this property being established. This
allows to regard threads largely in isolation---only
w.r.t.\ an environment constrained by these specifications.
While rely\slash guarantee based approaches often suffer
from a considerable specification overhead, we complement
functional thread specifications with frame conditions.
We will explain our approach using a simple, but concurrent
programing language. Besides the usual constructs for
sequential programs, it caters for dynamic thread creation.
We define semantics of concurrent programs w.r.t.\ an
underspecified deterministic scheduling function.
To formally reason about programs of this language, we
introduce a novel multi-modal logic, \emph{Concurrent
Dynamic Trace Logic} (CDTL). It combines the strengthes of
dynamic logic with those of linear temporal logic and
allows to express temporal properties about symbolic
program traces. We first develop a sound and complete
sequent calculus for the logic subset that uses the
sequential part of the language, based on symbolic
execution. In a second step, we extend this to a calculus
for the complete logic by adding symbolic execution rules
for concurrent interleavings and dynamic thread creation
based on the rely\slash guarantee methodology. Again, this
calculus is proven sound and complete. }
}
@inproceedings{Bruns15a,
author = {Daniel Bruns},
title = {A Theorem Proving Approach to Secure Information Flow in
Concurrent Programs (extended abstract)},
booktitle = {Workshop on Foundations of Computer Security (FCS~2015)},
editor = {Deepak Garg and Boris K{\"o}pf},
language = {english},
year = 2015,
month = jul,
url = {https://software.imdea.org/~bkoepf/FCS15/paper3.pdf}
}
@inproceedings{BeckertBrunsKlebanovEtAl14,
author = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov
and Christoph Scheben and Peter H. Schmitt and Mattias
Ulbrich},
title = {Information Flow in Object-Oriented Software},
booktitle = {Logic-Based Program Synthesis and Transformation, LOPSTR
2013},
editor = {Gopal Gupta and Ricardo Pe{\~n}a},
language = {english},
year = 2014,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
number = 8901,
pages = {19--37},
doi = {10.1007/978-3-319-14125-1_2},
isbn = {978-3-319-14125-1},
abstract = {This paper contributes to the investigation of
object-sensitive information-flow properties for sequential
Java, i.e., properties that take into account information
leakage through objects, as opposed to primitive values. We
present two improvements to a popular object-sensitive
non-interference property. Both reduce the burden on
analysis and monitoring tools. The second contribution is a
formalization of this property in a program logic -- JavaDL
in our case -- which allows using an existing tool without
requiring program modification. The third contribution is a
novel fine-grained specification methodology. In our
approach, arbitrary JavaDL terms (read side-effect-free
Java expressions) may be assigned a security level -- in
contrast to security labels being attached to fields and
variables only. }
}
@techreport{Bruns14,
author = {Bruns, Daniel},
title = {Formal Verification of an Electronic Voting System},
year = 2014,
month = aug,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
language = {english},
number = {2014,11},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000042284},
urn = {urn:nbn:de:swb:90-422842},
issn = {2190-4782},
license = {https://creativecommons.org/licenses/by-nc-nd/3.0/},
abstract = {Electronic voting (e-voting) systems that are used in
public elections need to fulfil a broad range of strong
requirements concerning both safety and security. Among
these requirements are reliability, robustness, privacy of
votes, coercion resistance and universal verifiability.
Bugs in or manipulations of an e-voting system may have
considerable influence on the life of the humans living in
a country where such a system is used. Hence, e-voting
systems are an obvious target for software verification.
In this paper, we report on an implementation of such a
system in Java and the formal verification of functional
properties thereof in the \KeY\ verification system. Even
though the actual components are clearly modularized, the
challenge lies in the fact that we need to prove a highly
nonlocal property: After all voters have cast their votes,
the server calculates the correct votes for each candidate
w.r.t.\ the original ballots. This kind of trace property
is difficult to prove with static techniques like
verification and typically yields a large specification
overhead. }
}
@techreport{HuismanAhrendtBrunsEtAl14,
author = {Huisman, Marieke and Ahrendt, Wolfgang and Bruns, Daniel
and Hentschel, Martin},
title = {Formal Specification with {JML}},
year = 2014,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2014,10},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000041881},
urn = {urn:nbn:de:swb:90-418817},
issn = {2190-4782},
language = {english},
license = {https://creativecommons.org/licenses/by-nc-nd/3.0/},
abstract = {This text is a general, self contained, and tool
independent introduction into the \emph{Java{} Modeling
Language}, JML. It is a preview of a chapter planned to
appear in a book about the \KeY\ approach and tool to the
verification of Java{} software. JML is the dominating
starting point of \KeY\ style Java{} verification. However,
this paper does not in any way depend on any tool nor
verification methodology. Other chapters in this book talk
about the usage of JML in \KeY\ style verification. Here,
we only refer to \KeY\ in very few places, without relying
on it. This introduction is written for all readers with an
interest in formal specification of software in general,
and anyone who wants to learn about the JML approach to
specification in particular. The authors appreciate any
comments or questions that help to improve the text. }
}
@inproceedings{AhrendtBeckertBrunsEtAl14,
author = {Ahrendt, Wolfgang and Beckert, Bernhard and Bruns, Daniel
and Bubel, Richard and Gladisch, Christoph and Grebing,
Sarah and H{\"a}hnle, Reiner and Hentschel, Martin and
Herda, Mihai and Klebanov, Vladimir and Mostowski, Wojciech
and Scheben, Christoph and Schmitt, Peter H. and Ulbrich,
Mattias},
title = {The {\KeY} Platform for Verification and Analysis of
{Java} Programs},
year = 2014,
booktitle = {Verified Software: Theories, Tools, and Experiments (VSTTE
2014)},
language = {english},
editor = {Giannakopoulou, Dimitra and Kroening, Daniel},
pages = {1--17},
publisher = {Springer-Verlag},
number = 8471,
series = {Lecture Notes in Computer Science},
isbn = {978-3-642-54107-0},
doi = {10.1007/978-3-319-12154-3_4},
url = {https://link.springer.com/chapter/10.1007/978-3-319-12154-3_4},
abstract = {The \KeY\ system offers a platform of software analysis
tools for sequential Java. Foremost, this includes full
functional verification against contracts written in the
Java Modeling Language. But the approach is general enough
to provide a basis for other methods and purposes: (i)
complementary validation techniques to formal verification
such as testing and debugging, (ii) methods that reduce the
complexity of verification such as modularization and
abstract interpretation, (iii) analyses of non-functional
properties such as information flow security, and (iv)
sound program transformation and code generation. We show
that deductive technology that has been developed for full
functional verification can be used as a basis and
framework for other purposes than pure functional
verification. We use the current release of the \KeY\
system as an example to explain and prove this claim.}
}
@techreport{Bruns14a,
author = {Daniel Bruns},
title = {Towards Specification and Verification of Information Flow
in Concurrent {Java-}like Programs},
year = 2014,
month = mar,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
language = {english},
number = {2014,5},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000039446},
urn = {urn:nbn:de:swb:90-394465},
issn = {2190-4782},
license = {https://creativecommons.org/licenses/by-nc-nd/3.0/},
abstract = {Today, nearly all personal computer systems are
multiprocessor systems, allowing multiple programs to be
executed in parallel while accessing a shared memory. At
the same time, computers are increasingly handling more and
more data. Ensuring that no confidential data is leaked to
untrusted sinks remains a major quest in software
engineering. Formal verification, based on theorem proving,
is a powerful technique to prove both functional
correctness and security properties such as absence of
information flow. Present verification systems are sound
and complete, but often lack efficiency and are only
applicable to sequential programs. Concurrent programs are
notorious for all possible environment actions have to be
taken into account.
In this paper, we point out steps towards a formal
verification methodology for information flow in concurrent
programs. We consider passive attackers who are able to
observe public parts of the memory at any time during
execution and to compare program traces between different
executions. Our approach consists of two main elements: (i)
formalizing properties on whether two executions are
indistinguishable to such an attacker in a decidable logic,
and (ii) defining a technique to reason about executions of
concurrent programs by regarding a single thread in
isolation. The latter is based on the rely/guarantee
approach. }
}
@techreport{BeckertBrunsKlebanovEtAl13,
author = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov
and Christoph Scheben and Peter H. Schmitt and Mattias
Ulbrich },
title = {Information Flow in Object-Oriented Software -- Extended
Version --},
year = 2013,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2013,14},
series = {Karlsruhe Reports in Informatics},
language = {english},
license = {https://creativecommons.org/licenses/by-nc-nd/3.0/},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000037606},
urn = {urn:nbn:de:swb:90-376067},
issn = {2190-4782}
}
@techreport{BeckertBrunsKlebanovEtAl13a,
author = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov
and Christoph Scheben and Peter H. Schmitt and Mattias
Ulbrich},
title = {Secure Information Flow for {Java} -- A Dynamic Logic
Approach},
year = 2013,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2013,10},
language = {english},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000036786},
issn = {2190-4782},
license = {https://creativecommons.org/licenses/by-nc-nd/3.0/},
annote = {sequence theory in Appendix~A}
}
@inproceedings{BeckertBruns13,
author = {Bernhard Beckert and Daniel Bruns},
title = {Dynamic Logic with Trace Semantics},
booktitle = {24th International Conference on Automated Deduction
(CADE-24)},
editor = {Maria Paola Bonacina},
year = 2013,
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 7898,
pages = {315--329},
isbn = {978-3-642-38573-5},
language = {english},
doi = {10.1007/978-3-642-38574-2_22},
url = {https://link.springer.com/chapter/10.1007/978-3-642-38574-2_22},
abstract = {Dynamic logic is an established instrument for program
verification and for reasoning about the semantics of
programs and programming languages. In this paper, we
define an extension of dynamic logic, called Dynamic Trace
Logic~(DTL), which combines the expressiveness of program
logics such as dynamic logic with that of temporal logic.
And we present a sound and relatively complete sequent
calculus for proving validity of DTL formulae. Due to its
expressiveness, DTL can serve as a basis for proving
functional and information-flow properties in concurrent
programs, among other applications.}
}
@inproceedings{KuestersTruderungBeckertEtAl13,
author = {Ralf K{\"u}sters and Tomasz Truderung and Bernhard Beckert
and Daniel Bruns and J{\"u}rgen Graf and Christoph Scheben},
title = {A Hybrid Approach for Proving Noninterference and
Applications to the Cryptographic Verification of {Java}
Programs},
booktitle = {Grande Region Security and Reliability Day 2013},
url = {https://grsrd.uni.lu/papers/grsrd2013_submission_2.pdf},
year = 2013,
editor = {Christian Hammer and Sjouke Mauw},
address = {Luxembourg},
language = {english},
note = {Extended Abstract}
}
@inproceedings{BeckertBrunsGrebing12,
author = {Bernhard Beckert and Daniel Bruns and Sarah Grebing},
title = {Mind the Gap: Formal Verification and the {Common}
{Criteria}},
year = 2012,
booktitle = {6th~International Verification Workshop, VERIFY-2010},
editor = {Markus Aderhold and Serge Autexier and Heiko Mantel},
language = {english},
abstract = {It is a common belief that the rise of standardized
software certification schemes like the Common Criteria
(CC) would give a boost to formal verification, and that
software certification may be a killer application for
program verification. However, while formal models are
indeed used throughout high-assurance certification,
verification of the actual implementation is not required
by the CC and largely neglected in certification practice
-- despite the great advances in program verification over
the last decade. In this paper we discuss the gap between
program verification and CC software certification, and we
point out possible uses of code-level program verification
in the CC certification process.},
series = {EPiC Series},
volume = 3,
pages = {4--12},
publisher = {EasyChair},
issn = {2040-557X},
url = {https://easychair.org/publications/?page=1489979161}
}
@inproceedings{BeckertBruns12,
author = {Beckert, Bernhard and Bruns, Daniel},
title = {Formal Semantics of Model Fields in Annotation-based
Specifications},
year = 2012,
booktitle = {{KI 2012}: Advances in Artificial Intelligence},
editor = {Birte Glimm and Antonio Kr{\"u}ger},
publisher = {Springer-Verlag},
language = {english},
series = {Lecture Notes in Computer Science},
volume = 7526,
isbn = {978-3-642-33346-0},
pages = {13--24},
url = {https://link.springer.com/chapter/10.1007/978-3-642-33347-7_2},
abstract = {It is widely recognized that abstraction and
modularization are indispensable for specification of
real-world programs. In source-code level program
specification and verification, model fields are a common
means for those goals. However, it remains a challenge to
provide a well-founded formal semantics for the general
case in which the abstraction relation defining a model
field is non-functional.
In this paper, we discuss and compare several possibilities
for defining model field semantics, and we give a complete
formal semantics for the general case. Our analysis and the
proposed semantics is based on a generalization of
Hilbert's $\varepsilon$~terms.}
}
@techreport{BeckertBruns12a,
author = {Bernhard Beckert and Daniel Bruns},
title = {Dynamic Trace Logic: Definition and Proofs},
year = 2012,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2012,10},
series = {Karlsruhe Reports in Informatics},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000028184},
urn = {urn:nbn:de:swb:90-281845},
issn = {2190-4782},
license = {https://creativecommons.org/licenses/by-nc-nd/3.0/},
language = {english},
abstract = { Dynamic logic is an established instrument for program
verification and for reasoning about the semantics of
programs and programming languages. In this paper, we
define an extension of dynamic logic, called Dynamic Trace
Logic~(DTL), which combines the expressiveness of program
logics such as dynamic logic with that of temporal logic.
And we present a sound and relatively complete sequent
calculus for proving validity of DTL formulae. Due to its
expressiveness, DTL can serve as a basis for functional
verification of concurrent programs and for proving
information-flow properties among other applications.},
note = {A revised version replacing an unsound rule is available
at
\url{https://formal.kastel.kit.edu/~bruns/papers/trace-tr.pdf}.}
}
@article{Bruns12,
author = {Daniel Bruns},
title = {Eine formale {S}emantik f{\"u}r die {J}ava {M}odeling
{L}anguage},
doi = {10.1007/s00287-011-0532-0},
journal = {Informatik-Spektrum},
publisher = {Springer-Verlag},
year = 2012,
volume = 35,
number = 1,
pages = {45--49},
language = {ngerman},
url = {https://www.springerlink.com/content/b503j663353x482w/}
}
@techreport{BeckertBrunsKuestersEtAl12,
author = {Bernhard Beckert and Daniel Bruns and Ralf K\"{u}sters and
Christoph Scheben and Schmitt, Peter H. and Tomasz
Truderung},
title = {The {\KeY} Approach for the Cryptographic Verification of
{J}ava Programs: {A} Case Study},
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2012,8},
year = 2012,
series = {Karlsruhe Reports in Informatics},
language = {english},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000027497},
urn = {urn:nbn:de:swb:90-274973},
license = {https://creativecommons.org/licenses/by-nc-nd/3.0/},
abstract = { In this paper, we report on an ongoing case study in
which we use the \KeY\ tool, a theorem prover for checking
functional correctness and noninterference properties of
Java programs, to establish computational
indistinguishability for a simple Java program that
involves clients sending encrypted messages over an
untrusted network to a server. The analysis uses a general
framework, recently proposed by K{\"u}sters et al., which
enables program analysis tools, such as \KeY, that can
check (standard) noninterference properties for Java
programs to establish computational indistinguishability
properties. }
}
@inproceedings{Bruns11,
author = {Daniel Bruns},
title = {Specification of Red-black Trees: Showcasing Dynamic
Frames, Model Fields and Sequences},
note = {Extended Abstract},
year = 2011,
booktitle = {10th~{\KeY} Symposium},
editor = {Ahrendt, Wolfgang and Bubel, Richard},
address = {Nijmegen, the Netherlands},
language = {english},
month = {26--27~} # aug,
url = {https://digbib.bibliothek.kit.edu/volltexte/1000024828},
urn = {urn:nbn:de:swb:90-248287},
abstract = {Complex data structures still pose a major challenge in
specification and verification of object-oriented programs.
Leino and Moskal have proposed a suite of benchmarks for
verification tools, nicknamed ``VACID-0''. In contrast to
similar papers, the tasks of VACID-0 do not only include
verification in terms of an observable behavior but also of
internal workings of algorithms and data structures. The
arguably most difficult target are so-called red-black
black trees. In this contribution, we present an
implementation and specification in Java/JML$^\ast$ (i.e.,
\KeY's extension to JML with dynamic frames). It makes use
of several new features: first and foremost the dynamic
frame theory, model fields, the sequence ADT, as well as
some newly supported features from standard JML.}
}
@inproceedings{BeckertBruns11,
author = {Bernhard Beckert and Daniel Bruns},
title = {Formal Semantics of Model Fields Inspired by a
Generalization of {Hilbert's} $\varepsilon$~Terms},
note = {Extended Abstract},
year = 2011,
booktitle = {10th~{\KeY} Symposium},
editor = {Ahrendt, Wolfgang and Bubel, Richard},
address = {Nijmegen, the Netherlands},
language = {english},
month = {26--27~} # aug,
url = {https://digbib.bibliothek.kit.edu/volltexte/1000024829},
urn = {urn:nbn:de:swb:90-248290},
abstract = { It is widely recognized that abstraction and
modularization are indispensable for specification of
real-world programs. In source-code level program
specification languages, such as the Java Modeling
Language~(JML), model fields are a common means for
achieving abstraction and information hiding. However,
there is yet no well-defined formal semantics for the
general case in which the abstraction relation defining a
model field is non-functional and may contain references to
other model fields. In this contribution, we discuss and
compare several possibilities for defining model field
semantics, and we give a complete formal semantics for the
general case. Our analysis and the proposed semantics is
inspired by a generalization of Hilbert's $\varepsilon$
terms.}
}
@inproceedings{BrunsKlebanovSchaefer11,
author = {Daniel Bruns and Vladimir Klebanov and Ina Schaefer},
title = {Verification of Software Product Lines with Delta-Oriented
Slicing},
year = 2011,
editor = {Bernhard Beckert and Claude March{\'e}},
booktitle = {Formal Verification of Object-Oriented Software ({FoVeOOS
2010})},
publisher = {Springer-Verlag},
language = {english},
series = {Lecture Notes in Computer Science},
volume = 6528,
pages = {61--75},
isbn = {978-3-642-18069-9},
url = {https://www.springerlink.com/content/441476732611n21t/},
doi = {10.1007/978-3-642-18070-5_5},
abstract = {Software product lines (SPL) are a well-known methodology
to develop industry-size adaptable software systems. SPL
are often used in domains where high-quality software is
desirable, but the overwhelming product diversity remains a
challenge for assuring correctness. We present our work in
progress on reducing the deductive verification effort
across different products of an SPL. On the specification
side, our approach enriches the delta language for
describing SPLs with formal product specifications. On the
verification side, we combine program slicing and
similarity-guided proof reuse to ease the verification
process.}
}
@inproceedings{BrunsKlebanovSchaefer10,
author = {Daniel Bruns and Vladimir Klebanov and Ina Schaefer},
title = {Verification of Software Product Lines: Reducing the
Effort with Delta-oriented Slicing and Proof Reuse},
year = 2010,
month = {28--30~} # jun,
address = {Paris, France},
booktitle = {Papers Presented at the International Conference on Formal
Verification of Object-Oriented Software ({FoVeOOS})},
editor = {Bernhard Beckert and Claude March{\'e}},
language = {english},
publisher = {Technical Report, Department of Informatics, Karlsruhe
Institute of Technology, 2010-13},
series = {Karlsruhe Reports in Informatics},
number = {2010,13},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000019096},
urn = {urn:nbn:de:swb:90-190964},
pages = {345--358},
abstract = {Software product lines (SPL) are a well-known methodology
to develop industry-size adaptable software systems. SPL
are often used in domains where high-quality software is
desirable, but the overwhelming product diversity remains a
challenge for assuring correctness. We present our work in
progress on reducing the deductive verification effort
across different products of an SPL. On the specification
side, our approach enriches the delta language for
describing SPLs with formal product specifications. On the
verification side, we combine program slicing and
similarity-guided proof reuse to ease the verification
process.}
}
@inproceedings{Bruns10,
author = {Daniel Bruns},
title = {Formal Semantics for the {Java} {Modeling} {Language}},
note = {Best Paper Award},
year = 2010,
month = {19--20~} # mar,
booktitle = {Informatiktage 2010},
address = {Bonn, Germany},
pages = {15--18},
publisher = {Gesellschaft f{\"u}r Informatik},
series = {Lecture Notes in Informatics},
volume = {S-9},
isbn = {978-3-88579-443-1},
url = {https://subs.emis.de/LNI/Seminar/Seminar09/S-09.pdf},
language = {english},
abstract = {A common critique of formal methods in software
development practise is, that they are not readily
understandable and thus not widely used. The Java Modeling
Language (JML) was created in an attempt to bridge that
gap. By building upon the syntax of Java it is meant to be
easily accessible to the common user -- who might not be
skilled in formal modeling. Due to this advantage, JML has
quickly become one of most popular specification languages
to use with both static and runtime analysis of programs.
JML specifications are written in a Java-like expression
language as comments straight into source files. It
provides both in-code assertions as well as method
contracts and class invariants which are indicated by
appropriate preceding keywords. However, the official
reference mostly lacks a clear definition of semantics. In
turn, several tools implementing JML syntax use their own
interpretations. Past approaches to formal semantics have
rather been documentations of those tools than providing a
unified reference.}
}
@mastersthesis{Bruns09,
author = {Daniel Bruns},
title = {Formal Semantics for the {Java} {Modeling} {Language}},
year = 2009,
month = jun,
language = {english},
school = {Universit{\"{a}}t {Karlsruhe}},
type = {Diplomarbeit},
url = {https://digbib.bibliothek.kit.edu/volltexte/1000012399},
urn = {urn:nbn:de:swb:90-123994},
license = {https://creativecommons.org/licenses/by/3.0},
abstract = {This thesis is concerned with the Java Modeling Language
(JML), a wide-spread specification language for Java, which
is used in both static and runtime analysis of programs.
Yet, the official reference mostly lacks semantics, while
several tools which implement JML do not agree on their
interpretation of JML specifications. Past approaches have
all centered around a certain verification tool and are
highly depending on specific higher order logics. In this
work, we develop a formalization with little requirements.
Upon a simple machine model we describe JML artifacts in
basic notations such as first order logic. In that, we
provide a nearly comprehensive overview of features which
cover nearly all specification elements for sequential Java
programs.}
}
@article{Bruns08,
author = {Daniel Bruns},
title = {Elektronische {Wahlen}: {Theoretisch} m{\"o}glich,
praktisch undemokratisch},
language = {ngerman},
year = 2008,
month = sep,
journal = {FIfF-Kommunikation},
volume = 25,
number = 3,
issn = {0938-3476},
pages = {33--35}
}
@mastersthesis{Bruns07,
author = {Daniel Bruns},
title = {A Fixpoint-based Rule for Loop Verification},
year = 2007,
month = jun,
language = {english},
school = {Universit{\"a}t Karlsruhe},
type = {Studienarbeit}
}
This file was generated by bibtex2html 1.98.