Zobrazeno 1 - 10
of 10
pro vyhledávání: '"Thorsten Bormer"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 102, Iss Proc. SSV 2012, Pp 18-32 (2012)
Software verification tools have become a lot more powerful in recent years. Even verification of large, complex systems is feasible, as demonstrated in the L4.verified and Verisoft XT projects. Still, functional verification of large software system
Externí odkaz:
https://doaj.org/article/2b653621c927404dbff3ab2a4387cd10
Autor:
Stephan Gocht, Mihai Herda, Thorsten Bormer, Daniel Lentzsch, Mattias Ulbrich, Bernhard Beckert
Publikováno v:
Software Engineering and Formal Methods ISBN: 9783030304454
SEFM
SEFM
Program slicing is the process of removing statements from a program such that defined aspects of its behavior are retained. For producing precise slices, i.e., slices that are minimal in size, the program’s semantics must be considered. Existing a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ab7cd0e4ce99222c32a9500fceed92d7
https://doi.org/10.1007/978-3-030-30446-1_19
https://doi.org/10.1007/978-3-030-30446-1_19
Autor:
Stephan Gocht, Bernhard Beckert, Thorsten Bormer, Daniel Lentzsch, Mattias Ulbrich, Mihai Herda
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319668444
IFM
IFM
We present SemSlice, a tool which automatically produces very precise slices for C routines. Slicing is the process of removing statements from a program such that defined aspects of its behavior are retained. For producing precise slices, i.e., slic
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ff661fab30c931d919a7ed64811e11df
https://doi.org/10.1007/978-3-319-66845-1_20
https://doi.org/10.1007/978-3-319-66845-1_20
Publikováno v:
Journal of Information Security and Applications. 19:115-129
The possibility to use computers for counting ballots allows us to design new voting schemes that are arguably fairer than existing schemes designed for hand-counting. We argue that formal methods can and should be used to ensure that such schemes be
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a3f077985f28be9c393d82b5d9e1202d
https://doi.org/10.1016/j.jisa.2014.04.005
https://doi.org/10.1016/j.jisa.2014.04.005
Publikováno v:
Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques ISBN: 9783319471655
ISoLA (1)
ISoLA (1)
Deductive verification is about proving that a piece of code conforms to a given requirement specification. For legacy code, this task is notoriously hard for three reasons: (1) writing specifications post-hoc is much more difficult than producing co
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e1f58f793849564b31b84fcae975f262
https://doi.org/10.1007/978-3-319-47166-2_53
https://doi.org/10.1007/978-3-319-47166-2_53
Publikováno v:
Tests and Proofs ISBN: 9783642389153
TAP@STAF
TAP@STAF
The correctness of program verification systems is of great importance, and it needs to be checked and demonstrated to users and certification agencies. One of the contributing factors to the correctness of the whole verification system is the correc
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9a6e18c2d63284ca773368dd5fcb7f88
https://doi.org/10.1007/978-3-642-38916-0_4
https://doi.org/10.1007/978-3-642-38916-0_4
Publikováno v:
Formal Verification of Object-Oriented Software ISBN: 9783642317613
FoVeOOS
FoVeOOS
Modular deductive verification of software systems is a complex task: the user has to put a lot of effort in writing module specifications that fit together when verifying the system as a whole. In this paper, we propose a combination of deductive ve
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c0d54cfe794fabb835368780e841fb64
https://doi.org/10.1007/978-3-642-31762-0_7
https://doi.org/10.1007/978-3-642-31762-0_7
Publikováno v:
ISORC Workshops
Often, an integrated mixed-criticality system is built in an environment which provides separation functionality for available on-board resources. In this paper we treat such an environment: the PikeOS separation kernel -- a commercial real-time embe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e310643c8c277c2a5b4bf7dd3e16082f
Publikováno v:
Formal Methods for Components and Objects ISBN: 9783642252709
FMCO
FMCO
It is widely recognized that human input is indispensable in deductive verification of real-world code. Verification engineers have to guide the proof search and provide information reflecting their insight into the workings of the program. Lately we
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d27ca89eb2f0fb0bebca33a35e6c3a7c
https://doi.org/10.1007/978-3-642-25271-6_4
https://doi.org/10.1007/978-3-642-25271-6_4
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642044670
SAFECOMP
SAFECOMP
In recent years, deductive program verification has improved to a degree that makes it feasible for real-world programs. Following this observation, the main goal of the BMBF-supported Verisoft XT project is (a) the creation of methods and tools whic
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::063e4e220f2561f0f3b22a6e7d3c146b
https://doi.org/10.1007/978-3-642-04468-7_16
https://doi.org/10.1007/978-3-642-04468-7_16