Zobrazeno 1 - 10
of 21
pro vyhledávání: '"Quoc-Sang Phan"'
Publikováno v:
Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::100e717a1b688420f1fee5d0db781dfa
https://doi.org/10.1145/3510457.3513064
https://doi.org/10.1145/3510457.3513064
Autor:
Timo Kehrer, Ji Wang, Minxing Tang, Pavel Parizek, Elena Sherman, Eric Mercer, Peter Aldous, Zhenbang Chen, Ismet Burak Kadron, Koushik Sen, Tevfik Bultan, Yannic Noller, Hoang Lam Nguyen, Cyrille Artho, Benjamin M. Ogles, Kyle Storey, Joshua Hooker, Lucas Bang, Egor Namakonov, Alyas Almaawi, Hengbiao Yu, Lars Grunske, Corina S. Păsăreanu, Seemanta Saha, S. Jacob Powell, Willem Visser, William Eiers, Sarfraz Khurshid, David Lo, Quoc-Sang Phan, Xuan-Bach D. Le, Wei Dong, Rohan Padhye, Simon Goldsmith, Hayes Converse, Lasse Berglund, Sasa Misailovic, Milos Gligoric
Publikováno v:
ACM SIGSOFT Software Engineering Notes. 45:20-22
Java Path nder (JPF) was originally developed as an explicit- state software model checker, and subsequently evolved into an extensible Java bytecode analysis framework that has been suc- cessfully used to implement techniques such as symbolic and co
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::cb6f34a542708d7be6ee77ad40a548a1
https://doi.org/10.1145/3385678.3385685
https://doi.org/10.1145/3385678.3385685
Publikováno v:
Proceedings of the 3rd ACM SIGSOFT International Workshop on Software Security from Design to Deployment.
Being able to detect program runtime complexity can help identify security vulnerabilities such as DoS attacks and side-channel information leakage. In prior work, we use dynamic invariant generation to infer nonlinear numerical relations to represen
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b55fc8259d81199b3ac6f274005c7b98
https://doi.org/10.1145/3416507.3423189
https://doi.org/10.1145/3416507.3423189
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030309411
FM
FM
Concolic testing is a test generation technique which works effectively by integrating random testing generation and symbolic execution. Existing concolic testing engines focus on numeric programs. Heap-manipulating programs make extensive use of com
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::31e85cd14a72980a25ab8fe21ef27193
https://doi.org/10.1007/978-3-030-30942-8_27
https://doi.org/10.1007/978-3-030-30942-8_27
Publikováno v:
Automated Technology for Verification and Analysis ISBN: 9783030317836
ATVA
ATVA
Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numerical domains, existing symbolic execution techniques for heap-based programs are limited due to the lack of a succinct
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b58df24a763f2ca1e7f27be6705033f8
https://doi.org/10.1007/978-3-030-31784-3_12
https://doi.org/10.1007/978-3-030-31784-3_12
Symbolic execution is a systematic program analysis technique which executes programs on symbolic inputs, representing multiple concrete inputs, and represents the program behavior using mathematical constraints over the symbolic inputs. Solving the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d956d135928a55451be01e9e14cca065
https://doi.org/10.1016/bs.adcom.2018.10.004
https://doi.org/10.1016/bs.adcom.2018.10.004
Publikováno v:
CSF
In this paper we describe symbolic side-channel analysis techniques for detecting and quantifying information leakage, given in terms of Shannon and min-entropy. Measuring the precise leakage is challenging due to the randomness and noise often prese
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::bd066e61eb8d8536aa8a79afd8cc1459
https://doi.org/10.1109/csf.2018.00030
https://doi.org/10.1109/csf.2018.00030
Publikováno v:
ICSE (Companion Volume)
We present Java StarFinder (JSF), a tool for automated test case generation and error detection for Java programs having inputs in the form of complex heap-manipulating data structures. The core of JSF is a symbolic execution engine that uses separat
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e86f34b92b433859cc7232010276e346
https://doi.org/10.1145/3183440.3194964
https://doi.org/10.1145/3183440.3194964
Publikováno v:
ACM SIGSOFT Software Engineering Notes. 40:1-5
We introduce a methodology, based on symbolic execution, for Concurrent Bounded Model Checking. In our approach, we translate a program into a formula in a disjunctive form. This design enables concurrent verification, with a main thread running symb
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3e820c830f4f8f050748e4268627777c
https://doi.org/10.1145/2693208.2693240
https://doi.org/10.1145/2693208.2693240
Publikováno v:
CSF
We present symbolic analysis techniques for detecting vulnerabilities that are due to adaptive side-channel attacks, and synthesizing inputs that exploit the identified vulnerabilities. We start with a symbolic attack model that encodes succinctly al
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7c4c738eb6b9c7ff1680f1eaa13450ad
https://doi.org/10.1109/csf.2017.8
https://doi.org/10.1109/csf.2017.8