Zobrazeno 1 - 10
of 215
pro vyhledávání: '"Emina Torlak"'
Publikováno v:
Proceedings of the ACM on Programming Languages. 6:1-28
Reusable symbolic evaluators are a key building block of solver-aided verification and synthesis tools. A reusable evaluator reduces the semantics of all paths in a program to logical constraints, and a client tool uses these constraints to formulate
Publikováno v:
Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis.
Publikováno v:
ACM SIGOPS Operating Systems Review. 54:31-39
This paper presents an analysis of noninterference specifications used in a range of formally verified systems. The main findings are that these systems use distinct specifications and that they often employ small variations, both complicating their
Publikováno v:
ASE
This paper presents Solar, a system for automatic synthesis of adversarial contracts that exploit vulnerabilities in a victim smart contract. To make the synthesis tractable, we introduce a query language as well as summary-based symbolic evaluation,
Publikováno v:
Computer Aided Verification ISBN: 9783030532901
CAV (2)
CAV (2)
Modern operating systems allow user-space applications to submit code for kernel execution through the use of in-kernel domain specific languages (DSLs). Applications use these DSLs to customize system policies and add new functionality. For performa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::42feba66e508294d8963604549984641
https://doi.org/10.1007/978-3-030-53291-8_29
https://doi.org/10.1007/978-3-030-53291-8_29
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030393212
VMCAI
VMCAI
Effective symbolic evaluation is key to building scalable verification and synthesis tools based on SMT solving. These tools use symbolic evaluators to reduce the semantics of all paths through a finite program to logical constraints, discharged with
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a31cc4b6fca3b63fb852d7c2b0f71e0f
https://doi.org/10.1007/978-3-030-39322-9_3
https://doi.org/10.1007/978-3-030-39322-9_3
Autor:
James Bornholt, Emina Torlak
Publikováno v:
Proceedings of the ACM on Programming Languages. 2:1-26
Solver-aided tools rely on symbolic evaluation to reduce programming tasks, such as verification and synthesis, to satisfiability queries. Many reusable symbolic evaluation engines are now available as part of solver-aided languages and frameworks, w
Publikováno v:
Proceedings of the ACM on Programming Languages. 2:1-29
We present lambda_sym, a typed λ-calculus for lenient symbolic execution , where some language constructs do not recognize symbolic values. Its type system, however, ensures safe behavior of all symbolic values in a program. Our calculus extends a b
Autor:
Steven Lyubomirsky, Michael D. Ernst, Emina Torlak, Stefan Heule, Konstantin Weitz, Zachary Tatlock
Publikováno v:
Proceedings of the ACM on Programming Languages. 1:1-28
Many verification tools build on automated solvers. These tools reduce problems in a specific application domain (e.g., compiler optimization validation) to queries that can be discharged with a highly optimized solver. But the correctness of the red
Autor:
James Bornholt, Emina Torlak
Publikováno v:
PLDI
A memory consistency model specifies which writes to shared memory a given read may see. Ambiguities or errors in these specifications can lead to bugs in both compilers and applications. Yet architectures usually define their memory models with pros