---
_id: '162'
author:
- first_name: Guangli
full_name: Zhang, Guangli
last_name: Zhang
citation:
ama: 'Zhang G. Program Slicing: A Way of Separating WHILE Programs into Precise
and Approximate Portions. Universität Paderborn; 2016.'
apa: 'Zhang, G. (2016). Program Slicing: A Way of Separating WHILE Programs into
Precise and Approximate Portions. Universität Paderborn.'
bibtex: '@book{Zhang_2016, title={Program Slicing: A Way of Separating WHILE Programs
into Precise and Approximate Portions}, publisher={Universität Paderborn}, author={Zhang,
Guangli}, year={2016} }'
chicago: 'Zhang, Guangli. Program Slicing: A Way of Separating WHILE Programs
into Precise and Approximate Portions. Universität Paderborn, 2016.'
ieee: 'G. Zhang, Program Slicing: A Way of Separating WHILE Programs into Precise
and Approximate Portions. Universität Paderborn, 2016.'
mla: 'Zhang, Guangli. Program Slicing: A Way of Separating WHILE Programs into
Precise and Approximate Portions. Universität Paderborn, 2016.'
short: 'G. Zhang, Program Slicing: A Way of Separating WHILE Programs into Precise
and Approximate Portions, Universität Paderborn, 2016.'
date_created: 2017-10-17T12:41:23Z
date_updated: 2022-01-06T06:52:45Z
department:
- _id: '77'
language:
- iso: eng
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Heike
full_name: Wehrheim, Heike
last_name: Wehrheim
title: 'Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate
Portions'
type: mastersthesis
user_id: '15504'
year: '2016'
...
---
_id: '132'
abstract:
- lang: eng
text: Runtime reconfiguration can be used to replace hardware modules in the field
and even to continuously improve them during operation. Runtime reconfiguration
poses new challenges for validation, since the required properties of newly arriving
modules may be difficult to check fast enough to sustain the intended system dynamics.
In this paper we present a method for just-in-time verification of the worst-case
completion time of a reconfigurable hardware module. We assume so-called run-to-completion
modules that exhibit start and done signals indicating the start and end of execution,
respectively. We present a formal verification approach that exploits the concept
of proof-carrying hardware. The approach tasks the creator of a hardware module
with constructing a proof of the worst-case completion time, which can then easily
be checked by the user of the module, just prior to reconfiguration. After explaining
the verification approach and a corresponding tool flow, we present results from
two case studies, a short term synthesis filter and a multihead weigher. The resultsclearly
show that cost of verifying the completion time of the module is paid by the creator
instead of the user of the module.
author:
- first_name: Tobias
full_name: Wiersema, Tobias
id: '3118'
last_name: Wiersema
- first_name: Marco
full_name: Platzner, Marco
id: '398'
last_name: Platzner
citation:
ama: 'Wiersema T, Platzner M. Verifying Worst-Case Completion Times for Reconfigurable
Hardware Modules using Proof-Carrying Hardware. In: Proceedings of the 11th
International Symposium on Reconfigurable Communication-Centric Systems-on-Chip
(ReCoSoC 2016). ; 2016:1--8. doi:10.1109/ReCoSoC.2016.7533910'
apa: Wiersema, T., & Platzner, M. (2016). Verifying Worst-Case Completion Times
for Reconfigurable Hardware Modules using Proof-Carrying Hardware. In Proceedings
of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip
(ReCoSoC 2016) (pp. 1--8). https://doi.org/10.1109/ReCoSoC.2016.7533910
bibtex: '@inproceedings{Wiersema_Platzner_2016, title={Verifying Worst-Case Completion
Times for Reconfigurable Hardware Modules using Proof-Carrying Hardware}, DOI={10.1109/ReCoSoC.2016.7533910},
booktitle={Proceedings of the 11th International Symposium on Reconfigurable Communication-centric
Systems-on-Chip (ReCoSoC 2016)}, author={Wiersema, Tobias and Platzner, Marco},
year={2016}, pages={1--8} }'
chicago: Wiersema, Tobias, and Marco Platzner. “Verifying Worst-Case Completion
Times for Reconfigurable Hardware Modules Using Proof-Carrying Hardware.” In Proceedings
of the 11th International Symposium on Reconfigurable Communication-Centric Systems-on-Chip
(ReCoSoC 2016), 1--8, 2016. https://doi.org/10.1109/ReCoSoC.2016.7533910.
ieee: T. Wiersema and M. Platzner, “Verifying Worst-Case Completion Times for Reconfigurable
Hardware Modules using Proof-Carrying Hardware,” in Proceedings of the 11th
International Symposium on Reconfigurable Communication-centric Systems-on-Chip
(ReCoSoC 2016), 2016, pp. 1--8.
mla: Wiersema, Tobias, and Marco Platzner. “Verifying Worst-Case Completion Times
for Reconfigurable Hardware Modules Using Proof-Carrying Hardware.” Proceedings
of the 11th International Symposium on Reconfigurable Communication-Centric Systems-on-Chip
(ReCoSoC 2016), 2016, pp. 1--8, doi:10.1109/ReCoSoC.2016.7533910.
short: 'T. Wiersema, M. Platzner, in: Proceedings of the 11th International Symposium
on Reconfigurable Communication-Centric Systems-on-Chip (ReCoSoC 2016), 2016,
pp. 1--8.'
date_created: 2017-10-17T12:41:17Z
date_updated: 2022-01-06T06:51:30Z
ddc:
- '040'
department:
- _id: '78'
doi: 10.1109/ReCoSoC.2016.7533910
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-21T13:02:30Z
date_updated: 2018-03-21T13:02:30Z
file_id: '1562'
file_name: 132-07533910.pdf
file_size: 911171
relation: main_file
success: 1
file_date_updated: 2018-03-21T13:02:30Z
has_accepted_license: '1'
language:
- iso: eng
page: 1--8
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 11th International Symposium on Reconfigurable Communication-centric
Systems-on-Chip (ReCoSoC 2016)
status: public
title: Verifying Worst-Case Completion Times for Reconfigurable Hardware Modules using
Proof-Carrying Hardware
type: conference
user_id: '477'
year: '2016'
...
---
_id: '250'
abstract:
- lang: eng
text: Before execution, users should formally validate the correctness of software
received from untrusted providers. To accelerate this validation, in the proof
carrying code (PCC) paradigm the provider delivers the software together with
a certificate, a formal proof of the software’s correctness. Thus, the user only
checks if the attached certificate shows correctness of the delivered software.Recently,
we introduced configurable program certification, a generic, PCC based framework
supporting various software analyses and safety properties. Evaluation of our
framework revealed that validation suffers from certificate reading. In this paper,
we present two orthogonal approaches which improve certificate validation, both
reducing the impact of certificate reading. The first approach reduces the certificate
size, storing information only if it cannot easily be recomputed. The second approach
partitions the certificate into independently checkable parts. The trick is to
read parts of the certificate while already checking read parts. Our experiments
show that validation highly benefits from our improvements.
author:
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
citation:
ama: 'Jakobs M-C. Speed Up Configurable Certificate Validation by Certificate Reduction
and Partitioning. In: Proceedings of the 13th International Conference on Software
Engineering and Formal Methods (SEFM). LNCS. ; 2015:159--174. doi:10.1007/978-3-319-22969-0_12'
apa: Jakobs, M.-C. (2015). Speed Up Configurable Certificate Validation by Certificate
Reduction and Partitioning. In Proceedings of the 13th International Conference
on Software Engineering and Formal Methods (SEFM) (pp. 159--174). https://doi.org/10.1007/978-3-319-22969-0_12
bibtex: '@inproceedings{Jakobs_2015, series={LNCS}, title={Speed Up Configurable
Certificate Validation by Certificate Reduction and Partitioning}, DOI={10.1007/978-3-319-22969-0_12},
booktitle={Proceedings of the 13th International Conference on Software Engineering
and Formal Methods (SEFM)}, author={Jakobs, Marie-Christine}, year={2015}, pages={159--174},
collection={LNCS} }'
chicago: Jakobs, Marie-Christine. “Speed Up Configurable Certificate Validation
by Certificate Reduction and Partitioning.” In Proceedings of the 13th International
Conference on Software Engineering and Formal Methods (SEFM), 159--174. LNCS,
2015. https://doi.org/10.1007/978-3-319-22969-0_12.
ieee: M.-C. Jakobs, “Speed Up Configurable Certificate Validation by Certificate
Reduction and Partitioning,” in Proceedings of the 13th International Conference
on Software Engineering and Formal Methods (SEFM), 2015, pp. 159--174.
mla: Jakobs, Marie-Christine. “Speed Up Configurable Certificate Validation by Certificate
Reduction and Partitioning.” Proceedings of the 13th International Conference
on Software Engineering and Formal Methods (SEFM), 2015, pp. 159--174, doi:10.1007/978-3-319-22969-0_12.
short: 'M.-C. Jakobs, in: Proceedings of the 13th International Conference on Software
Engineering and Formal Methods (SEFM), 2015, pp. 159--174.'
date_created: 2017-10-17T12:41:40Z
date_updated: 2022-01-06T06:56:43Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-319-22969-0_12
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-21T09:45:15Z
date_updated: 2018-03-21T09:45:15Z
file_id: '1489'
file_name: 250-Jakobs2015.pdf
file_size: 724308
relation: main_file
success: 1
file_date_updated: 2018-03-21T09:45:15Z
has_accepted_license: '1'
language:
- iso: eng
page: 159--174
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 13th International Conference on Software Engineering
and Formal Methods (SEFM)
series_title: LNCS
status: public
title: Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning
type: conference
user_id: '477'
year: '2015'
...
---
_id: '283'
abstract:
- lang: eng
text: Today, software verification is an established analysis method which can provide
high guarantees for software safety. However, the resources (time and/or memory)
for an exhaustive verification are not always available, and analysis then has
to resort to other techniques, like testing. Most often, the already achieved
partial verification results arediscarded in this case, and testing has to start
from scratch.In this paper, we propose a method for combining verification and
testing in which testing only needs to check the residual fraction of an uncompleted
verification. To this end, the partial results of a verification run are used
to construct a residual program (and residual assertions to be checked on it).
The residual program can afterwards be fed into standardtesting tools. The proposed
technique is sound modulo the soundness of the testing procedure. Experimental
results show that this combinedusage of verification and testing can significantly
reduce the effort for the subsequent testing.
author:
- first_name: Mike
full_name: Czech, Mike
last_name: Czech
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Czech M, Jakobs M-C, Wehrheim H. Just test what you cannot verify! In: Egyed
A, Schaefer I, eds. Fundamental Approaches to Software Engineering. Lecture
Notes in Computer Science. ; 2015:100-114. doi:10.1007/978-3-662-46675-9_7'
apa: Czech, M., Jakobs, M.-C., & Wehrheim, H. (2015). Just test what you cannot
verify! In A. Egyed & I. Schaefer (Eds.), Fundamental Approaches to Software
Engineering (pp. 100–114). https://doi.org/10.1007/978-3-662-46675-9_7
bibtex: '@inproceedings{Czech_Jakobs_Wehrheim_2015, series={Lecture Notes in Computer
Science}, title={Just test what you cannot verify!}, DOI={10.1007/978-3-662-46675-9_7},
booktitle={Fundamental Approaches to Software Engineering}, author={Czech, Mike
and Jakobs, Marie-Christine and Wehrheim, Heike}, editor={Egyed, Alexander and
Schaefer, InaEditors}, year={2015}, pages={100–114}, collection={Lecture Notes
in Computer Science} }'
chicago: Czech, Mike, Marie-Christine Jakobs, and Heike Wehrheim. “Just Test What
You Cannot Verify!” In Fundamental Approaches to Software Engineering,
edited by Alexander Egyed and Ina Schaefer, 100–114. Lecture Notes in Computer
Science, 2015. https://doi.org/10.1007/978-3-662-46675-9_7.
ieee: M. Czech, M.-C. Jakobs, and H. Wehrheim, “Just test what you cannot verify!,”
in Fundamental Approaches to Software Engineering, 2015, pp. 100–114.
mla: Czech, Mike, et al. “Just Test What You Cannot Verify!” Fundamental Approaches
to Software Engineering, edited by Alexander Egyed and Ina Schaefer, 2015,
pp. 100–14, doi:10.1007/978-3-662-46675-9_7.
short: 'M. Czech, M.-C. Jakobs, H. Wehrheim, in: A. Egyed, I. Schaefer (Eds.), Fundamental
Approaches to Software Engineering, 2015, pp. 100–114.'
date_created: 2017-10-17T12:41:47Z
date_updated: 2022-01-06T06:58:00Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-662-46675-9_7
editor:
- first_name: Alexander
full_name: Egyed, Alexander
last_name: Egyed
- first_name: Ina
full_name: Schaefer, Ina
last_name: Schaefer
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-21T09:25:36Z
date_updated: 2018-03-21T09:25:36Z
file_id: '1469'
file_name: 283-FASEsubmission38_01.pdf
file_size: 391253
relation: main_file
success: 1
file_date_updated: 2018-03-21T09:25:36Z
has_accepted_license: '1'
language:
- iso: eng
page: 100-114
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Fundamental Approaches to Software Engineering
series_title: Lecture Notes in Computer Science
status: public
title: Just test what you cannot verify!
type: conference
user_id: '477'
year: '2015'
...
---
_id: '285'
abstract:
- lang: eng
text: We propose an incremental workflow for the verification of parameterized systems
modeled as symmetric networks of timed automata. Starting with a small number
of timed automata in the network, a safety property is verified using IC3, a state-of-the-art
algorithm based on induction.The result of the verification, an inductive strengthening,
is reused proposing a candidate inductive strengthening for a larger network.If
the candidate is valid, our main theorem states that the safety property holds
for all sizes of the network of timed automata. Otherwise the number of automata
is increased and the next iteration is started with a new run of IC3.We propose
and thoroughly examine optimizations to our workflow, e.g. Feedback mechanisms
to speed up the run of IC3.
author:
- first_name: Tobias
full_name: Isenberg, Tobias
last_name: Isenberg
citation:
ama: 'Isenberg T. Incremental Inductive Verification of Parameterized Timed Systems.
In: Proceedings of the 15th International Conference on Application of Concurrency
to System Design (ACSD). ; 2015:1-9. doi:10.1109/ACSD.2015.13'
apa: Isenberg, T. (2015). Incremental Inductive Verification of Parameterized Timed
Systems. In Proceedings of the 15th International Conference on Application
of Concurrency to System Design (ACSD) (pp. 1–9). https://doi.org/10.1109/ACSD.2015.13
bibtex: '@inproceedings{Isenberg_2015, title={Incremental Inductive Verification
of Parameterized Timed Systems}, DOI={10.1109/ACSD.2015.13},
booktitle={Proceedings of the 15th International Conference on Application of
Concurrency to System Design (ACSD)}, author={Isenberg, Tobias}, year={2015},
pages={1–9} }'
chicago: Isenberg, Tobias. “Incremental Inductive Verification of Parameterized
Timed Systems.” In Proceedings of the 15th International Conference on Application
of Concurrency to System Design (ACSD), 1–9, 2015. https://doi.org/10.1109/ACSD.2015.13.
ieee: T. Isenberg, “Incremental Inductive Verification of Parameterized Timed Systems,”
in Proceedings of the 15th International Conference on Application of Concurrency
to System Design (ACSD), 2015, pp. 1–9.
mla: Isenberg, Tobias. “Incremental Inductive Verification of Parameterized Timed
Systems.” Proceedings of the 15th International Conference on Application of
Concurrency to System Design (ACSD), 2015, pp. 1–9, doi:10.1109/ACSD.2015.13.
short: 'T. Isenberg, in: Proceedings of the 15th International Conference on Application
of Concurrency to System Design (ACSD), 2015, pp. 1–9.'
date_created: 2017-10-17T12:41:47Z
date_updated: 2022-01-06T06:58:07Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1109/ACSD.2015.13
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-21T09:23:45Z
date_updated: 2018-03-21T09:23:45Z
file_id: '1466'
file_name: 285-07352419.pdf
file_size: 479808
relation: main_file
success: 1
file_date_updated: 2018-03-21T09:23:45Z
has_accepted_license: '1'
language:
- iso: eng
page: '1-9 '
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 15th International Conference on Application of Concurrency
to System Design (ACSD)
status: public
title: Incremental Inductive Verification of Parameterized Timed Systems
type: conference
user_id: '477'
year: '2015'
...
---
_id: '262'
abstract:
- lang: eng
text: Programs from Proofs" is a generic method which generates new programs out
of correctness proofs of given programs. The technique ensures that the new and
given program are behaviorally equivalent and that the new program is easily verifiable,
thus serving as an alternative to proof-carrying code concepts. So far, this generic
method has one instantiation that verifies type-state properties of programs.
In this paper, we present a whole range of new instantiations, all based on data
ow analyses. More precisely, we show how an imprecise but fast data ow analysis
can be enhanced with a predicate analysis as to yield a precise but expensive
analysis. Out of the safety proofs of this analysis, we generate new programs,
again behaviorally equivalent to the given ones, which are easily verifiable"
in the sense that now the data ow analysis alone can yield precise results. An
experimental evaluation practically supports our claim of easy verification.
author:
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Jakobs M-C, Wehrheim H. Programs from Proofs of Predicated Dataflow Analyses.
In: Proceedings of the 30th Annual ACM Symposium on Applied Computing.
SAC ’15. ; 2015:1729-1736. doi:10.1145/2695664.2695690'
apa: Jakobs, M.-C., & Wehrheim, H. (2015). Programs from Proofs of Predicated
Dataflow Analyses. In Proceedings of the 30th Annual ACM Symposium on Applied
Computing (pp. 1729–1736). https://doi.org/10.1145/2695664.2695690
bibtex: '@inproceedings{Jakobs_Wehrheim_2015, series={SAC ’15}, title={Programs
from Proofs of Predicated Dataflow Analyses}, DOI={10.1145/2695664.2695690},
booktitle={Proceedings of the 30th Annual ACM Symposium on Applied Computing},
author={Jakobs, Marie-Christine and Wehrheim, Heike}, year={2015}, pages={1729–1736},
collection={SAC ’15} }'
chicago: Jakobs, Marie-Christine, and Heike Wehrheim. “Programs from Proofs of Predicated
Dataflow Analyses.” In Proceedings of the 30th Annual ACM Symposium on Applied
Computing, 1729–36. SAC ’15, 2015. https://doi.org/10.1145/2695664.2695690.
ieee: M.-C. Jakobs and H. Wehrheim, “Programs from Proofs of Predicated Dataflow
Analyses,” in Proceedings of the 30th Annual ACM Symposium on Applied Computing,
2015, pp. 1729–1736.
mla: Jakobs, Marie-Christine, and Heike Wehrheim. “Programs from Proofs of Predicated
Dataflow Analyses.” Proceedings of the 30th Annual ACM Symposium on Applied
Computing, 2015, pp. 1729–36, doi:10.1145/2695664.2695690.
short: 'M.-C. Jakobs, H. Wehrheim, in: Proceedings of the 30th Annual ACM Symposium
on Applied Computing, 2015, pp. 1729–1736.'
date_created: 2017-10-17T12:41:43Z
date_updated: 2022-01-06T06:57:18Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1145/2695664.2695690
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-21T09:35:34Z
date_updated: 2018-03-21T09:35:34Z
file_id: '1483'
file_name: 262-mainSACfinal.pdf
file_size: 554583
relation: main_file
success: 1
file_date_updated: 2018-03-21T09:35:34Z
has_accepted_license: '1'
language:
- iso: eng
page: 1729-1736
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 30th Annual ACM Symposium on Applied Computing
series_title: SAC '15
status: public
title: Programs from Proofs of Predicated Dataflow Analyses
type: conference
user_id: '477'
year: '2015'
...
---
_id: '269'
abstract:
- lang: eng
text: Proof-carrying hardware is an approach that has recently been proposed for
the efficient verification of reconfigurable modules. We present an application
of proof-carrying hardware to guarantee the correct functionality of dynamically
reconfigured image processing modules. Our prototype comprises a reconfigurable-system-on-chip
with an embedded virtual FPGA fabric. This setup allows us to leverage open source
FPGA synthesis and backend tools to produce FPGA configuration bitstreams with
an open format and, thus, to demonstrate and experimentally evaluate proof-carrying
hardware at the bitstream level.
author:
- first_name: Tobias
full_name: Wiersema, Tobias
id: '3118'
last_name: Wiersema
- first_name: Sen
full_name: Wu, Sen
last_name: Wu
- first_name: Marco
full_name: Platzner, Marco
id: '398'
last_name: Platzner
citation:
ama: 'Wiersema T, Wu S, Platzner M. On-The-Fly Verification of Reconfigurable Image
Processing Modules based on a Proof-Carrying Hardware Approach. In: Proceedings
of the International Symposium in Reconfigurable Computing (ARC). LNCS. ;
2015:365--372. doi:10.1007/978-3-319-16214-0_32'
apa: Wiersema, T., Wu, S., & Platzner, M. (2015). On-The-Fly Verification of
Reconfigurable Image Processing Modules based on a Proof-Carrying Hardware Approach.
In Proceedings of the International Symposium in Reconfigurable Computing (ARC)
(pp. 365--372). https://doi.org/10.1007/978-3-319-16214-0_32
bibtex: '@inproceedings{Wiersema_Wu_Platzner_2015, series={LNCS}, title={On-The-Fly
Verification of Reconfigurable Image Processing Modules based on a Proof-Carrying
Hardware Approach}, DOI={10.1007/978-3-319-16214-0_32},
booktitle={Proceedings of the International Symposium in Reconfigurable Computing
(ARC)}, author={Wiersema, Tobias and Wu, Sen and Platzner, Marco}, year={2015},
pages={365--372}, collection={LNCS} }'
chicago: Wiersema, Tobias, Sen Wu, and Marco Platzner. “On-The-Fly Verification
of Reconfigurable Image Processing Modules Based on a Proof-Carrying Hardware
Approach.” In Proceedings of the International Symposium in Reconfigurable
Computing (ARC), 365--372. LNCS, 2015. https://doi.org/10.1007/978-3-319-16214-0_32.
ieee: T. Wiersema, S. Wu, and M. Platzner, “On-The-Fly Verification of Reconfigurable
Image Processing Modules based on a Proof-Carrying Hardware Approach,” in Proceedings
of the International Symposium in Reconfigurable Computing (ARC), 2015, pp.
365--372.
mla: Wiersema, Tobias, et al. “On-The-Fly Verification of Reconfigurable Image Processing
Modules Based on a Proof-Carrying Hardware Approach.” Proceedings of the International
Symposium in Reconfigurable Computing (ARC), 2015, pp. 365--372, doi:10.1007/978-3-319-16214-0_32.
short: 'T. Wiersema, S. Wu, M. Platzner, in: Proceedings of the International Symposium
in Reconfigurable Computing (ARC), 2015, pp. 365--372.'
date_created: 2017-10-17T12:41:44Z
date_updated: 2022-01-06T06:57:30Z
ddc:
- '040'
department:
- _id: '78'
doi: 10.1007/978-3-319-16214-0_32
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-21T09:32:42Z
date_updated: 2018-03-21T09:32:42Z
file_id: '1477'
file_name: 269-paper_53.pdf
file_size: 344309
relation: main_file
success: 1
file_date_updated: 2018-03-21T09:32:42Z
has_accepted_license: '1'
language:
- iso: eng
page: 365--372
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the International Symposium in Reconfigurable Computing
(ARC)
series_title: LNCS
status: public
title: On-The-Fly Verification of Reconfigurable Image Processing Modules based on
a Proof-Carrying Hardware Approach
type: conference
user_id: '477'
year: '2015'
...
---
_id: '5207'
author:
- first_name: Li
full_name: Li, Li
last_name: Li
- first_name: Alexandre
full_name: Bartel, Alexandre
last_name: Bartel
- first_name: Tegawende F.
full_name: Bissyande, Tegawende F.
last_name: Bissyande
- first_name: Jacques
full_name: Klein, Jacques
last_name: Klein
- first_name: Yves
full_name: Le Traon, Yves
last_name: Le Traon
- first_name: Steven
full_name: Arzt, Steven
last_name: Arzt
- first_name: Siegfried
full_name: Rasthofer, Siegfried
last_name: Rasthofer
- first_name: Eric
full_name: Bodden, Eric
id: '59256'
last_name: Bodden
orcid: 0000-0003-3470-3647
- first_name: Damien
full_name: Octeau, Damien
last_name: Octeau
- first_name: Patrick
full_name: McDaniel, Patrick
last_name: McDaniel
citation:
ama: 'Li L, Bartel A, Bissyande TF, et al. IccTA: Detecting Inter-Component Privacy
Leaks in Android Apps. In: 2015 International Conference on Software Engineering
(ICSE). ; 2015:280-291.'
apa: 'Li, L., Bartel, A., Bissyande, T. F., Klein, J., Le Traon, Y., Arzt, S., …
McDaniel, P. (2015). IccTA: Detecting Inter-Component Privacy Leaks in Android
Apps. In 2015 International Conference on Software Engineering (ICSE) (pp.
280–291).'
bibtex: '@inproceedings{Li_Bartel_Bissyande_Klein_Le Traon_Arzt_Rasthofer_Bodden_Octeau_McDaniel_2015,
title={IccTA: Detecting Inter-Component Privacy Leaks in Android Apps}, booktitle={2015
International Conference on Software Engineering (ICSE)}, author={Li, Li and Bartel,
Alexandre and Bissyande, Tegawende F. and Klein, Jacques and Le Traon, Yves and
Arzt, Steven and Rasthofer, Siegfried and Bodden, Eric and Octeau, Damien and
McDaniel, Patrick}, year={2015}, pages={280–291} }'
chicago: 'Li, Li, Alexandre Bartel, Tegawende F. Bissyande, Jacques Klein, Yves
Le Traon, Steven Arzt, Siegfried Rasthofer, Eric Bodden, Damien Octeau, and Patrick
McDaniel. “IccTA: Detecting Inter-Component Privacy Leaks in Android Apps.” In
2015 International Conference on Software Engineering (ICSE), 280–91, 2015.'
ieee: 'L. Li et al., “IccTA: Detecting Inter-Component Privacy Leaks in Android
Apps,” in 2015 International Conference on Software Engineering (ICSE),
2015, pp. 280–291.'
mla: 'Li, Li, et al. “IccTA: Detecting Inter-Component Privacy Leaks in Android
Apps.” 2015 International Conference on Software Engineering (ICSE), 2015,
pp. 280–91.'
short: 'L. Li, A. Bartel, T.F. Bissyande, J. Klein, Y. Le Traon, S. Arzt, S. Rasthofer,
E. Bodden, D. Octeau, P. McDaniel, in: 2015 International Conference on Software
Engineering (ICSE), 2015, pp. 280–291.'
date_created: 2018-10-31T12:59:44Z
date_updated: 2022-01-06T07:01:46Z
ddc:
- '000'
department:
- _id: '76'
extern: '1'
file:
- access_level: closed
content_type: application/pdf
creator: ups
date_created: 2018-11-02T14:10:22Z
date_updated: 2018-11-02T14:10:22Z
file_id: '5263'
file_name: lbb+15iccta.pdf
file_size: 206378
relation: main_file
success: 1
file_date_updated: 2018-11-02T14:10:22Z
has_accepted_license: '1'
keyword:
- CROSSING
- ATTRACT
- ITSECWEBSITE
language:
- iso: eng
main_file_link:
- url: http://www.bodden.de/pubs/lbb+15iccta.pdf
page: 280-291
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
publication: 2015 International Conference on Software Engineering (ICSE)
publication_identifier:
isbn:
- 978-1-4799-1934-5
status: public
title: 'IccTA: Detecting Inter-Component Privacy Leaks in Android Apps'
type: conference
user_id: '477'
year: '2015'
...
---
_id: '10714'
author:
- first_name: Roland
full_name: Meißner, Roland
last_name: Meißner
citation:
ama: Meißner R. Konzept Und Implementation Einer Benutzeroberfläche Zur Generierung
Virtueller FPGAs. Universität Paderborn; 2015.
apa: Meißner, R. (2015). Konzept und Implementation einer Benutzeroberfläche
zur Generierung virtueller FPGAs. Universität Paderborn.
bibtex: '@book{Meißner_2015, title={Konzept und Implementation einer Benutzeroberfläche
zur Generierung virtueller FPGAs}, publisher={Universität Paderborn}, author={Meißner,
Roland}, year={2015} }'
chicago: Meißner, Roland. Konzept Und Implementation Einer Benutzeroberfläche
Zur Generierung Virtueller FPGAs. Universität Paderborn, 2015.
ieee: R. Meißner, Konzept und Implementation einer Benutzeroberfläche zur Generierung
virtueller FPGAs. Universität Paderborn, 2015.
mla: Meißner, Roland. Konzept Und Implementation Einer Benutzeroberfläche Zur
Generierung Virtueller FPGAs. Universität Paderborn, 2015.
short: R. Meißner, Konzept Und Implementation Einer Benutzeroberfläche Zur Generierung
Virtueller FPGAs, Universität Paderborn, 2015.
date_created: 2019-07-10T11:48:25Z
date_updated: 2022-01-06T06:50:50Z
department:
- _id: '78'
language:
- iso: eng
project:
- _id: '12'
name: SFB 901 - Subproject B4
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Tobias
full_name: Wiersema, Tobias
id: '3118'
last_name: Wiersema
title: Konzept und Implementation einer Benutzeroberfläche zur Generierung virtueller
FPGAs
type: bachelorsthesis
user_id: '477'
year: '2015'
...
---
_id: '331'
author:
- first_name: Sen
full_name: Wu, Sen
last_name: Wu
citation:
ama: Wu S. Webcam Application Using Virtual FPGA. Universität Paderborn;
2014.
apa: Wu, S. (2014). Webcam application using virtual FPGA. Universität Paderborn.
bibtex: '@book{Wu_2014, title={Webcam application using virtual FPGA}, publisher={Universität
Paderborn}, author={Wu, Sen}, year={2014} }'
chicago: Wu, Sen. Webcam Application Using Virtual FPGA. Universität Paderborn,
2014.
ieee: S. Wu, Webcam application using virtual FPGA. Universität Paderborn,
2014.
mla: Wu, Sen. Webcam Application Using Virtual FPGA. Universität Paderborn,
2014.
short: S. Wu, Webcam Application Using Virtual FPGA, Universität Paderborn, 2014.
date_created: 2017-10-17T12:41:56Z
date_updated: 2022-01-06T06:59:10Z
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publisher: Universität Paderborn
status: public
title: Webcam application using virtual FPGA
type: bachelorsthesis
user_id: '477'
year: '2014'
...
---
_id: '340'
author:
- first_name: Philipp
full_name: Korth, Philipp
last_name: Korth
citation:
ama: Korth P. Untersuchung transitiver Eigenschaften der Technik “Programs from
Proofs.” Universität Paderborn; 2014.
apa: Korth, P. (2014). Untersuchung transitiver Eigenschaften der Technik “Programs
from Proofs.” Universität Paderborn.
bibtex: '@book{Korth_2014, title={Untersuchung transitiver Eigenschaften der Technik
“Programs from Proofs”}, publisher={Universität Paderborn}, author={Korth, Philipp},
year={2014} }'
chicago: Korth, Philipp. Untersuchung transitiver Eigenschaften der Technik “Programs
from Proofs.” Universität Paderborn, 2014.
ieee: P. Korth, Untersuchung transitiver Eigenschaften der Technik “Programs
from Proofs.” Universität Paderborn, 2014.
mla: Korth, Philipp. Untersuchung transitiver Eigenschaften der Technik “Programs
from Proofs.” Universität Paderborn, 2014.
short: P. Korth, Untersuchung transitiver Eigenschaften der Technik “Programs from
Proofs,” Universität Paderborn, 2014.
date_created: 2017-10-17T12:41:58Z
date_updated: 2022-01-06T06:59:14Z
department:
- _id: '77'
language:
- iso: ger
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Heike
full_name: Wehrheim, Heike
last_name: Wehrheim
title: Untersuchung transitiver Eigenschaften der Technik "Programs from Proofs"
type: bachelorsthesis
user_id: '15504'
year: '2014'
...
---
_id: '342'
author:
- first_name: Christoph
full_name: Klauke, Christoph
last_name: Klauke
citation:
ama: Klauke C. Transformation Graphischer Protokollspezifikationen in Model-Checker-Anfragen.
Universität Paderborn; 2014.
apa: Klauke, C. (2014). Transformation graphischer Protokollspezifikationen in
Model-Checker-Anfragen. Universität Paderborn.
bibtex: '@book{Klauke_2014, title={Transformation graphischer Protokollspezifikationen
in Model-Checker-Anfragen}, publisher={Universität Paderborn}, author={Klauke,
Christoph}, year={2014} }'
chicago: Klauke, Christoph. Transformation Graphischer Protokollspezifikationen
in Model-Checker-Anfragen. Universität Paderborn, 2014.
ieee: C. Klauke, Transformation graphischer Protokollspezifikationen in Model-Checker-Anfragen.
Universität Paderborn, 2014.
mla: Klauke, Christoph. Transformation Graphischer Protokollspezifikationen in
Model-Checker-Anfragen. Universität Paderborn, 2014.
short: C. Klauke, Transformation Graphischer Protokollspezifikationen in Model-Checker-Anfragen,
Universität Paderborn, 2014.
date_created: 2017-10-17T12:41:58Z
date_updated: 2022-01-06T06:59:15Z
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publisher: Universität Paderborn
status: public
title: Transformation graphischer Protokollspezifikationen in Model-Checker-Anfragen
type: bachelorsthesis
user_id: '477'
year: '2014'
...
---
_id: '383'
abstract:
- lang: eng
text: Proof-carrying code approaches aim at safe execution of untrusted code by
having the code producer attach a safety proof to the code which the code consumer
only has to validate. Depending on the type of safety property, proofs can however
become quite large and their validation - though faster than their construction
- still time consuming. In this paper we introduce a new concept for safe execution
of untrusted code. It keeps the idea of putting the time consuming part of proving
on the side of the code producer, however, attaches no proofs to code anymore
but instead uses the proof to transform the program into an equivalent but more
efficiently verifiable program. Code consumers thus still do proving themselves,
however, on a computationally inexpensive level only. Experimental results show
that the proof effort can be reduced by several orders of magnitude, both with
respect to time and space.
author:
- first_name: Daniel
full_name: Wonisch, Daniel
last_name: Wonisch
- first_name: Alexander
full_name: Schremmer, Alexander
last_name: Schremmer
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Wonisch D, Schremmer A, Wehrheim H. Programs from Proofs -- Approach and Applications.
In: Proceedings of the Software Engineering Conference (SE). Lecture Notes
in Informatics (LNI). ; 2014:67-68.'
apa: Wonisch, D., Schremmer, A., & Wehrheim, H. (2014). Programs from Proofs
-- Approach and Applications. In Proceedings of the Software Engineering Conference
(SE) (pp. 67–68).
bibtex: '@inproceedings{Wonisch_Schremmer_Wehrheim_2014, series={Lecture Notes in
Informatics (LNI)}, title={Programs from Proofs -- Approach and Applications},
booktitle={Proceedings of the Software Engineering Conference (SE)}, author={Wonisch,
Daniel and Schremmer, Alexander and Wehrheim, Heike}, year={2014}, pages={67–68},
collection={Lecture Notes in Informatics (LNI)} }'
chicago: Wonisch, Daniel, Alexander Schremmer, and Heike Wehrheim. “Programs from
Proofs -- Approach and Applications.” In Proceedings of the Software Engineering
Conference (SE), 67–68. Lecture Notes in Informatics (LNI), 2014.
ieee: D. Wonisch, A. Schremmer, and H. Wehrheim, “Programs from Proofs -- Approach
and Applications,” in Proceedings of the Software Engineering Conference (SE),
2014, pp. 67–68.
mla: Wonisch, Daniel, et al. “Programs from Proofs -- Approach and Applications.”
Proceedings of the Software Engineering Conference (SE), 2014, pp. 67–68.
short: 'D. Wonisch, A. Schremmer, H. Wehrheim, in: Proceedings of the Software Engineering
Conference (SE), 2014, pp. 67–68.'
date_created: 2017-10-17T12:42:06Z
date_updated: 2022-01-06T06:59:38Z
ddc:
- '040'
department:
- _id: '77'
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-20T07:04:52Z
date_updated: 2018-03-20T07:04:52Z
file_id: '1392'
file_name: 383-programmsFromProofsSE.pdf
file_size: 66474
relation: main_file
success: 1
file_date_updated: 2018-03-20T07:04:52Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- url: http://eprints.uni-kiel.de/23752/
page: 67-68
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the Software Engineering Conference (SE)
series_title: Lecture Notes in Informatics (LNI)
status: public
title: Programs from Proofs -- Approach and Applications
type: conference
user_id: '477'
year: '2014'
...
---
_id: '450'
abstract:
- lang: eng
text: 'Configurable program analysis (CPA) is a generic concept for the formalization
of different software analysis techniques in a single framework. With the tool
CPAchecker, this framework allows for an easy configuration and subsequent automatic
execution of analysis procedures ranging from data-flow analysis to model checking.
The focus of the tool CPAchecker is thus on analysis. In this paper, we study
configurability from the point of view of software certification. Certification
aims at providing (via a prior analysis) a certificate of correctness for a program
which is (a) tamper-proof and (b) more efficient to check for validity than a
full analysis. Here, we will show how, given an analysis instance of a CPA, to
construct a corresponding sound certification instance, thereby arriving at configurable
program certification. We report on experiments with certification based on different
analysis techniques, and in particular explain which characteristics of an underlying
analysis allow us to design an efficient (in the above (b) sense) certification
procedure. '
author:
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Jakobs M-C, Wehrheim H. Certification for Configurable Program Analysis. In:
Proceedings of the 21st International Symposium on Model Checking of Software
(SPIN). SPIN 2014. ; 2014:30-39. doi:10.1145/2632362.2632372'
apa: Jakobs, M.-C., & Wehrheim, H. (2014). Certification for Configurable Program
Analysis. In Proceedings of the 21st International Symposium on Model Checking
of Software (SPIN) (pp. 30–39). https://doi.org/10.1145/2632362.2632372
bibtex: '@inproceedings{Jakobs_Wehrheim_2014, series={SPIN 2014}, title={Certification
for Configurable Program Analysis}, DOI={10.1145/2632362.2632372},
booktitle={Proceedings of the 21st International Symposium on Model Checking of
Software (SPIN)}, author={Jakobs, Marie-Christine and Wehrheim, Heike}, year={2014},
pages={30–39}, collection={SPIN 2014} }'
chicago: Jakobs, Marie-Christine, and Heike Wehrheim. “Certification for Configurable
Program Analysis.” In Proceedings of the 21st International Symposium on Model
Checking of Software (SPIN), 30–39. SPIN 2014, 2014. https://doi.org/10.1145/2632362.2632372.
ieee: M.-C. Jakobs and H. Wehrheim, “Certification for Configurable Program Analysis,”
in Proceedings of the 21st International Symposium on Model Checking of Software
(SPIN), 2014, pp. 30–39.
mla: Jakobs, Marie-Christine, and Heike Wehrheim. “Certification for Configurable
Program Analysis.” Proceedings of the 21st International Symposium on Model
Checking of Software (SPIN), 2014, pp. 30–39, doi:10.1145/2632362.2632372.
short: 'M.-C. Jakobs, H. Wehrheim, in: Proceedings of the 21st International Symposium
on Model Checking of Software (SPIN), 2014, pp. 30–39.'
date_created: 2017-10-17T12:42:19Z
date_updated: 2022-01-06T07:01:07Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1145/2632362.2632372
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-16T11:25:35Z
date_updated: 2018-03-16T11:25:35Z
file_id: '1345'
file_name: 450-p30-jakobs.pdf
file_size: 487366
relation: main_file
success: 1
file_date_updated: 2018-03-16T11:25:35Z
has_accepted_license: '1'
language:
- iso: eng
page: 30-39
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 21st International Symposium on Model Checking of
Software (SPIN)
series_title: SPIN 2014
status: public
title: Certification for Configurable Program Analysis
type: conference
user_id: '477'
year: '2014'
...
---
_id: '399'
abstract:
- lang: eng
text: Ensuring memory access security is a challenge for reconfigurable systems
with multiple cores. Previous work introduced access monitors attached to the
memory subsystem to ensure that the cores adhere to pre-defined protocols when
accessing memory. In this paper, we combine access monitors with a formal runtime
verification technique known as proof-carrying hardware to guarantee memory security.
We extend previous work on proof-carrying hardware by covering sequential circuits
and demonstrate our approach with a prototype leveraging ReconOS/Zynq with an
embedded ZUMA virtual FPGA overlay. Experiments show the feasibility of the approach
and the capabilities of the prototype, which constitutes the first realization
of proof-carrying hardware on real FPGAs. The area overheads for the virtual FPGA
are measured as 2x-10x, depending on the resource type. The delay overhead is
substantial with almost 100x, but this is an extremely pessimistic estimate that
will be lowered once accurate timing analysis for FPGA overlays become available.
Finally, reconfiguration time for the virtual FPGA is about one order of magnitude
lower than for the native Zynq fabric.
author:
- first_name: Tobias
full_name: Wiersema, Tobias
id: '3118'
last_name: Wiersema
- first_name: Stephanie
full_name: Drzevitzky, Stephanie
last_name: Drzevitzky
- first_name: Marco
full_name: Platzner, Marco
id: '398'
last_name: Platzner
citation:
ama: 'Wiersema T, Drzevitzky S, Platzner M. Memory Security in Reconfigurable Computers:
Combining Formal Verification with Monitoring. In: Proceedings of the International
Conference on Field-Programmable Technology (FPT). ; 2014:167-174. doi:10.1109/FPT.2014.7082771'
apa: 'Wiersema, T., Drzevitzky, S., & Platzner, M. (2014). Memory Security in
Reconfigurable Computers: Combining Formal Verification with Monitoring. In Proceedings
of the International Conference on Field-Programmable Technology (FPT) (pp.
167–174). https://doi.org/10.1109/FPT.2014.7082771'
bibtex: '@inproceedings{Wiersema_Drzevitzky_Platzner_2014, title={Memory Security
in Reconfigurable Computers: Combining Formal Verification with Monitoring}, DOI={10.1109/FPT.2014.7082771},
booktitle={Proceedings of the International Conference on Field-Programmable Technology
(FPT)}, author={Wiersema, Tobias and Drzevitzky, Stephanie and Platzner, Marco},
year={2014}, pages={167–174} }'
chicago: 'Wiersema, Tobias, Stephanie Drzevitzky, and Marco Platzner. “Memory Security
in Reconfigurable Computers: Combining Formal Verification with Monitoring.” In
Proceedings of the International Conference on Field-Programmable Technology
(FPT), 167–74, 2014. https://doi.org/10.1109/FPT.2014.7082771.'
ieee: 'T. Wiersema, S. Drzevitzky, and M. Platzner, “Memory Security in Reconfigurable
Computers: Combining Formal Verification with Monitoring,” in Proceedings of
the International Conference on Field-Programmable Technology (FPT), 2014,
pp. 167–174.'
mla: 'Wiersema, Tobias, et al. “Memory Security in Reconfigurable Computers: Combining
Formal Verification with Monitoring.” Proceedings of the International Conference
on Field-Programmable Technology (FPT), 2014, pp. 167–74, doi:10.1109/FPT.2014.7082771.'
short: 'T. Wiersema, S. Drzevitzky, M. Platzner, in: Proceedings of the International
Conference on Field-Programmable Technology (FPT), 2014, pp. 167–174.'
date_created: 2017-10-17T12:42:09Z
date_updated: 2022-01-06T07:00:05Z
ddc:
- '040'
department:
- _id: '78'
doi: 10.1109/FPT.2014.7082771
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-20T06:57:44Z
date_updated: 2018-03-20T06:57:44Z
file_id: '1380'
file_name: 399-wiersema14_fpt_IEEE_approved.pdf
file_size: 404328
relation: main_file
success: 1
file_date_updated: 2018-03-20T06:57:44Z
has_accepted_license: '1'
language:
- iso: eng
page: 167-174
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the International Conference on Field-Programmable Technology
(FPT)
status: public
title: 'Memory Security in Reconfigurable Computers: Combining Formal Verification
with Monitoring'
type: conference
user_id: '477'
year: '2014'
...
---
_id: '408'
abstract:
- lang: eng
text: Verification of hardware and software usually proceeds separately, software
analysis relying on the correctness of processors executing instructions. This
assumption is valid as long as the software runs on standard CPUs that have been
extensively validated and are in wide use. However, for processors exploiting
custom instruction set extensions to meet performance and energy constraints the
validation might be less extensive, challenging the correctness assumption.In
this paper we present an approach for integrating software analyses with hardware
verification, specifically targeting custom instruction set extensions. We propose
three different techniques for deriving the properties to be proven for the hardware
implementation of a custom instruction in order to support software analyses.
The techniques are designed to explore the trade-off between generality and efficiency
and span from proving functional equivalence over checking the rules of a particular
analysis domain to verifying actual pre and post conditions resulting from program
analysis. We demonstrate and compare the three techniques on example programs
with custom instructions, using stateof-the-art software and hardware verification
techniques.
author:
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
- first_name: Marco
full_name: Platzner, Marco
id: '398'
last_name: Platzner
- first_name: Tobias
full_name: Wiersema, Tobias
id: '3118'
last_name: Wiersema
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Jakobs M-C, Platzner M, Wiersema T, Wehrheim H. Integrating Software and Hardware
Verification. In: Albert E, Sekerinski E, eds. Proceedings of the 11th International
Conference on Integrated Formal Methods (IFM). LNCS. ; 2014:307-322. doi:10.1007/978-3-319-10181-1_19'
apa: Jakobs, M.-C., Platzner, M., Wiersema, T., & Wehrheim, H. (2014). Integrating
Software and Hardware Verification. In E. Albert & E. Sekerinski (Eds.), Proceedings
of the 11th International Conference on Integrated Formal Methods (iFM) (pp.
307–322). https://doi.org/10.1007/978-3-319-10181-1_19
bibtex: '@inproceedings{Jakobs_Platzner_Wiersema_Wehrheim_2014, series={LNCS}, title={Integrating
Software and Hardware Verification}, DOI={10.1007/978-3-319-10181-1_19},
booktitle={Proceedings of the 11th International Conference on Integrated Formal
Methods (iFM)}, author={Jakobs, Marie-Christine and Platzner, Marco and Wiersema,
Tobias and Wehrheim, Heike}, editor={Albert, Elvira and Sekerinski, EmilEditors},
year={2014}, pages={307–322}, collection={LNCS} }'
chicago: Jakobs, Marie-Christine, Marco Platzner, Tobias Wiersema, and Heike Wehrheim.
“Integrating Software and Hardware Verification.” In Proceedings of the 11th
International Conference on Integrated Formal Methods (IFM), edited by Elvira
Albert and Emil Sekerinski, 307–22. LNCS, 2014. https://doi.org/10.1007/978-3-319-10181-1_19.
ieee: M.-C. Jakobs, M. Platzner, T. Wiersema, and H. Wehrheim, “Integrating Software
and Hardware Verification,” in Proceedings of the 11th International Conference
on Integrated Formal Methods (iFM), 2014, pp. 307–322.
mla: Jakobs, Marie-Christine, et al. “Integrating Software and Hardware Verification.”
Proceedings of the 11th International Conference on Integrated Formal Methods
(IFM), edited by Elvira Albert and Emil Sekerinski, 2014, pp. 307–22, doi:10.1007/978-3-319-10181-1_19.
short: 'M.-C. Jakobs, M. Platzner, T. Wiersema, H. Wehrheim, in: E. Albert, E. Sekerinski
(Eds.), Proceedings of the 11th International Conference on Integrated Formal
Methods (IFM), 2014, pp. 307–322.'
date_created: 2017-10-17T12:42:11Z
date_updated: 2022-01-06T07:00:14Z
ddc:
- '040'
department:
- _id: '77'
- _id: '78'
doi: 10.1007/978-3-319-10181-1_19
editor:
- first_name: Elvira
full_name: Albert, Elvira
last_name: Albert
- first_name: Emil
full_name: Sekerinski, Emil
last_name: Sekerinski
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-16T11:35:28Z
date_updated: 2018-03-16T11:35:28Z
file_id: '1364'
file_name: 408-jakobs14_ifm.pdf
file_size: 561325
relation: main_file
success: 1
file_date_updated: 2018-03-16T11:35:28Z
has_accepted_license: '1'
language:
- iso: eng
page: 307-322
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 11th International Conference on Integrated Formal
Methods (iFM)
series_title: LNCS
status: public
title: Integrating Software and Hardware Verification
type: conference
user_id: '477'
year: '2014'
...
---
_id: '418'
author:
- first_name: Felix
full_name: Pauck, Felix
id: '22398'
last_name: Pauck
citation:
ama: Pauck F. Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren.
Universität Paderborn; 2014.
apa: Pauck, F. (2014). Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren.
Universität Paderborn.
bibtex: '@book{Pauck_2014, title={Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren},
publisher={Universität Paderborn}, author={Pauck, Felix}, year={2014} }'
chicago: Pauck, Felix. Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren.
Universität Paderborn, 2014.
ieee: F. Pauck, Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren.
Universität Paderborn, 2014.
mla: Pauck, Felix. Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren.
Universität Paderborn, 2014.
short: F. Pauck, Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren,
Universität Paderborn, 2014.
date_created: 2017-10-17T12:42:13Z
date_updated: 2022-01-06T07:00:30Z
ddc:
- '000'
department:
- _id: '77'
file:
- access_level: open_access
content_type: application/pdf
creator: fpauck
date_created: 2019-08-07T09:00:20Z
date_updated: 2019-08-07T09:05:38Z
file_id: '12906'
file_name: fpauck_2014.pdf
file_size: 3191756
relation: main_file
title: Bachelorarbeit
file_date_updated: 2019-08-07T09:05:38Z
has_accepted_license: '1'
language:
- iso: ger
oa: '1'
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
title: Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren
type: bachelorsthesis
user_id: '22398'
year: '2014'
...
---
_id: '433'
abstract:
- lang: eng
text: Virtual FPGAs are overlay architectures realized on top of physical FPGAs.
They are proposed to enhance or abstract away from the physical FPGA for experimenting
with novel architectures and design tool flows. In this paper, we present an embedding
of a ZUMA-based virtual FPGA fabric into a complete configurable system-on-chip.
Such an embedding is required to fully harness the potential of virtual FPGAs,
in particular to give the virtual circuits access to main memory and operating
system services, and to enable a concurrent operation of virtualized and non-virtualized
circuitry. We discuss our extension to ZUMA and its embedding into the ReconOS
operating system for hardware/software systems. Furthermore, we present an open
source tool flow to synthesize configurations for the virtual FPGA.
author:
- first_name: Tobias
full_name: Wiersema, Tobias
id: '3118'
last_name: Wiersema
- first_name: Arne
full_name: Bockhorn, Arne
last_name: Bockhorn
- first_name: Marco
full_name: Platzner, Marco
id: '398'
last_name: Platzner
citation:
ama: 'Wiersema T, Bockhorn A, Platzner M. Embedding FPGA Overlays into Configurable
Systems-on-Chip: ReconOS meets ZUMA. In: Proceedings of the International Conference
on ReConFigurable Computing and FPGAs (ReConFig). ; 2014:1-6. doi:10.1109/ReConFig.2014.7032514'
apa: 'Wiersema, T., Bockhorn, A., & Platzner, M. (2014). Embedding FPGA Overlays
into Configurable Systems-on-Chip: ReconOS meets ZUMA. In Proceedings of the
International Conference on ReConFigurable Computing and FPGAs (ReConFig)
(pp. 1–6). https://doi.org/10.1109/ReConFig.2014.7032514'
bibtex: '@inproceedings{Wiersema_Bockhorn_Platzner_2014, title={Embedding FPGA Overlays
into Configurable Systems-on-Chip: ReconOS meets ZUMA}, DOI={10.1109/ReConFig.2014.7032514},
booktitle={Proceedings of the International Conference on ReConFigurable Computing
and FPGAs (ReConFig)}, author={Wiersema, Tobias and Bockhorn, Arne and Platzner,
Marco}, year={2014}, pages={1–6} }'
chicago: 'Wiersema, Tobias, Arne Bockhorn, and Marco Platzner. “Embedding FPGA Overlays
into Configurable Systems-on-Chip: ReconOS Meets ZUMA.” In Proceedings of the
International Conference on ReConFigurable Computing and FPGAs (ReConFig),
1–6, 2014. https://doi.org/10.1109/ReConFig.2014.7032514.'
ieee: 'T. Wiersema, A. Bockhorn, and M. Platzner, “Embedding FPGA Overlays into
Configurable Systems-on-Chip: ReconOS meets ZUMA,” in Proceedings of the International
Conference on ReConFigurable Computing and FPGAs (ReConFig), 2014, pp. 1–6.'
mla: 'Wiersema, Tobias, et al. “Embedding FPGA Overlays into Configurable Systems-on-Chip:
ReconOS Meets ZUMA.” Proceedings of the International Conference on ReConFigurable
Computing and FPGAs (ReConFig), 2014, pp. 1–6, doi:10.1109/ReConFig.2014.7032514.'
short: 'T. Wiersema, A. Bockhorn, M. Platzner, in: Proceedings of the International
Conference on ReConFigurable Computing and FPGAs (ReConFig), 2014, pp. 1–6.'
date_created: 2017-10-17T12:42:16Z
date_updated: 2022-01-06T07:00:56Z
ddc:
- '040'
department:
- _id: '78'
doi: 10.1109/ReConFig.2014.7032514
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-16T11:30:58Z
date_updated: 2018-03-16T11:30:58Z
file_id: '1355'
file_name: 433-wiersema14_reconfig_IEEE_approved.pdf
file_size: 369333
relation: main_file
success: 1
file_date_updated: 2018-03-16T11:30:58Z
has_accepted_license: '1'
language:
- iso: eng
page: '1-6 '
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the International Conference on ReConFigurable Computing
and FPGAs (ReConFig)
status: public
title: 'Embedding FPGA Overlays into Configurable Systems-on-Chip: ReconOS meets ZUMA'
type: conference
user_id: '477'
year: '2014'
...
---
_id: '5189'
author:
- first_name: Steven
full_name: Arzt, Steven
last_name: Arzt
- first_name: Siegfried
full_name: Rasthofer, Siegfried
last_name: Rasthofer
- first_name: Christian
full_name: Fritz, Christian
last_name: Fritz
- first_name: Eric
full_name: Bodden, Eric
id: '59256'
last_name: Bodden
orcid: 0000-0003-3470-3647
- first_name: Alexandre
full_name: Bartel, Alexandre
last_name: Bartel
- first_name: Jacques
full_name: Klein, Jacques
last_name: Klein
- first_name: Yves
full_name: Le Traon, Yves
last_name: Le Traon
- first_name: Damien
full_name: Octeau, Damien
last_name: Octeau
- first_name: Patrick
full_name: McDaniel, Patrick
last_name: McDaniel
citation:
ama: 'Arzt S, Rasthofer S, Fritz C, et al. FlowDroid: Precise Context, Flow, Field,
Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps. In: Proceedings
of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation
- PLDI ’14. ACM Press; 2014. doi:10.1145/2594291.2594299'
apa: 'Arzt, S., Rasthofer, S., Fritz, C., Bodden, E., Bartel, A., Klein, J., … McDaniel,
P. (2014). FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware
Taint Analysis for Android Apps. In Proceedings of the 35th ACM SIGPLAN Conference
on Programming Language Design and Implementation - PLDI ’14. ACM Press. https://doi.org/10.1145/2594291.2594299'
bibtex: '@inproceedings{Arzt_Rasthofer_Fritz_Bodden_Bartel_Klein_Le Traon_Octeau_McDaniel_2014,
title={FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware
Taint Analysis for Android Apps}, DOI={10.1145/2594291.2594299},
booktitle={Proceedings of the 35th ACM SIGPLAN Conference on Programming Language
Design and Implementation - PLDI ’14}, publisher={ACM Press}, author={Arzt, Steven
and Rasthofer, Siegfried and Fritz, Christian and Bodden, Eric and Bartel, Alexandre
and Klein, Jacques and Le Traon, Yves and Octeau, Damien and McDaniel, Patrick},
year={2014} }'
chicago: 'Arzt, Steven, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre
Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel. “FlowDroid:
Precise Context, Flow, Field, Object-Sensitive and Lifecycle-Aware Taint Analysis
for Android Apps.” In Proceedings of the 35th ACM SIGPLAN Conference on Programming
Language Design and Implementation - PLDI ’14. ACM Press, 2014. https://doi.org/10.1145/2594291.2594299.'
ieee: 'S. Arzt et al., “FlowDroid: Precise Context, Flow, Field, Object-sensitive
and Lifecycle-aware Taint Analysis for Android Apps,” in Proceedings of the
35th ACM SIGPLAN Conference on Programming Language Design and Implementation
- PLDI ’14, 2014.'
mla: 'Arzt, Steven, et al. “FlowDroid: Precise Context, Flow, Field, Object-Sensitive
and Lifecycle-Aware Taint Analysis for Android Apps.” Proceedings of the 35th
ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI
’14, ACM Press, 2014, doi:10.1145/2594291.2594299.'
short: 'S. Arzt, S. Rasthofer, C. Fritz, E. Bodden, A. Bartel, J. Klein, Y. Le Traon,
D. Octeau, P. McDaniel, in: Proceedings of the 35th ACM SIGPLAN Conference on
Programming Language Design and Implementation - PLDI ’14, ACM Press, 2014.'
date_created: 2018-10-31T10:55:28Z
date_updated: 2022-01-06T07:01:42Z
ddc:
- '000'
department:
- _id: '76'
doi: 10.1145/2594291.2594299
extern: '1'
file:
- access_level: closed
content_type: application/pdf
creator: ups
date_created: 2018-11-02T13:59:33Z
date_updated: 2018-11-02T13:59:33Z
file_id: '5258'
file_name: p259-arzt.pdf
file_size: 406920
relation: main_file
success: 1
file_date_updated: 2018-11-02T13:59:33Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- url: http://www.bodden.de/pubs/far+14flowdroid.pdf
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
publication: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language
Design and Implementation - PLDI '14
publication_identifier:
isbn:
- '9781450327848'
publication_status: published
publisher: ACM Press
status: public
title: 'FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware
Taint Analysis for Android Apps'
type: conference
user_id: '477'
year: '2014'
...
---
_id: '5190'
author:
- first_name: Steven
full_name: Arzt, Steven
last_name: Arzt
- first_name: Siegfried
full_name: Rasthofer, Siegfried
last_name: Rasthofer
- first_name: Enrico
full_name: Lovat, Enrico
last_name: Lovat
- first_name: Eric
full_name: Bodden, Eric
id: '59256'
last_name: Bodden
orcid: 0000-0003-3470-3647
citation:
ama: 'Arzt S, Rasthofer S, Lovat E, Bodden E. DroidForce: Enforcing Complex, Data-Centric,
System-Wide Policies in Android. In: International Conference on Availability,
Reliability and Security (ARES 2014). IEEE; 2014:40-49.'
apa: 'Arzt, S., Rasthofer, S., Lovat, E., & Bodden, E. (2014). DroidForce: Enforcing
Complex, Data-Centric, System-Wide Policies in Android. In International Conference
on Availability, Reliability and Security (ARES 2014) (pp. 40–49). IEEE.'
bibtex: '@inproceedings{Arzt_Rasthofer_Lovat_Bodden_2014, title={DroidForce: Enforcing
Complex, Data-Centric, System-Wide Policies in Android}, booktitle={International
Conference on Availability, Reliability and Security (ARES 2014)}, publisher={IEEE},
author={Arzt, Steven and Rasthofer, Siegfried and Lovat, Enrico and Bodden, Eric},
year={2014}, pages={40–49} }'
chicago: 'Arzt, Steven, Siegfried Rasthofer, Enrico Lovat, and Eric Bodden. “DroidForce:
Enforcing Complex, Data-Centric, System-Wide Policies in Android.” In International
Conference on Availability, Reliability and Security (ARES 2014), 40–49. IEEE,
2014.'
ieee: 'S. Arzt, S. Rasthofer, E. Lovat, and E. Bodden, “DroidForce: Enforcing Complex,
Data-Centric, System-Wide Policies in Android,” in International Conference
on Availability, Reliability and Security (ARES 2014), 2014, pp. 40–49.'
mla: 'Arzt, Steven, et al. “DroidForce: Enforcing Complex, Data-Centric, System-Wide
Policies in Android.” International Conference on Availability, Reliability
and Security (ARES 2014), IEEE, 2014, pp. 40–49.'
short: 'S. Arzt, S. Rasthofer, E. Lovat, E. Bodden, in: International Conference
on Availability, Reliability and Security (ARES 2014), IEEE, 2014, pp. 40–49.'
date_created: 2018-10-31T11:04:43Z
date_updated: 2022-01-06T07:01:43Z
ddc:
- '004'
department:
- _id: '76'
extern: '1'
file:
- access_level: closed
content_type: application/pdf
creator: ups
date_created: 2018-11-02T13:21:13Z
date_updated: 2018-11-02T13:21:13Z
file_id: '5247'
file_name: ralb14droidforce.pdf
file_size: 661565
relation: main_file
file_date_updated: 2018-11-02T13:21:13Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- url: http://www.bodden.de/pubs/ralb14droidforce.pdf
page: 40-49
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
publication: International Conference on Availability, Reliability and Security (ARES
2014)
publisher: IEEE
status: public
title: 'DroidForce: Enforcing Complex, Data-Centric, System-Wide Policies in Android'
type: conference
user_id: '477'
year: '2014'
...