Zobrazeno 1 - 8
of 8
pro vyhledávání: '"Karlheinz Friedberger"'
Autor:
Dirk Beyer, Karlheinz Friedberger
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 233, Iss Proc. MEMICS 2016, Pp 61-71 (2016)
Verifying multi-threaded programs is becoming more and more important, because of the strong trend to increase the number of processing units per CPU socket. We introduce a new configurable program analysis for verifying multi-threaded programs with
Externí odkaz:
https://doaj.org/article/c772c074af6d4c36927a9c0bc7d9cd84
Publikováno v:
Computer Aided Verification ISBN: 9783030816872
CAV (2)
CAV (2)
Satisfiability Modulo Theories (SMT) is an enabling technology with many applications, especially in computer-aided verification. Due to advances in research and strong demand for solvers, there are many SMT solvers available. Since different impleme
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b02e585fa863b2bf296bc39334a6ae7f
https://doi.org/10.1007/978-3-030-81688-9_9
https://doi.org/10.1007/978-3-030-81688-9_9
Autor:
Karlheinz Friedberger, Dirk Beyer
Publikováno v:
ESEC/SIGSOFT FSE
Whenever a new software-verification technique is developed, additional effort is necessary to extend the new program analysis to an interprocedural one, such that it supports recursive procedures. We would like to reduce that additional effort. Our
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c1c1abfc5e21df491489105b5e577417
https://doi.org/10.1145/3368089.3409718
https://doi.org/10.1145/3368089.3409718
Autor:
Karlheinz Friedberger, Dirk Beyer
Publikováno v:
ASE
Recent development of software aims at massively parallel execution, because of the trend to increase the number of processing units per CPU socket. But many approaches for program analysis are not designed to benefit from a multi-threaded execution
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::01bbd95e153d221e163282d8af594071
https://doi.org/10.1145/3238147.3238195
https://doi.org/10.1145/3238147.3238195
Autor:
Karlheinz Friedberger, Dirk Beyer
Publikováno v:
Leveraging Applications of Formal Methods, Verification and Validation. Verification ISBN: 9783030034207
ISoLA (2)
ISoLA (2)
Block summarization is an efficient technique in software verification to decompose a verification problem into separate tasks and to avoid repeated exploration of reusable parts of a program. In order to benefit from abstraction at the same time, bl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::04763738da063497c6bdb1c88b7cfdf0
https://doi.org/10.1007/978-3-030-03421-4_14
https://doi.org/10.1007/978-3-030-03421-4_14
CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783662545799
TACAS (2)
TACAS (2)
Our submission to SV-COMP'17 is based on the software verification framework CPAchecker. Combined with value analysis and predicate analysis we use the concept of block-abstraction memoization with optimization and several fixes relative to the versi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e8c725e7ca36368624f38637ba9019ef
https://doi.org/10.1007/978-3-662-54580-5_22
https://doi.org/10.1007/978-3-662-54580-5_22
Autor:
Karlheinz Friedberger
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783662496732
TACAS
TACAS
The software verification framework CPAchecker is built on basic approaches like CPA and CEGAR. The configuration for the SV-COMP'16 uses the concept of block-abstraction memoization and combines it with the parallel execution of value analysis and p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c2edb30240d7533da63afa37b0e506b6
https://doi.org/10.1007/978-3-662-49674-9_58
https://doi.org/10.1007/978-3-662-49674-9_58
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319488684
VSTTE
VSTTE
Satisfiability Modulo Theory (SMT) solvers received a lot of attention in the research community in the last decade, and consequently their expressiveness and performance have significantly improved. In the areas of program analysis and model checkin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8ac9ce4cdab4d85517075e17bf45df16
https://doi.org/10.1007/978-3-319-48869-1_11
https://doi.org/10.1007/978-3-319-48869-1_11