Zobrazeno 1 - 8
of 8
pro vyhledávání: '"Alex Sanchez-Stern"'
Publikováno v:
Proceedings of the ACM on Programming Languages. 6:505-531
Interactive proofs of theorems often require auxiliary helper lemmas to prove the desired theorem. Existing approaches for automatically synthesizing helper lemmas fall into two broad categories. Some approaches are goal-directed, producing lemmas sp
Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification by learning from proof corpor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8a9b2017cc485608cde6861161290846
Publikováno v:
PLDI
Web applications often handle large amounts of sensitive user data. Modern secure web frameworks protect this data by (1) using declarative languages to specify security policies alongside database schemas and (2) automatically enforcing these polici
Publikováno v:
CPP
Proof engineering tools make it easier to develop and maintain large systems verified using interactive theorem provers. Developing useful proof engineering tools hinges on understanding the development processes of proof engineers. This paper breaks
Publikováno v:
MAPL@PLDI
Foundational verification allows programmers to build software which has been empirically shown to have high levels of assurance in a variety of important domains. However, the cost of producing foundationally verified software remains prohibitively
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::064be63fef0b2c64626786dd90f6f2b9
http://arxiv.org/abs/1907.07794
http://arxiv.org/abs/1907.07794
Publikováno v:
PLDI
Floating-point arithmetic plays a central role in science, engineering, and finance by enabling developers to approximate real arithmetic. To address numerical issues in large floating-point applications, developers must identify root causes, which i
Autor:
Zachary Tatlock, Alex Sanchez-Stern, Chen Qiu, Pavel Panchekha, Nasrine Damouche, Matthieu Martel
Publikováno v:
Numerical Software Verification ISBN: 9783319542911
NSV@CAV
NSV@CAV
We introduce FPBench, a standard benchmark format for validation and optimization of numerical accuracy in floating-point computations. FPBench is a first step toward addressing an increasing need in our community for comparisons and combinations of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4b6941ab8b565780c8b2af404d590a03
https://oatao.univ-toulouse.fr/29009/
https://oatao.univ-toulouse.fr/29009/
Publikováno v:
PLDI
Scientific and engineering applications depend on floating point arithmetic to approximate real arithmetic. This approximation introduces rounding error, which can accumulate to produce unacceptable results. While the numerical methods literature pro