Zobrazeno 1 - 10
of 12
pro vyhledávání: '"Duc-Hiep Chu"'
Publikováno v:
Proceedings of the ACM on Programming Languages. 4:1-27
Solvers in the framework of Satisfiability Modulo Theories (SMT) have been widely successful in practice. Recently there has been an increasing interest in solvers for string constraints to address security issues in web programming, for example. To
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b80f7c30a5104d1f65bca26f48b8c4d9
https://doi.org/10.1145/3428260
https://doi.org/10.1145/3428260
Publikováno v:
Computer Aided Verification ISBN: 9783319633893
CAV (2)
CAV (2)
We present a new algorithm for model counting of a class of string constraints. In addition to the classic operation of concatenation, our class includes some recursively defined operations such as Kleene closure, and replacement of substrings. Addit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e63b18b6d988feb573b3ad5c3dbca5a3
https://doi.org/10.1007/978-3-319-63390-9_21
https://doi.org/10.1007/978-3-319-63390-9_21
Publikováno v:
ACM Conference on Computer and Communications Security
Cryptocurrencies record transactions in a decentralized data structure called a blockchain. Two of the most popular cryptocurrencies, Bitcoin and Ethereum, support the feature to encode rules or scripts for processing transactions. This feature has e
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f9740dd9252a58f7cd7036a34fbb8db4
https://doi.org/10.1145/2976749.2978309
https://doi.org/10.1145/2976749.2978309
Publikováno v:
LCTES
With the advances in both hardware and software of embedded systems in the past few years, dynamic memory allocation can now be safely used in embedded software. As a result, the need to develop methods to avoid heap overflow errors in safety-critica
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::fcee0fa5c2d439a939759ff95d833873
https://doi.org/10.1145/2907950.2907955
https://doi.org/10.1145/2907950.2907955
Publikováno v:
RTAS
We present a framework for WCET analysis of programs with emphasis on cache micro-architecture. Such an analysis is challenging primarily because of the timing model of a dynamic nature, that is, the timing of a basic block is heavily dependent on th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1c2db5e7a3677112d6e9055173e180eb
https://doi.org/10.1109/rtas.2016.7461358
https://doi.org/10.1109/rtas.2016.7461358
Publikováno v:
Computer Aided Verification ISBN: 9783319415277
CAV (1)
CAV (1)
We consider the problem of reasoning over an expressive constraint language for unbounded strings. The difficulty comes from “recursively defined” functions such as replace, making state-of-the-art algorithms non-terminating. Our first contributi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4cbe28de05c527e0fb7df2bff8b535e5
https://doi.org/10.1007/978-3-319-41528-4_12
https://doi.org/10.1007/978-3-319-41528-4_12
Publikováno v:
PLDI
We consider the problem of automated reasoning about dynamically manipulated data structures. Essential properties are encoded as predicates whose definitions are formalized via user-defined recursive rules. Traditionally, proving relationships betwe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9fa7b8bfd9ef255276b7ad773438af8e
https://doi.org/10.1145/2737924.2737984
https://doi.org/10.1145/2737924.2737984
Publikováno v:
ACM Conference on Computer and Communications Security
Motivated by the vulnerability analysis of web programs which work on string inputs, we present S3, a new symbolic string solver. Our solver employs a new algorithm for a constraint language that is expressive enough for widespread applicability. Spe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::424ac317f523a32e950c15c301a4ff06
https://doi.org/10.1145/2660267.2660372
https://doi.org/10.1145/2660267.2660372
Autor:
Duc-Hiep Chu, Joxan Jaffar
Publikováno v:
Hardware and Software: Verification and Testing ISBN: 9783319133379
Haifa Verification Conference
Haifa Verification Conference
We address the problem of reasoning about interleavings in safety verification of concurrent programs. In the literature, there are two prominent techniques for pruning the search space. First, there are wellinvestigated trace-based methods, collecti
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::29c56e97ef626f7cf33fae8b10098e2e
https://doi.org/10.1007/978-3-319-13338-6_14
https://doi.org/10.1007/978-3-319-13338-6_14
Publikováno v:
Runtime Verification ISBN: 9783319111636
RV
RV
The performance of symbolic execution based verifiers relies heavily on the quality of “interpolants”, formulas which succinctly describe a generalization of states proven safe so far. By default, symbolic execution along a path stops the moment
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6d20973309b4ec0a4923b5120278901c
https://doi.org/10.1007/978-3-319-11164-3_27
https://doi.org/10.1007/978-3-319-11164-3_27