Zobrazeno 1 - 7
of 7
pro vyhledávání: '"Minh-Thai Trinh"'
Publikováno v:
Proceedings of the ACM on Programming Languages. 7:56-84
Previous work on rewriting and reachability logic establishes a vision for a language-agnostic program verifier, which takes three inputs: a program, its formal specification, and the formal semantics of the programming language in which the program
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c6bf8e396bf2212bd7aaa2d881cd563c
https://doi.org/10.1145/3586029
https://doi.org/10.1145/3586029
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:
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
Publikováno v:
Computer Aided Verification ISBN: 9783642221095
CAV
CAV
interpretation techniques have played a major role in advancing the state-of-the-art in program analysis. Traditionally, stand-alone tools for these techniques have been developed for the numerical domains which may be sufficient for lower levels of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::31023d1b1c141643a84553c75b226312
https://doi.org/10.1007/978-3-642-22110-1_53
https://doi.org/10.1007/978-3-642-22110-1_53