---
_id: '7626'
author:
- first_name: Philipp
full_name: Schubert, Philipp
id: '60543'
last_name: Schubert
orcid: 0000-0002-8674-1859
- first_name: Ben
full_name: Hermann, Ben
id: '66173'
last_name: Hermann
orcid: 0000-0001-9848-2017
- first_name: Eric
full_name: Bodden, Eric
id: '59256'
last_name: Bodden
orcid: 0000-0003-3470-3647
citation:
ama: 'Schubert P, Hermann B, Bodden E. PhASAR: An Inter-Procedural Static Analysis
Framework for C/C++. In: Proceedings of the 25th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019),
Held as Part of the European Joint Conferences on Theory and Practice of Software
(ETAPS 2019). Vol II. ; 2019:393-410. doi:10.1007/978-3-030-17465-1_22'
apa: 'Schubert, P., Hermann, B., & Bodden, E. (2019). PhASAR: An Inter-Procedural
Static Analysis Framework for C/C++. Proceedings of the 25th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice
of Software (ETAPS 2019), II, 393–410. https://doi.org/10.1007/978-3-030-17465-1_22'
bibtex: '@inproceedings{Schubert_Hermann_Bodden_2019, title={PhASAR: An Inter-Procedural
Static Analysis Framework for C/C++}, volume={II}, DOI={10.1007/978-3-030-17465-1_22},
booktitle={Proceedings of the 25th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the
European Joint Conferences on Theory and Practice of Software (ETAPS 2019)}, author={Schubert,
Philipp and Hermann, Ben and Bodden, Eric}, year={2019}, pages={393–410} }'
chicago: 'Schubert, Philipp, Ben Hermann, and Eric Bodden. “PhASAR: An Inter-Procedural
Static Analysis Framework for C/C++.” In Proceedings of the 25th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice
of Software (ETAPS 2019), II:393–410, 2019. https://doi.org/10.1007/978-3-030-17465-1_22.'
ieee: 'P. Schubert, B. Hermann, and E. Bodden, “PhASAR: An Inter-Procedural Static
Analysis Framework for C/C++,” in Proceedings of the 25th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019),
Held as Part of the European Joint Conferences on Theory and Practice of Software
(ETAPS 2019), Prague, Czech Republic, 2019, vol. II, pp. 393–410, doi: 10.1007/978-3-030-17465-1_22.'
mla: 'Schubert, Philipp, et al. “PhASAR: An Inter-Procedural Static Analysis Framework
for C/C++.” Proceedings of the 25th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the
European Joint Conferences on Theory and Practice of Software (ETAPS 2019),
vol. II, 2019, pp. 393–410, doi:10.1007/978-3-030-17465-1_22.'
short: 'P. Schubert, B. Hermann, E. Bodden, in: Proceedings of the 25th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice
of Software (ETAPS 2019), 2019, pp. 393–410.'
conference:
end_date: 2019-04-11
location: Prague, Czech Republic
name: 25th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS)
start_date: 2019-04-08
date_created: 2019-02-12T07:20:07Z
date_updated: 2022-03-25T07:48:36Z
ddc:
- '000'
department:
- _id: '76'
doi: 10.1007/978-3-030-17465-1_22
file:
- access_level: closed
content_type: application/pdf
creator: pdschbrt
date_created: 2019-02-12T07:18:17Z
date_updated: 2019-02-12T07:18:17Z
file_id: '7627'
file_name: main.pdf
file_size: 504897
relation: main_file
success: 1
file_date_updated: 2019-02-12T07:18:17Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://link.springer.com/chapter/10.1007/978-3-030-17465-1_22
oa: '1'
page: 393-410
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subproject B4
- _id: '3'
name: SFB 901 - Project Area B
publication: Proceedings of the 25th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the European
Joint Conferences on Theory and Practice of Software (ETAPS 2019)
publication_status: published
status: public
title: 'PhASAR: An Inter-Procedural Static Analysis Framework for C/C++'
type: conference
user_id: '60543'
volume: II
year: '2019'
...
---
_id: '10108'
abstract:
- lang: eng
text: "Recent years have seen the development of numerous tools for the analysis
of taint flows in Android apps. Taint analyses aim at detecting data leaks, accidentally
or by purpose programmed into apps. Often, such tools specialize in the treatment
of specific features impeding precise taint analysis (like reflection or inter-app
communication). This multitude of tools, their specific applicability and their
various combination options complicate the selection of a tool (or multiple tools)
when faced with an analysis instance, even for knowledgeable users, and hence
hinders the successful adoption of taint analyses.\r\n\r\nIn this work, we thus
present CoDiDroid, a framework for cooperative Android app analysis. CoDiDroid
(1) allows users to ask questions about flows in apps in varying degrees of detail,
(2) automatically generates subtasks for answering such questions, (3) distributes
tasks onto analysis tools (currently DroidRA, FlowDroid, HornDroid, IC3 and two
novel tools) and (4) at the end merges tool answers on subtasks into an overall
answer. Thereby, users are freed from having to learn about the use and functionality
of all these tools while still being able to leverage their capabilities. Moreover,
we experimentally show that cooperation among tools pays off with respect to effectiveness,
precision and scalability."
author:
- first_name: Felix
full_name: Pauck, Felix
id: '22398'
last_name: Pauck
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Pauck F, Wehrheim H. Together Strong: Cooperative Android App Analysis. In:
Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering
Conference and Symposium on the Foundations of Software Engineering. ; 2019:374-384.
doi:10.1145/3338906.3338915'
apa: 'Pauck, F., & Wehrheim, H. (2019). Together Strong: Cooperative Android
App Analysis. Proceedings of the 2019 27th ACM Joint Meeting on European Software
Engineering Conference and Symposium on the Foundations of Software Engineering,
374–384. https://doi.org/10.1145/3338906.3338915'
bibtex: '@inproceedings{Pauck_Wehrheim_2019, title={Together Strong: Cooperative
Android App Analysis}, DOI={10.1145/3338906.3338915},
booktitle={Proceedings of the 2019 27th ACM Joint Meeting on European Software
Engineering Conference and Symposium on the Foundations of Software Engineering},
author={Pauck, Felix and Wehrheim, Heike}, year={2019}, pages={374–384} }'
chicago: 'Pauck, Felix, and Heike Wehrheim. “Together Strong: Cooperative Android
App Analysis.” In Proceedings of the 2019 27th ACM Joint Meeting on European
Software Engineering Conference and Symposium on the Foundations of Software Engineering,
374–84, 2019. https://doi.org/10.1145/3338906.3338915.'
ieee: 'F. Pauck and H. Wehrheim, “Together Strong: Cooperative Android App Analysis,”
in Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering
Conference and Symposium on the Foundations of Software Engineering, 2019,
pp. 374–384, doi: 10.1145/3338906.3338915.'
mla: 'Pauck, Felix, and Heike Wehrheim. “Together Strong: Cooperative Android App
Analysis.” Proceedings of the 2019 27th ACM Joint Meeting on European Software
Engineering Conference and Symposium on the Foundations of Software Engineering,
2019, pp. 374–84, doi:10.1145/3338906.3338915.'
short: 'F. Pauck, H. Wehrheim, in: Proceedings of the 2019 27th ACM Joint Meeting
on European Software Engineering Conference and Symposium on the Foundations of
Software Engineering, 2019, pp. 374–384.'
date_created: 2019-06-04T11:15:25Z
date_updated: 2023-01-18T08:32:47Z
ddc:
- '004'
department:
- _id: '77'
doi: 10.1145/3338906.3338915
file:
- access_level: closed
content_type: application/pdf
creator: fpauck
date_created: 2019-08-20T08:47:20Z
date_updated: 2019-08-20T08:47:20Z
file_id: '12947'
file_name: fse19main-id44-p-ef9ce42-41855-final.pdf
file_size: 442603
relation: main_file
file_date_updated: 2019-08-20T08:47:20Z
has_accepted_license: '1'
keyword:
- Android Taint Analysis
- Cooperation
- Precision
- Tools
language:
- iso: eng
page: 374-384
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 2019 27th ACM Joint Meeting on European Software Engineering
Conference and Symposium on the Foundations of Software Engineering
publication_identifier:
isbn:
- 978-1-4503-5572-8
publication_status: published
status: public
title: 'Together Strong: Cooperative Android App Analysis'
type: conference
user_id: '22398'
year: '2019'
...
---
_id: '13874'
author:
- first_name: Tobias
full_name: Isenberg, Tobias
last_name: Isenberg
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
- first_name: Felix
full_name: Pauck, Felix
id: '22398'
last_name: Pauck
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Isenberg T, Jakobs M-C, Pauck F, Wehrheim H. When Are Software Verification
Results Valid for Approximate Hardware? In: Tests and Proofs - 13th International
Conference, {TAP} 2019, Held as Part of the Third World Congress on Formal Methods
2019, Porto, Portugal, October 9-11, 2019, Proceedings. ; 2019:3-20. doi:10.1007/978-3-030-31157-5_1'
apa: Isenberg, T., Jakobs, M.-C., Pauck, F., & Wehrheim, H. (2019). When Are
Software Verification Results Valid for Approximate Hardware? Tests and Proofs
- 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress
on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings,
3–20. https://doi.org/10.1007/978-3-030-31157-5_1
bibtex: '@inproceedings{Isenberg_Jakobs_Pauck_Wehrheim_2019, title={When Are Software
Verification Results Valid for Approximate Hardware?}, DOI={10.1007/978-3-030-31157-5_1},
booktitle={Tests and Proofs - 13th International Conference, {TAP} 2019, Held
as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October
9-11, 2019, Proceedings}, author={Isenberg, Tobias and Jakobs, Marie-Christine
and Pauck, Felix and Wehrheim, Heike}, year={2019}, pages={3–20} }'
chicago: Isenberg, Tobias, Marie-Christine Jakobs, Felix Pauck, and Heike Wehrheim.
“When Are Software Verification Results Valid for Approximate Hardware?” In Tests
and Proofs - 13th International Conference, {TAP} 2019, Held as Part of the Third
World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings,
3–20, 2019. https://doi.org/10.1007/978-3-030-31157-5_1.
ieee: 'T. Isenberg, M.-C. Jakobs, F. Pauck, and H. Wehrheim, “When Are Software
Verification Results Valid for Approximate Hardware?,” in Tests and Proofs
- 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress
on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings,
2019, pp. 3–20, doi: 10.1007/978-3-030-31157-5_1.'
mla: Isenberg, Tobias, et al. “When Are Software Verification Results Valid for
Approximate Hardware?” Tests and Proofs - 13th International Conference, {TAP}
2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto,
Portugal, October 9-11, 2019, Proceedings, 2019, pp. 3–20, doi:10.1007/978-3-030-31157-5_1.
short: 'T. Isenberg, M.-C. Jakobs, F. Pauck, H. Wehrheim, in: Tests and Proofs -
13th International Conference, {TAP} 2019, Held as Part of the Third World Congress
on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings, 2019,
pp. 3–20.'
date_created: 2019-10-16T09:40:20Z
date_updated: 2023-01-18T08:41:17Z
department:
- _id: '77'
doi: 10.1007/978-3-030-31157-5_1
language:
- iso: eng
page: 3-20
project:
- _id: '12'
name: SFB 901 - Subproject B4
- _id: '3'
name: SFB 901 - Project Area B
- _id: '1'
name: SFB 901
publication: Tests and Proofs - 13th International Conference, {TAP} 2019, Held as
Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October
9-11, 2019, Proceedings
publication_status: published
status: public
title: When Are Software Verification Results Valid for Approximate Hardware?
type: conference
user_id: '22398'
year: '2019'
...
---
_id: '9913'
abstract:
- lang: eng
text: Reconfigurable hardware has received considerable attention as a platform
that enables dynamic hardware updates and thus is able to adapt new configurations
at runtime. However, due to their dynamic nature, e.g., field-programmable gate
arrays (FPGA) are subject to a constant possibility of attacks, since each new
configuration might be compromised. Trojans for reconfigurable hardware that evade
state-of-the-art detection techniques and even formal verification, are thus a
large threat to these devices. One such stealthy hardware Trojan, that is inserted
and activated in two stages by compromised electronic design automation (EDA)
tools, has recently been presented and shown to evade all forms of classical pre-configuration
detection techniques. This paper presents a successful pre-configuration countermeasure
against this ``Malicious Look-up-table (LUT)''-hardware Trojan, by employing bitstream-level
Proof-Carrying Hardware (PCH). We show that the method is able to alert innocent
module creators to infected EDA tools, and to prohibit malicious ones to sell
infected modules to unsuspecting customers.
author:
- first_name: Qazi Arbab
full_name: Ahmed, Qazi Arbab
id: '72764'
last_name: Ahmed
orcid: 0000-0002-1837-2254
- 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: 'Ahmed QA, Wiersema T, Platzner M. Proof-Carrying Hardware Versus the Stealthy
Malicious LUT Hardware Trojan. In: Hochberger C, Nelson B, Koch A, Woods R, Diniz
P, eds. Applied Reconfigurable Computing. Vol 11444. Lecture Notes in Computer
Science. Springer International Publishing; 2019:127-136. doi:10.1007/978-3-030-17227-5_10'
apa: Ahmed, Q. A., Wiersema, T., & Platzner, M. (2019). Proof-Carrying Hardware
Versus the Stealthy Malicious LUT Hardware Trojan. In C. Hochberger, B. Nelson,
A. Koch, R. Woods, & P. Diniz (Eds.), Applied Reconfigurable Computing
(Vol. 11444, pp. 127–136). Springer International Publishing. https://doi.org/10.1007/978-3-030-17227-5_10
bibtex: '@inproceedings{Ahmed_Wiersema_Platzner_2019, place={Cham}, series={Lecture
Notes in Computer Science}, title={Proof-Carrying Hardware Versus the Stealthy
Malicious LUT Hardware Trojan}, volume={11444}, DOI={10.1007/978-3-030-17227-5_10},
booktitle={Applied Reconfigurable Computing}, publisher={Springer International
Publishing}, author={Ahmed, Qazi Arbab and Wiersema, Tobias and Platzner, Marco},
editor={Hochberger, Christian and Nelson, Brent and Koch, Andreas and Woods, Roger
and Diniz, Pedro}, year={2019}, pages={127–136}, collection={Lecture Notes in
Computer Science} }'
chicago: 'Ahmed, Qazi Arbab, Tobias Wiersema, and Marco Platzner. “Proof-Carrying
Hardware Versus the Stealthy Malicious LUT Hardware Trojan.” In Applied Reconfigurable
Computing, edited by Christian Hochberger, Brent Nelson, Andreas Koch, Roger
Woods, and Pedro Diniz, 11444:127–36. Lecture Notes in Computer Science. Cham:
Springer International Publishing, 2019. https://doi.org/10.1007/978-3-030-17227-5_10.'
ieee: 'Q. A. Ahmed, T. Wiersema, and M. Platzner, “Proof-Carrying Hardware Versus
the Stealthy Malicious LUT Hardware Trojan,” in Applied Reconfigurable Computing,
Darmstadt, Germany, 2019, vol. 11444, pp. 127–136, doi: 10.1007/978-3-030-17227-5_10.'
mla: Ahmed, Qazi Arbab, et al. “Proof-Carrying Hardware Versus the Stealthy Malicious
LUT Hardware Trojan.” Applied Reconfigurable Computing, edited by Christian
Hochberger et al., vol. 11444, Springer International Publishing, 2019, pp. 127–36,
doi:10.1007/978-3-030-17227-5_10.
short: 'Q.A. Ahmed, T. Wiersema, M. Platzner, in: C. Hochberger, B. Nelson, A. Koch,
R. Woods, P. Diniz (Eds.), Applied Reconfigurable Computing, Springer International
Publishing, Cham, 2019, pp. 127–136.'
conference:
end_date: 2019-04-11
location: Darmstadt, Germany
name: 15th International Symposium on Applied Reconfigurable Computing (ARC 2019)
start_date: 2019-04-09
date_created: 2019-05-22T07:36:05Z
date_updated: 2023-05-15T08:13:37Z
ddc:
- '000'
department:
- _id: '78'
doi: 10.1007/978-3-030-17227-5_10
editor:
- first_name: Christian
full_name: Hochberger, Christian
last_name: Hochberger
- first_name: Brent
full_name: Nelson, Brent
last_name: Nelson
- first_name: Andreas
full_name: Koch, Andreas
last_name: Koch
- first_name: Roger
full_name: Woods, Roger
last_name: Woods
- first_name: Pedro
full_name: Diniz, Pedro
last_name: Diniz
file:
- access_level: closed
content_type: application/pdf
creator: qazi
date_created: 2023-05-11T09:12:33Z
date_updated: 2023-05-11T09:12:33Z
file_id: '44749'
file_name: 978-3-030-17227-5_10.pdf
file_size: 661354
relation: main_file
success: 1
file_date_updated: 2023-05-11T09:12:33Z
has_accepted_license: '1'
intvolume: ' 11444'
language:
- iso: eng
main_file_link:
- open_access: '1'
oa: '1'
page: 127-136
place: Cham
project:
- _id: '12'
name: SFB 901 - Subproject B4
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
publication: Applied Reconfigurable Computing
publication_identifier:
isbn:
- 978-3-030-17227-5
publication_status: published
publisher: Springer International Publishing
series_title: Lecture Notes in Computer Science
status: public
title: Proof-Carrying Hardware Versus the Stealthy Malicious LUT Hardware Trojan
type: conference
user_id: '72764'
volume: 11444
year: '2019'
...
---
_id: '14898'
author:
- first_name: Philipp
full_name: Schubert, Philipp
id: '60543'
last_name: Schubert
orcid: 0000-0002-8674-1859
- first_name: Richard
full_name: Leer, Richard
last_name: Leer
- first_name: Ben
full_name: Hermann, Ben
id: '66173'
last_name: Hermann
orcid: 0000-0001-9848-2017
- first_name: Eric
full_name: Bodden, Eric
id: '59256'
last_name: Bodden
orcid: 0000-0003-3470-3647
citation:
ama: 'Schubert P, Leer R, Hermann B, Bodden E. Know your analysis: how instrumentation
aids understanding static analysis. In: Proceedings of the 8th ACM SIGPLAN
International Workshop on State Of the Art in Program Analysis - SOAP 2019.
; 2019. doi:10.1145/3315568.3329965'
apa: 'Schubert, P., Leer, R., Hermann, B., & Bodden, E. (2019). Know your analysis:
how instrumentation aids understanding static analysis. Proceedings of the
8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis
- SOAP 2019. https://doi.org/10.1145/3315568.3329965'
bibtex: '@inproceedings{Schubert_Leer_Hermann_Bodden_2019, title={Know your analysis:
how instrumentation aids understanding static analysis}, DOI={10.1145/3315568.3329965},
booktitle={Proceedings of the 8th ACM SIGPLAN International Workshop on State
Of the Art in Program Analysis - SOAP 2019}, author={Schubert, Philipp and Leer,
Richard and Hermann, Ben and Bodden, Eric}, year={2019} }'
chicago: 'Schubert, Philipp, Richard Leer, Ben Hermann, and Eric Bodden. “Know Your
Analysis: How Instrumentation Aids Understanding Static Analysis.” In Proceedings
of the 8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis
- SOAP 2019, 2019. https://doi.org/10.1145/3315568.3329965.'
ieee: 'P. Schubert, R. Leer, B. Hermann, and E. Bodden, “Know your analysis: how
instrumentation aids understanding static analysis,” 2019, doi: 10.1145/3315568.3329965.'
mla: 'Schubert, Philipp, et al. “Know Your Analysis: How Instrumentation Aids Understanding
Static Analysis.” Proceedings of the 8th ACM SIGPLAN International Workshop
on State Of the Art in Program Analysis - SOAP 2019, 2019, doi:10.1145/3315568.3329965.'
short: 'P. Schubert, R. Leer, B. Hermann, E. Bodden, in: Proceedings of the 8th
ACM SIGPLAN International Workshop on State Of the Art in Program Analysis -
SOAP 2019, 2019.'
date_created: 2019-11-12T12:22:16Z
date_updated: 2023-06-15T08:52:37Z
department:
- _id: '76'
- _id: '34'
- _id: '26'
doi: 10.1145/3315568.3329965
language:
- iso: eng
project:
- _id: '12'
name: 'SFB 901 - B4: SFB 901 - Subproject B4'
- _id: '3'
name: 'SFB 901 - B: SFB 901 - Project Area B'
- _id: '1'
grant_number: '160364472'
name: 'SFB 901: SFB 901: On-The-Fly Computing - Individualisierte IT-Dienstleistungen
in dynamischen Märkten '
publication: Proceedings of the 8th ACM SIGPLAN International Workshop on State Of
the Art in Program Analysis - SOAP 2019
publication_identifier:
isbn:
- '9781450367202'
publication_status: published
status: public
title: 'Know your analysis: how instrumentation aids understanding static analysis'
type: conference
user_id: '15249'
year: '2019'
...
---
_id: '3373'
abstract:
- lang: eng
text: Modern Boolean satisfiability solvers can emit proofs of unsatisfiability.
There is substantial interest in being able to verify such proofs and also in
using them for further computations. In this paper, we present an FPGA accelerator
for checking resolution proofs, a popular proof format. Our accelerator exploits
parallelism at the low level by implementing the basic resolution step in hardware,
and at the high level by instantiating a number of parallel modules for proof
checking. Since proof checking involves highly irregular memory accesses, we employ
Hybrid Memory Cube technology for accelerator memory. The results show that while
the accelerator is scalable and achieves speedups for all benchmark proofs, performance
improvements are currently limited by the overhead of transitioning the proof
into the accelerator memory.
author:
- first_name: Tim
full_name: Hansmeier, Tim
id: '49992'
last_name: Hansmeier
orcid: 0000-0003-1377-3339
- first_name: Marco
full_name: Platzner, Marco
id: '398'
last_name: Platzner
- first_name: David
full_name: Andrews, David
last_name: Andrews
citation:
ama: 'Hansmeier T, Platzner M, Andrews D. An FPGA/HMC-Based Accelerator for Resolution
Proof Checking. In: ARC 2018: Applied Reconfigurable Computing. Architectures,
Tools, and Applications. Vol 10824. Lecture Notes in Computer Science. Springer
International Publishing; 2018:153-165. doi:10.1007/978-3-319-78890-6_13'
apa: 'Hansmeier, T., Platzner, M., & Andrews, D. (2018). An FPGA/HMC-Based Accelerator
for Resolution Proof Checking. In ARC 2018: Applied Reconfigurable Computing.
Architectures, Tools, and Applications (Vol. 10824, pp. 153–165). Santorini,
Greece: Springer International Publishing. https://doi.org/10.1007/978-3-319-78890-6_13'
bibtex: '@inproceedings{Hansmeier_Platzner_Andrews_2018, series={Lecture Notes in
Computer Science}, title={An FPGA/HMC-Based Accelerator for Resolution Proof Checking},
volume={10824}, DOI={10.1007/978-3-319-78890-6_13},
booktitle={ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and
Applications}, publisher={Springer International Publishing}, author={Hansmeier,
Tim and Platzner, Marco and Andrews, David}, year={2018}, pages={153–165}, collection={Lecture
Notes in Computer Science} }'
chicago: 'Hansmeier, Tim, Marco Platzner, and David Andrews. “An FPGA/HMC-Based
Accelerator for Resolution Proof Checking.” In ARC 2018: Applied Reconfigurable
Computing. Architectures, Tools, and Applications, 10824:153–65. Lecture Notes
in Computer Science. Springer International Publishing, 2018. https://doi.org/10.1007/978-3-319-78890-6_13.'
ieee: 'T. Hansmeier, M. Platzner, and D. Andrews, “An FPGA/HMC-Based Accelerator
for Resolution Proof Checking,” in ARC 2018: Applied Reconfigurable Computing.
Architectures, Tools, and Applications, Santorini, Greece, 2018, vol. 10824,
pp. 153–165.'
mla: 'Hansmeier, Tim, et al. “An FPGA/HMC-Based Accelerator for Resolution Proof
Checking.” ARC 2018: Applied Reconfigurable Computing. Architectures, Tools,
and Applications, vol. 10824, Springer International Publishing, 2018, pp.
153–65, doi:10.1007/978-3-319-78890-6_13.'
short: 'T. Hansmeier, M. Platzner, D. Andrews, in: ARC 2018: Applied Reconfigurable
Computing. Architectures, Tools, and Applications, Springer International Publishing,
2018, pp. 153–165.'
conference:
end_date: 2018-05-04
location: Santorini, Greece
name: 'ARC: International Symposium on Applied Reconfigurable Computing'
start_date: 2018-05-02
date_created: 2018-06-27T09:30:24Z
date_updated: 2022-01-06T06:59:13Z
ddc:
- '000'
department:
- _id: '78'
doi: 10.1007/978-3-319-78890-6_13
file:
- access_level: closed
content_type: application/pdf
creator: ups
date_created: 2018-11-02T13:55:07Z
date_updated: 2018-11-02T13:55:07Z
file_id: '5257'
file_name: AnFPGAHMC-BasedAcceleratorForR.pdf
file_size: 612367
relation: main_file
success: 1
file_date_updated: 2018-11-02T13:55:07Z
has_accepted_license: '1'
intvolume: ' 10824'
language:
- iso: eng
page: 153-165
project:
- _id: '12'
name: SFB 901 - Subproject B4
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
publication: 'ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and
Applications'
publication_identifier:
isbn:
- '9783319788890'
- '9783319788906'
issn:
- 0302-9743
- 1611-3349
publication_status: published
publisher: Springer International Publishing
series_title: Lecture Notes in Computer Science
status: public
title: An FPGA/HMC-Based Accelerator for Resolution Proof Checking
type: conference
user_id: '3118'
volume: 10824
year: '2018'
...
---
_id: '3586'
abstract:
- lang: eng
text: Existing approaches and tools for the generation of approximate circuits often
lack generality and are restricted to certain circuit types, approximation techniques,
and quality assurance methods. Moreover, only few tools are publicly available.
This hinders the development and evaluation of new techniques for approximating
circuits and their comparison to previous approaches. In this paper, we first analyze
and classify related approaches and then present CIRCA, our flexible framework
for search-based approximate circuit generation. CIRCA is developed with a focus
on modularity and extensibility. We present the architecture of CIRCA with its
clear separation into stages and functional blocks, report on the current prototype,
and show initial experiments.
author:
- first_name: Linus Matthias
full_name: Witschen, Linus Matthias
id: '49051'
last_name: Witschen
- first_name: Tobias
full_name: Wiersema, Tobias
id: '3118'
last_name: Wiersema
- first_name: Hassan
full_name: Ghasemzadeh Mohammadi, Hassan
id: '61186'
last_name: Ghasemzadeh Mohammadi
- first_name: Muhammad
full_name: Awais, Muhammad
id: '64665'
last_name: Awais
orcid: https://orcid.org/0000-0003-4148-2969
- first_name: Marco
full_name: Platzner, Marco
id: '398'
last_name: Platzner
citation:
ama: 'Witschen LM, Wiersema T, Ghasemzadeh Mohammadi H, Awais M, Platzner M. CIRCA:
Towards a Modular and Extensible Framework for Approximate Circuit Generation.
Third Workshop on Approximate Computing (AxC 2018).'
apa: 'Witschen, L. M., Wiersema, T., Ghasemzadeh Mohammadi, H., Awais, M., &
Platzner, M. (n.d.). CIRCA: Towards a Modular and Extensible Framework for Approximate
Circuit Generation. Third Workshop on Approximate Computing (AxC 2018).'
bibtex: '@article{Witschen_Wiersema_Ghasemzadeh Mohammadi_Awais_Platzner, title={CIRCA:
Towards a Modular and Extensible Framework for Approximate Circuit Generation},
journal={Third Workshop on Approximate Computing (AxC 2018)}, author={Witschen,
Linus Matthias and Wiersema, Tobias and Ghasemzadeh Mohammadi, Hassan and Awais,
Muhammad and Platzner, Marco} }'
chicago: 'Witschen, Linus Matthias, Tobias Wiersema, Hassan Ghasemzadeh Mohammadi,
Muhammad Awais, and Marco Platzner. “CIRCA: Towards a Modular and Extensible Framework
for Approximate Circuit Generation.” Third Workshop on Approximate Computing
(AxC 2018), n.d.'
ieee: 'L. M. Witschen, T. Wiersema, H. Ghasemzadeh Mohammadi, M. Awais, and M. Platzner,
“CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit Generation,”
Third Workshop on Approximate Computing (AxC 2018). .'
mla: 'Witschen, Linus Matthias, et al. “CIRCA: Towards a Modular and Extensible
Framework for Approximate Circuit Generation.” Third Workshop on Approximate
Computing (AxC 2018).'
short: L.M. Witschen, T. Wiersema, H. Ghasemzadeh Mohammadi, M. Awais, M. Platzner,
Third Workshop on Approximate Computing (AxC 2018) (n.d.).
date_created: 2018-07-20T14:10:46Z
date_updated: 2022-01-06T06:59:26Z
ddc:
- '000'
department:
- _id: '78'
file:
- access_level: closed
content_type: application/pdf
creator: tobias82
date_created: 2018-07-20T14:13:31Z
date_updated: 2018-07-20T14:13:31Z
file_id: '3587'
file_name: WitschenWMAP2018.pdf
file_size: 285348
relation: main_file
success: 1
file_date_updated: 2018-07-20T14:13:31Z
has_accepted_license: '1'
keyword:
- Approximate Computing
- Framework
- Pareto Front
- Accuracy
language:
- iso: eng
page: '6'
project:
- _id: '12'
name: SFB 901 - Subproject B4
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '52'
name: Computing Resources Provided by the Paderborn Center for Parallel Computing
publication: Third Workshop on Approximate Computing (AxC 2018)
publication_status: accepted
status: public
title: 'CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit
Generation'
type: preprint
user_id: '49051'
year: '2018'
...
---
_id: '3720'
abstract:
- lang: eng
text: Traditional cache design uses a consolidated block of memory address bits
to index a cache set, equivalent to the use of modulo functions. While this module-based
mapping scheme is widely used in contemporary cache structures due to the simplicity
of its hardware design and its good performance for sequences of consecutive addresses,
its use may not be satisfactory for a variety of application domains having different
characteristics.This thesis presents a new type of cache mapping scheme, motivated
by programmable capabilities combined with Nature-inspired optimization of reconfigurable
hardware. This research has focussed on an FPGA-based evolvable cache structure
of the first level cache in a multi-core processor architecture, able to dynamically
change cache indexing. To solve the challenge of reconfigurable cache mappings,
a programmable Boolean circuit based on a combination of Look-up Table (LUT) memory
elements is proposed. Focusing on optimization aspects at the system level, a
Performance Measurement Infrastructure is introduced that is able to monitor the
underlying microarchitectural metrics, and an adaptive evaluation strategy is
presented that leverages on Evolutionary Algorithms, that is not only capable
of evolving application-specific address-to-cache-index mappings for level one
split caches but also of reducing optimization times. Putting this all together
and prototyping in an FPGA for a LEON3/Linux-based multi-core processor, the creation
of a system architecture reduces cache misses and improves performance over the
use of conventional caches.
- lang: ger
text: Traditionelle Cachedesigns verwenden konsolidierte Blöcke von Speicheradressbits
um einen Cachesatz zu indizieren, vergleichbar mit der Anwendung einer Modulofunktion.
Obwohl dieses modulobasierte Abbildungsschema in heutigen Cachestrukturen weit
verbreitet ist, vor allem wegen seiner einfachen Anforderungen an das Hardwaredesign
und seiner Effizienz für die Indizierung eufeinanderfolgender Speicheradressen,
kann seine Verwendung für eine Vielzahl von Anwendungsdomänen mit unterschiedlichen
Charakteristiken zu suboptimalen Ergebnissen führen. Diese Dissertation präsentiert
einen neuen Typ von Cacheabbildungsschema, motiviert durch die Kombination programmierbarer
Ressourcen mit der naturinspirierten Optimierung rekonfigurierbarer Hardware.
Im Fokus dieser Forschung steht eine FPGA-basierte Cachestruktur für den first
level Cache einer Mehrkernprozessorarchitektur, welche die Cacheindizierung dynamisch
ändern kann. Um die Herausforderung rekonfigurierbarer Cacheabbildungen zu lösen,
wird eine reprogrammierbare Boolesche Schaltung eingeführt, die auf Look-up Table
(LUT) Speicherelementen basiert. Weiterhin wird eine Infrastruktur zur Effizienzmessung
eingeführt, welche die zugrundeliege Mikroarchitektur überwachen kann, sowie eine
adaptive Evaluationsstrategie präsentiert, die evolutionäre Algorithmen wirksam
einsetzt, und die nicht nur anwendungsspezifische Abbildungen von Speicheradressen
zu Cacheindizes für level one Caches evolvieren sondern dabei auch die Optimierungszeiten
reduzieren kann. All diese Aspekte zusammen in einer prototypischen Implementierung
auf einem FPGA für einen LEON3/Linux-basierten Mehrkernprozessor zeigen, dass
evolvierbare Cacheabbildungsfunktionen Cache Misses reduzieren, sowie die Effizienz
im Vergleich zu konventionellen Caches erhöhen können.
author:
- first_name: Nam
full_name: Ho, Nam
last_name: Ho
citation:
ama: 'Ho N. FPGA-Based Reconfigurable Cache Mapping Schemes: Design and Optimization.
Universität Paderborn; 2018. doi:10.17619/UNIPB/1-376'
apa: 'Ho, N. (2018). FPGA-based Reconfigurable Cache Mapping Schemes: Design
and Optimization. Universität Paderborn. https://doi.org/10.17619/UNIPB/1-376'
bibtex: '@book{Ho_2018, title={FPGA-based Reconfigurable Cache Mapping Schemes:
Design and Optimization}, DOI={10.17619/UNIPB/1-376},
publisher={Universität Paderborn}, author={Ho, Nam}, year={2018} }'
chicago: 'Ho, Nam. FPGA-Based Reconfigurable Cache Mapping Schemes: Design and
Optimization. Universität Paderborn, 2018. https://doi.org/10.17619/UNIPB/1-376.'
ieee: 'N. Ho, FPGA-based Reconfigurable Cache Mapping Schemes: Design and Optimization.
Universität Paderborn, 2018.'
mla: 'Ho, Nam. FPGA-Based Reconfigurable Cache Mapping Schemes: Design and Optimization.
Universität Paderborn, 2018, doi:10.17619/UNIPB/1-376.'
short: 'N. Ho, FPGA-Based Reconfigurable Cache Mapping Schemes: Design and Optimization,
Universität Paderborn, 2018.'
date_created: 2018-07-27T06:41:13Z
date_updated: 2022-01-06T06:59:31Z
department:
- _id: '78'
doi: 10.17619/UNIPB/1-376
language:
- iso: eng
page: '139'
project:
- _id: '12'
name: SFB 901 - Subproject B4
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
publication_status: published
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Paul
full_name: Kaufmann, Paul
last_name: Kaufmann
- first_name: Marco
full_name: Platzner, Marco
id: '398'
last_name: Platzner
title: 'FPGA-based Reconfigurable Cache Mapping Schemes: Design and Optimization'
type: dissertation
user_id: '477'
year: '2018'
...
---
_id: '2711'
abstract:
- lang: eng
text: "In recent years, researchers have developed a number of tools to conduct\r\ntaint
analysis of Android applications. While all the respective papers aim at\r\nproviding
a thorough empirical evaluation, comparability is hindered by varying\r\nor unclear
evaluation targets. Sometimes, the apps used for evaluation are not\r\nprecisely
described. In other cases, authors use an established benchmark but\r\ncover it
only partially. In yet other cases, the evaluations differ in terms of\r\nthe
data leaks searched for, or lack a ground truth to compare against. All\r\nthose
limitations make it impossible to truly compare the tools based on those\r\npublished
evaluations.\r\n We thus present ReproDroid, a framework allowing the accurate
comparison of\r\nAndroid taint analysis tools. ReproDroid supports researchers
in inferring the\r\nground truth for data leaks in apps, in automatically applying
tools to\r\nbenchmarks, and in evaluating the obtained results. We use ReproDroid
to\r\ncomparatively evaluate on equal grounds the six prominent taint analysis
tools\r\nAmandroid, DIALDroid, DidFail, DroidSafe, FlowDroid and IccTA. The results
are\r\nlargely positive although four tools violate some promises concerning features\r\nand
accuracy. Finally, we contribute to the area of unbiased benchmarking with\r\na
new and improved version of the open test suite DroidBench."
author:
- first_name: Felix
full_name: Pauck, Felix
id: '22398'
last_name: Pauck
- first_name: Eric
full_name: Bodden, Eric
id: '59256'
last_name: Bodden
orcid: 0000-0003-3470-3647
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: Pauck F, Bodden E, Wehrheim H. Do Android Taint Analysis Tools Keep their Promises?
arXiv:180402903. 2018.
apa: Pauck, F., Bodden, E., & Wehrheim, H. (2018). Do Android Taint Analysis
Tools Keep their Promises? ArXiv:1804.02903.
bibtex: '@article{Pauck_Bodden_Wehrheim_2018, title={Do Android Taint Analysis Tools
Keep their Promises?}, journal={arXiv:1804.02903}, author={Pauck, Felix and Bodden,
Eric and Wehrheim, Heike}, year={2018} }'
chicago: Pauck, Felix, Eric Bodden, and Heike Wehrheim. “Do Android Taint Analysis
Tools Keep Their Promises?” ArXiv:1804.02903, 2018.
ieee: F. Pauck, E. Bodden, and H. Wehrheim, “Do Android Taint Analysis Tools Keep
their Promises?,” arXiv:1804.02903. 2018.
mla: Pauck, Felix, et al. “Do Android Taint Analysis Tools Keep Their Promises?”
ArXiv:1804.02903, 2018.
short: F. Pauck, E. Bodden, H. Wehrheim, ArXiv:1804.02903 (2018).
date_created: 2018-05-09T08:27:11Z
date_updated: 2022-01-06T06:57:35Z
ddc:
- '000'
department:
- _id: '77'
- _id: '76'
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-11-21T10:49:23Z
date_updated: 2018-11-21T10:49:23Z
file_id: '5781'
file_name: Do Android Taint Analysis Tools Keep their Promises.pdf
file_size: 1045861
relation: main_file
success: 1
file_date_updated: 2018-11-21T10:49:23Z
has_accepted_license: '1'
language:
- iso: eng
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
publication: arXiv:1804.02903
status: public
title: Do Android Taint Analysis Tools Keep their Promises?
type: preprint
user_id: '477'
year: '2018'
...
---
_id: '1165'
author:
- first_name: Linus Matthias
full_name: Witschen, Linus Matthias
id: '49051'
last_name: Witschen
- 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: Witschen LM, Wiersema T, Platzner M. Making the Case for Proof-carrying Approximate
Circuits. 4th Workshop On Approximate Computing (WAPCO 2018). 2018.
apa: Witschen, L. M., Wiersema, T., & Platzner, M. (2018). Making the Case for
Proof-carrying Approximate Circuits. 4th Workshop On Approximate Computing
(WAPCO 2018).
bibtex: '@article{Witschen_Wiersema_Platzner_2018, title={Making the Case for Proof-carrying
Approximate Circuits}, journal={4th Workshop On Approximate Computing (WAPCO 2018)},
author={Witschen, Linus Matthias and Wiersema, Tobias and Platzner, Marco}, year={2018}
}'
chicago: Witschen, Linus Matthias, Tobias Wiersema, and Marco Platzner. “Making
the Case for Proof-Carrying Approximate Circuits.” 4th Workshop On Approximate
Computing (WAPCO 2018), 2018.
ieee: L. M. Witschen, T. Wiersema, and M. Platzner, “Making the Case for Proof-carrying
Approximate Circuits,” 4th Workshop On Approximate Computing (WAPCO 2018).
2018.
mla: Witschen, Linus Matthias, et al. “Making the Case for Proof-Carrying Approximate
Circuits.” 4th Workshop On Approximate Computing (WAPCO 2018), 2018.
short: L.M. Witschen, T. Wiersema, M. Platzner, 4th Workshop On Approximate Computing
(WAPCO 2018) (2018).
date_created: 2018-02-01T14:24:54Z
date_updated: 2022-01-06T06:51:06Z
ddc:
- '000'
department:
- _id: '7'
- _id: '34'
- _id: '78'
file:
- access_level: closed
content_type: application/pdf
creator: tobias82
date_created: 2018-11-26T08:00:53Z
date_updated: 2018-11-26T08:00:53Z
file_id: '5821'
file_name: WitschenWP2018[1].pdf
file_size: 287224
relation: main_file
success: 1
file_date_updated: 2018-11-26T08:00:53Z
has_accepted_license: '1'
language:
- iso: eng
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
- _id: '52'
name: Computing Resources Provided by the Paderborn Center for Parallel Computing
publication: 4th Workshop On Approximate Computing (WAPCO 2018)
status: public
title: Making the Case for Proof-carrying Approximate Circuits
type: preprint
user_id: '49051'
year: '2018'
...
---
_id: '5774'
abstract:
- lang: eng
text: Information flow analysis investigates the flow of data in applications, checking
in particular for flows from private sources to public sinks. Flow- and path-sensitive
analyses are, however, often too costly to be performed every time a security-critical
application is run. In this paper, we propose a variant of proof carrying code
for information flow security. To this end, we develop information flow (IF) certificates
which get attached to programs as well as a method for IF certificate validation.
We prove soundness of our technique, i.e., show it to be tamper-free. The technique
is implemented within the program analysis tool CPAchecker. Our experiments confirm
that the use of certificates pays off for costly analysis runs.
author:
- first_name: Manuel
full_name: Töws, Manuel
id: '11315'
last_name: Töws
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Töws M, Wehrheim H. Information Flow Certificates. In: Theoretical Aspects
of Computing – ICTAC 2018. Cham: Springer International Publishing; 2018:435-454.
doi:10.1007/978-3-030-02508-3_23'
apa: 'Töws, M., & Wehrheim, H. (2018). Information Flow Certificates. In Theoretical
Aspects of Computing – ICTAC 2018 (pp. 435–454). Cham: Springer International
Publishing. https://doi.org/10.1007/978-3-030-02508-3_23'
bibtex: '@inproceedings{Töws_Wehrheim_2018, place={Cham}, title={Information Flow
Certificates}, DOI={10.1007/978-3-030-02508-3_23},
booktitle={Theoretical Aspects of Computing – ICTAC 2018}, publisher={Springer
International Publishing}, author={Töws, Manuel and Wehrheim, Heike}, year={2018},
pages={435–454} }'
chicago: 'Töws, Manuel, and Heike Wehrheim. “Information Flow Certificates.” In
Theoretical Aspects of Computing – ICTAC 2018, 435–54. Cham: Springer International
Publishing, 2018. https://doi.org/10.1007/978-3-030-02508-3_23.'
ieee: M. Töws and H. Wehrheim, “Information Flow Certificates,” in Theoretical
Aspects of Computing – ICTAC 2018, 2018, pp. 435–454.
mla: Töws, Manuel, and Heike Wehrheim. “Information Flow Certificates.” Theoretical
Aspects of Computing – ICTAC 2018, Springer International Publishing, 2018,
pp. 435–54, doi:10.1007/978-3-030-02508-3_23.
short: 'M. Töws, H. Wehrheim, in: Theoretical Aspects of Computing – ICTAC 2018,
Springer International Publishing, Cham, 2018, pp. 435–454.'
date_created: 2018-11-21T09:51:37Z
date_updated: 2022-01-06T07:02:40Z
ddc:
- '000'
department:
- _id: '77'
doi: 10.1007/978-3-030-02508-3_23
file:
- access_level: closed
content_type: application/pdf
creator: mtoews
date_created: 2018-11-26T15:11:32Z
date_updated: 2018-11-26T15:11:32Z
file_id: '5837'
file_name: Töws-Wehrheim2018_Chapter_InformationFlowCertificates.pdf
file_size: 518016
relation: main_file
success: 1
file_date_updated: 2018-11-26T15:11:32Z
has_accepted_license: '1'
language:
- iso: eng
page: 435-454
place: Cham
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
publication: Theoretical Aspects of Computing – ICTAC 2018
publication_identifier:
isbn:
- '9783030025076'
- '9783030025083'
issn:
- 0302-9743
- 1611-3349
publication_status: published
publisher: Springer International Publishing
status: public
title: Information Flow Certificates
type: conference
user_id: '477'
year: '2018'
...
---
_id: '4999'
author:
- first_name: Felix
full_name: Pauck, Felix
id: '22398'
last_name: Pauck
- first_name: Eric
full_name: Bodden, Eric
id: '59256'
last_name: Bodden
orcid: 0000-0003-3470-3647
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Pauck F, Bodden E, Wehrheim H. Do Android taint analysis tools keep their
promises? In: Proceedings of the 2018 26th ACM Joint Meeting on European Software
Engineering Conference and Symposium on the Foundations of Software Engineering
- ESEC/FSE 2018. ACM Press; 2018. doi:10.1145/3236024.3236029'
apa: Pauck, F., Bodden, E., & Wehrheim, H. (2018). Do Android taint analysis
tools keep their promises? In Proceedings of the 2018 26th ACM Joint Meeting
on European Software Engineering Conference and Symposium on the Foundations of
Software Engineering - ESEC/FSE 2018. ACM Press. https://doi.org/10.1145/3236024.3236029
bibtex: '@inproceedings{Pauck_Bodden_Wehrheim_2018, title={Do Android taint analysis
tools keep their promises?}, DOI={10.1145/3236024.3236029},
booktitle={Proceedings of the 2018 26th ACM Joint Meeting on European Software
Engineering Conference and Symposium on the Foundations of Software Engineering
- ESEC/FSE 2018}, publisher={ACM Press}, author={Pauck, Felix and Bodden, Eric
and Wehrheim, Heike}, year={2018} }'
chicago: Pauck, Felix, Eric Bodden, and Heike Wehrheim. “Do Android Taint Analysis
Tools Keep Their Promises?” In Proceedings of the 2018 26th ACM Joint Meeting
on European Software Engineering Conference and Symposium on the Foundations of
Software Engineering - ESEC/FSE 2018. ACM Press, 2018. https://doi.org/10.1145/3236024.3236029.
ieee: F. Pauck, E. Bodden, and H. Wehrheim, “Do Android taint analysis tools keep
their promises?,” in Proceedings of the 2018 26th ACM Joint Meeting on European
Software Engineering Conference and Symposium on the Foundations of Software Engineering
- ESEC/FSE 2018, 2018.
mla: Pauck, Felix, et al. “Do Android Taint Analysis Tools Keep Their Promises?”
Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering
Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE
2018, ACM Press, 2018, doi:10.1145/3236024.3236029.
short: 'F. Pauck, E. Bodden, H. Wehrheim, in: Proceedings of the 2018 26th ACM Joint
Meeting on European Software Engineering Conference and Symposium on the Foundations
of Software Engineering - ESEC/FSE 2018, ACM Press, 2018.'
date_created: 2018-10-30T08:03:17Z
date_updated: 2022-01-06T07:01:34Z
ddc:
- '004'
department:
- _id: '77'
- _id: '76'
doi: 10.1145/3236024.3236029
file:
- access_level: closed
content_type: application/pdf
creator: ups
date_created: 2018-11-02T13:37:38Z
date_updated: 2018-11-02T13:37:38Z
file_id: '5251'
file_name: fse18main-id76-p.pdf
file_size: 524169
relation: main_file
success: 1
file_date_updated: 2018-11-02T13:37:38Z
has_accepted_license: '1'
language:
- iso: eng
project:
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
- _id: '1'
name: SFB 901
publication: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering
Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE
2018
publication_identifier:
isbn:
- '9781450355735'
publication_status: published
publisher: ACM Press
status: public
title: Do Android taint analysis tools keep their promises?
type: conference
user_id: '477'
year: '2018'
...
---
_id: '5203'
author:
- first_name: Stefan
full_name: Krüger, Stefan
last_name: Krüger
- first_name: Johannes
full_name: Späth, Johannes
last_name: Späth
- first_name: Karim
full_name: Ali, Karim
last_name: Ali
- first_name: Eric
full_name: Bodden, Eric
id: '59256'
last_name: Bodden
orcid: 0000-0003-3470-3647
- first_name: Mira
full_name: Mezini, Mira
last_name: Mezini
citation:
ama: 'Krüger S, Späth J, Ali K, Bodden E, Mezini M. CrySL: An Extensible Approach
to Validating the Correct Usage of Cryptographic APIs. In: European Conference
on Object-Oriented Programming (ECOOP). ; 2018:10:1-10:27.'
apa: 'Krüger, S., Späth, J., Ali, K., Bodden, E., & Mezini, M. (2018). CrySL:
An Extensible Approach to Validating the Correct Usage of Cryptographic APIs.
In European Conference on Object-Oriented Programming (ECOOP) (pp. 10:1-10:27).'
bibtex: '@inproceedings{Krüger_Späth_Ali_Bodden_Mezini_2018, title={CrySL: An Extensible
Approach to Validating the Correct Usage of Cryptographic APIs}, booktitle={European
Conference on Object-Oriented Programming (ECOOP)}, author={Krüger, Stefan and
Späth, Johannes and Ali, Karim and Bodden, Eric and Mezini, Mira}, year={2018},
pages={10:1-10:27} }'
chicago: 'Krüger, Stefan, Johannes Späth, Karim Ali, Eric Bodden, and Mira Mezini.
“CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic
APIs.” In European Conference on Object-Oriented Programming (ECOOP), 10:1-10:27,
2018.'
ieee: 'S. Krüger, J. Späth, K. Ali, E. Bodden, and M. Mezini, “CrySL: An Extensible
Approach to Validating the Correct Usage of Cryptographic APIs,” in European
Conference on Object-Oriented Programming (ECOOP), 2018, pp. 10:1-10:27.'
mla: 'Krüger, Stefan, et al. “CrySL: An Extensible Approach to Validating the Correct
Usage of Cryptographic APIs.” European Conference on Object-Oriented Programming
(ECOOP), 2018, pp. 10:1-10:27.'
short: 'S. Krüger, J. Späth, K. Ali, E. Bodden, M. Mezini, in: European Conference
on Object-Oriented Programming (ECOOP), 2018, pp. 10:1-10:27.'
date_created: 2018-10-31T12:37:29Z
date_updated: 2022-01-06T07:01:44Z
ddc:
- '000'
department:
- _id: '76'
file:
- access_level: closed
content_type: application/pdf
creator: ups
date_created: 2018-11-02T13:51:05Z
date_updated: 2018-11-02T13:51:05Z
file_id: '5255'
file_name: ksa+18crysl.pdf
file_size: 747259
relation: main_file
success: 1
file_date_updated: 2018-11-02T13:51:05Z
has_accepted_license: '1'
keyword:
- ITSECWEBSITE
- CROSSING
language:
- iso: eng
main_file_link:
- url: http://bodden.de/pubs/ksa+18crysl.pdf
page: 10:1-10:27
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
publication: European Conference on Object-Oriented Programming (ECOOP)
status: public
title: 'CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic
APIs'
type: conference
user_id: '477'
year: '2018'
...
---
_id: '1043'
abstract:
- lang: eng
text: 'Approximate computing (AC) is an emerging paradigm for energy-efficient computation.
The basic idea of AC is to sacrifice high precision for low energy by allowing
hardware to carry out “approximately correct” calculations. This provides a major
challenge for software quality assurance: programs successfully verified to be
correct might be erroneous on approximate hardware. In this letter, we present
a novel approach for determining under what conditions a software verification
result is valid for approximate hardware. To this end, we compute the allowed
tolerances for AC hardware from successful verification runs. More precisely,
we derive a set of constraints which—when met by the AC hardware—guarantees the
verification result to carry over to AC. On the practical side, we furthermore:
1) show how to extract tolerances from verification runs employing predicate abstraction
as verification technology and 2) show how to check such constraints on hardware
designs. We have implemented all techniques, and exemplify them on example C programs
and a number of recently proposed approximate adders.'
author:
- first_name: Tobias
full_name: Isenberg, Tobias
last_name: Isenberg
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
- first_name: Felix
full_name: Pauck, Felix
id: '22398'
last_name: Pauck
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: Isenberg T, Jakobs M-C, Pauck F, Wehrheim H. Validity of Software Verification
Results on Approximate Hardware. IEEE Embedded Systems Letters. 2018:22-25.
doi:10.1109/LES.2017.2758200
apa: Isenberg, T., Jakobs, M.-C., Pauck, F., & Wehrheim, H. (2018). Validity
of Software Verification Results on Approximate Hardware. IEEE Embedded Systems
Letters, 22–25. https://doi.org/10.1109/LES.2017.2758200
bibtex: '@article{Isenberg_Jakobs_Pauck_Wehrheim_2018, title={Validity of Software
Verification Results on Approximate Hardware}, DOI={10.1109/LES.2017.2758200},
journal={IEEE Embedded Systems Letters}, publisher={Institute of Electrical and
Electronics Engineers (IEEE)}, author={Isenberg, Tobias and Jakobs, Marie-Christine
and Pauck, Felix and Wehrheim, Heike}, year={2018}, pages={22–25} }'
chicago: Isenberg, Tobias, Marie-Christine Jakobs, Felix Pauck, and Heike Wehrheim.
“Validity of Software Verification Results on Approximate Hardware.” IEEE Embedded
Systems Letters, 2018, 22–25. https://doi.org/10.1109/LES.2017.2758200.
ieee: T. Isenberg, M.-C. Jakobs, F. Pauck, and H. Wehrheim, “Validity of Software
Verification Results on Approximate Hardware,” IEEE Embedded Systems Letters,
pp. 22–25, 2018.
mla: Isenberg, Tobias, et al. “Validity of Software Verification Results on Approximate
Hardware.” IEEE Embedded Systems Letters, Institute of Electrical and Electronics
Engineers (IEEE), 2018, pp. 22–25, doi:10.1109/LES.2017.2758200.
short: T. Isenberg, M.-C. Jakobs, F. Pauck, H. Wehrheim, IEEE Embedded Systems Letters
(2018) 22–25.
date_created: 2017-12-11T16:11:00Z
date_updated: 2022-01-06T06:50:39Z
ddc:
- '000'
department:
- _id: '77'
doi: 10.1109/LES.2017.2758200
file:
- access_level: closed
content_type: application/pdf
creator: ups
date_created: 2018-11-02T15:27:04Z
date_updated: 2018-11-02T15:27:04Z
file_id: '5303'
file_name: 08053741.pdf
file_size: 523362
relation: main_file
success: 1
file_date_updated: 2018-11-02T15:27:04Z
has_accepted_license: '1'
language:
- iso: eng
page: 22-25
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
publication: IEEE Embedded Systems Letters
publication_identifier:
issn:
- 1943-0663
- 1943-0671
publication_status: published
publisher: Institute of Electrical and Electronics Engineers (IEEE)
status: public
title: Validity of Software Verification Results on Approximate Hardware
type: journal_article
user_id: '477'
year: '2018'
...
---
_id: '1044'
author:
- first_name: Richard
full_name: Leer, Richard
last_name: Leer
citation:
ama: Leer R. Measuring Performance of a Static Analysis Framework with an Application
to Immutability Analysis. Universität Paderborn; 2018.
apa: Leer, R. (2018). Measuring Performance of a Static Analysis Framework with
an application to Immutability Analysis. Universität Paderborn.
bibtex: '@book{Leer_2018, title={Measuring Performance of a Static Analysis Framework
with an application to Immutability Analysis}, publisher={Universität Paderborn},
author={Leer, Richard}, year={2018} }'
chicago: Leer, Richard. Measuring Performance of a Static Analysis Framework
with an Application to Immutability Analysis. Universität Paderborn, 2018.
ieee: R. Leer, Measuring Performance of a Static Analysis Framework with an application
to Immutability Analysis. Universität Paderborn, 2018.
mla: Leer, Richard. Measuring Performance of a Static Analysis Framework with
an Application to Immutability Analysis. Universität Paderborn, 2018.
short: R. Leer, Measuring Performance of a Static Analysis Framework with an Application
to Immutability Analysis, Universität Paderborn, 2018.
date_created: 2017-12-13T07:52:01Z
date_updated: 2022-01-06T06:50:39Z
ddc:
- '000'
department:
- _id: '76'
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-11-21T06:15:51Z
date_updated: 2018-11-21T06:15:51Z
file_id: '5768'
file_name: ba_leer.pdf
file_size: 1383049
relation: main_file
success: 1
file_date_updated: 2018-11-21T06:15:51Z
has_accepted_license: '1'
language:
- iso: eng
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Eric
full_name: Bodden, Eric
id: '59256'
last_name: Bodden
orcid: 0000-0003-3470-3647
title: Measuring Performance of a Static Analysis Framework with an application to
Immutability Analysis
type: bachelorsthesis
user_id: '15504'
year: '2018'
...
---
_id: '1045'
author:
- first_name: Jan Niclas
full_name: Strüwer, Jan Niclas
last_name: Strüwer
citation:
ama: Strüwer JN. Interactive Data Visualization for Exploded Supergraphs.
Universität Paderborn; 2018.
apa: Strüwer, J. N. (2018). Interactive Data Visualization for Exploded Supergraphs.
Universität Paderborn.
bibtex: '@book{Strüwer_2018, title={Interactive Data Visualization for Exploded
Supergraphs}, publisher={Universität Paderborn}, author={Strüwer, Jan Niclas},
year={2018} }'
chicago: Strüwer, Jan Niclas. Interactive Data Visualization for Exploded Supergraphs.
Universität Paderborn, 2018.
ieee: J. N. Strüwer, Interactive Data Visualization for Exploded Supergraphs.
Universität Paderborn, 2018.
mla: Strüwer, Jan Niclas. Interactive Data Visualization for Exploded Supergraphs.
Universität Paderborn, 2018.
short: J.N. Strüwer, Interactive Data Visualization for Exploded Supergraphs, Universität
Paderborn, 2018.
date_created: 2017-12-13T07:53:49Z
date_updated: 2022-01-06T06:50:40Z
ddc:
- '000'
department:
- _id: '76'
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-11-21T06:14:15Z
date_updated: 2018-11-21T06:14:15Z
file_id: '5767'
file_name: ba_struewer.pdf
file_size: 15839765
relation: main_file
success: 1
file_date_updated: 2018-11-21T06:14:15Z
has_accepted_license: '1'
language:
- iso: eng
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Eric
full_name: Bodden, Eric
id: '59256'
last_name: Bodden
orcid: 0000-0003-3470-3647
title: Interactive Data Visualization for Exploded Supergraphs
type: bachelorsthesis
user_id: '15504'
year: '2018'
...
---
_id: '1096'
abstract:
- lang: eng
text: to appear
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Marie-Christine
full_name: Jakobs, Marie-Christine
last_name: Jakobs
- first_name: Thomas
full_name: Lemberger, Thomas
last_name: Lemberger
- first_name: Heike
full_name: Wehrheim, Heike
id: '573'
last_name: Wehrheim
citation:
ama: 'Beyer D, Jakobs M-C, Lemberger T, Wehrheim H. Reducer-Based Construction of
Conditional Verifiers. In: Proceedings of the 40th International Conference
on Software Engineering (ICSE). ACM; 2018:1182--1193.'
apa: 'Beyer, D., Jakobs, M.-C., Lemberger, T., & Wehrheim, H. (2018). Reducer-Based
Construction of Conditional Verifiers. In Proceedings of the 40th International
Conference on Software Engineering (ICSE) (pp. 1182--1193). Gothenburg, Sweden:
ACM.'
bibtex: '@inproceedings{Beyer_Jakobs_Lemberger_Wehrheim_2018, title={Reducer-Based
Construction of Conditional Verifiers}, booktitle={Proceedings of the 40th International
Conference on Software Engineering (ICSE)}, publisher={ACM}, author={Beyer, Dirk
and Jakobs, Marie-Christine and Lemberger, Thomas and Wehrheim, Heike}, year={2018},
pages={1182--1193} }'
chicago: Beyer, Dirk, Marie-Christine Jakobs, Thomas Lemberger, and Heike Wehrheim.
“Reducer-Based Construction of Conditional Verifiers.” In Proceedings of the
40th International Conference on Software Engineering (ICSE), 1182--1193.
ACM, 2018.
ieee: D. Beyer, M.-C. Jakobs, T. Lemberger, and H. Wehrheim, “Reducer-Based Construction
of Conditional Verifiers,” in Proceedings of the 40th International Conference
on Software Engineering (ICSE), Gothenburg, Sweden, 2018, pp. 1182--1193.
mla: Beyer, Dirk, et al. “Reducer-Based Construction of Conditional Verifiers.”
Proceedings of the 40th International Conference on Software Engineering (ICSE),
ACM, 2018, pp. 1182--1193.
short: 'D. Beyer, M.-C. Jakobs, T. Lemberger, H. Wehrheim, in: Proceedings of the
40th International Conference on Software Engineering (ICSE), ACM, 2018, pp. 1182--1193.'
conference:
end_date: 2018-06-03
location: Gothenburg, Sweden
name: 40th International Conference on Software Engineering
start_date: 2018-05-27
date_created: 2018-01-08T10:52:51Z
date_updated: 2022-01-06T06:50:54Z
ddc:
- '000'
department:
- _id: '77'
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-11-21T10:50:51Z
date_updated: 2018-11-21T10:50:51Z
file_id: '5783'
file_name: Reducer-Based Construction of Conditional Verifiers.pdf
file_size: 826719
relation: main_file
success: 1
file_date_updated: 2018-11-21T10:50:51Z
has_accepted_license: '1'
language:
- iso: eng
page: 1182--1193
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
- _id: '85'
name: Kooperative Softwareverifikation
publication: Proceedings of the 40th International Conference on Software Engineering
(ICSE)
publisher: ACM
status: public
title: Reducer-Based Construction of Conditional Verifiers
type: conference
user_id: '29719'
year: '2018'
...
---
_id: '1097'
author:
- first_name: Felix Paul
full_name: Jentzsch, Felix Paul
last_name: Jentzsch
citation:
ama: Jentzsch FP. Enforcing IP Core Connection Properties with Verifiable Security
Monitors. Universität Paderborn; 2018.
apa: Jentzsch, F. P. (2018). Enforcing IP Core Connection Properties with Verifiable
Security Monitors. Universität Paderborn.
bibtex: '@book{Jentzsch_2018, title={Enforcing IP Core Connection Properties with
Verifiable Security Monitors}, publisher={Universität Paderborn}, author={Jentzsch,
Felix Paul}, year={2018} }'
chicago: Jentzsch, Felix Paul. Enforcing IP Core Connection Properties with Verifiable
Security Monitors. Universität Paderborn, 2018.
ieee: F. P. Jentzsch, Enforcing IP Core Connection Properties with Verifiable
Security Monitors. Universität Paderborn, 2018.
mla: Jentzsch, Felix Paul. Enforcing IP Core Connection Properties with Verifiable
Security Monitors. Universität Paderborn, 2018.
short: F.P. Jentzsch, Enforcing IP Core Connection Properties with Verifiable Security
Monitors, Universität Paderborn, 2018.
date_created: 2018-01-15T16:48:05Z
date_updated: 2022-01-06T06:50:54Z
department:
- _id: '78'
keyword:
- Approximate Computing
- Proof-Carrying Hardware
- Formal Verification
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: Enforcing IP Core Connection Properties with Verifiable Security Monitors
type: bachelorsthesis
user_id: '477'
year: '2018'
...
---
_id: '3580'
author:
- first_name: Tim
full_name: Hansmeier, Tim
id: '49992'
last_name: Hansmeier
orcid: 0000-0003-1377-3339
citation:
ama: Hansmeier T. An FPGA Accelerator for Checking Resolution Proofs. Universität
Paderborn; 2017.
apa: Hansmeier, T. (2017). An FPGA Accelerator for Checking Resolution Proofs.
Universität Paderborn.
bibtex: '@book{Hansmeier_2017, title={An FPGA Accelerator for Checking Resolution
Proofs}, publisher={Universität Paderborn}, author={Hansmeier, Tim}, year={2017}
}'
chicago: Hansmeier, Tim. An FPGA Accelerator for Checking Resolution Proofs.
Universität Paderborn, 2017.
ieee: T. Hansmeier, An FPGA Accelerator for Checking Resolution Proofs. Universität
Paderborn, 2017.
mla: Hansmeier, Tim. An FPGA Accelerator for Checking Resolution Proofs.
Universität Paderborn, 2017.
short: T. Hansmeier, An FPGA Accelerator for Checking Resolution Proofs, Universität
Paderborn, 2017.
date_created: 2018-07-20T13:44:34Z
date_updated: 2022-01-06T06:59:25Z
department:
- _id: '78'
- _id: '34'
- _id: '7'
language:
- iso: eng
project:
- _id: '1'
name: SFB 901
- _id: '3'
name: SFB 901 - Project Area B
- _id: '12'
name: SFB 901 - Subproject B4
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Marco
full_name: Platzner, Marco
id: '398'
last_name: Platzner
title: An FPGA Accelerator for Checking Resolution Proofs
type: bachelorsthesis
user_id: '3118'
year: '2017'
...
---
_id: '114'
abstract:
- lang: eng
text: Proof witnesses are proof artifacts showing correctness of programs wrt. safety
properties. The recent past has seen a rising interest in witnesses as (a) proofs
in a proof-carrying-code context, (b) certificates for the correct functioning
of verification tools, or simply (c) exchange formats for (partial) verification
results. As witnesses in all theses scenarios need to be stored and processed,
witnesses are required to be as small as possible. However, software verification
tools – the prime suppliers of witnesses – do not necessarily construct small
witnesses. In this paper, we present a formal account of proof witnesses. We introduce
the concept of weakenings, reducing the complexity of proof witnesses while preserving
the ability of witnessing safety. We develop aweakening technique for a specific
class of program analyses, and prove it to be sound. Finally, we experimentally
demonstrate our weakening technique to indeed achieve a size reduction of proof
witnesses.
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. Compact Proof Witnesses. In: Barrett C, Davies M,
Kahsai T, eds. NASA Formal Methods: 9th International Symposium. Lecture
Notes in Computer Science. ; 2017:389-403. doi:10.1007/978-3-319-57288-8_28'
apa: 'Jakobs, M.-C., & Wehrheim, H. (2017). Compact Proof Witnesses. In C. Barrett,
M. Davies, & T. Kahsai (Eds.), NASA Formal Methods: 9th International Symposium
(pp. 389–403). https://doi.org/10.1007/978-3-319-57288-8_28'
bibtex: '@inproceedings{Jakobs_Wehrheim_2017, series={Lecture Notes in Computer
Science}, title={Compact Proof Witnesses}, DOI={10.1007/978-3-319-57288-8_28},
booktitle={NASA Formal Methods: 9th International Symposium}, author={Jakobs,
Marie-Christine and Wehrheim, Heike}, editor={Barrett, Clark and Davies, Misty
and Kahsai, TemesghenEditors}, year={2017}, pages={389–403}, collection={Lecture
Notes in Computer Science} }'
chicago: 'Jakobs, Marie-Christine, and Heike Wehrheim. “Compact Proof Witnesses.”
In NASA Formal Methods: 9th International Symposium, edited by Clark Barrett,
Misty Davies, and Temesghen Kahsai, 389–403. Lecture Notes in Computer Science,
2017. https://doi.org/10.1007/978-3-319-57288-8_28.'
ieee: 'M.-C. Jakobs and H. Wehrheim, “Compact Proof Witnesses,” in NASA Formal
Methods: 9th International Symposium, 2017, pp. 389–403.'
mla: 'Jakobs, Marie-Christine, and Heike Wehrheim. “Compact Proof Witnesses.” NASA
Formal Methods: 9th International Symposium, edited by Clark Barrett et al.,
2017, pp. 389–403, doi:10.1007/978-3-319-57288-8_28.'
short: 'M.-C. Jakobs, H. Wehrheim, in: C. Barrett, M. Davies, T. Kahsai (Eds.),
NASA Formal Methods: 9th International Symposium, 2017, pp. 389–403.'
date_created: 2017-10-17T12:41:13Z
date_updated: 2022-01-06T06:51:00Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-319-57288-8_28
editor:
- first_name: Clark
full_name: Barrett, Clark
last_name: Barrett
- first_name: Misty
full_name: Davies, Misty
last_name: Davies
- first_name: Temesghen
full_name: Kahsai, Temesghen
last_name: Kahsai
file:
- access_level: closed
content_type: application/pdf
creator: florida
date_created: 2018-03-21T13:05:02Z
date_updated: 2018-03-21T13:05:02Z
file_id: '1565'
file_name: 114-chp_3A10.1007_2F978-3-319-57288-8_28.pdf
file_size: 492800
relation: main_file
success: 1
file_date_updated: 2018-03-21T13:05:02Z
has_accepted_license: '1'
language:
- iso: eng
page: 389-403
project:
- _id: '1'
name: SFB 901
- _id: '12'
name: SFB 901 - Subprojekt B4
- _id: '3'
name: SFB 901 - Project Area B
publication: 'NASA Formal Methods: 9th International Symposium'
series_title: Lecture Notes in Computer Science
status: public
title: Compact Proof Witnesses
type: conference
user_id: '477'
year: '2017'
...