Zobrazeno 1 - 9
of 9
pro vyhledávání: '"Talia Ringer"'
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
Early in the pandemic, we -- leaders in the research areas of programming languages (PL) and computer architecture (CA) -- realized that we had a problem: the only way to form new lasting connections in the community was to already have lasting conne
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8f6744ddf10ae7852c7e216143985a97
Publikováno v:
Foundations and Trends® in Programming Languages. 5:102-281
Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underlying assumptions. Tools supporting such development have been availabl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::45e060a3c9761524bf2ce0a9d87fa41e
https://doi.org/10.1561/2500000045
https://doi.org/10.1561/2500000045
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
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::defc5c33e7b7831a3e9d6e41268eccef
https://doi.org/10.1145/3372885.3373823
https://doi.org/10.1145/3372885.3373823
Publikováno v:
PLDI
We describe a new approach to automatically repairing broken proofs in the Coq proof assistant in response to changes in types. Our approach combines a configurable proof term transformation with a decompiler from proof terms to tactic scripts. The p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ef0c24ac27a65c4d0a7ea811deac93e5
Publikováno v:
Proceedings of the ACM on Programming Languages. 1:1-24
Developing a small but useful set of inputs for tests is challenging. We show that a domain-specific language backed by a constraint solver can help the programmer with this process. The solver can generate a set of test inputs and guarantee that eac
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::004c2e4da98443c7f1339a896d8a68b4
https://doi.org/10.1145/3133915
https://doi.org/10.1145/3133915
Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underlying assumptions. Tools supporting such development have been availabl
Publikováno v:
CPP
We extend proof automation in an interactive theorem prover to analyze changes in specifications and proofs. Our approach leverages the history of changes to specifications and proofs to search for a patch that can be applied to other specifications
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0111b9523853953b4ea065c5c568595e
https://doi.org/10.1145/3176245.3167094
https://doi.org/10.1145/3176245.3167094
Publikováno v:
ACM Conference on Computer and Communications Security
User-driven access control improves the coarse-grained access control of current operating systems (particularly in the mobile space) that provide only all-or-nothing access to a resource such as the camera or the current location. By granting approp
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d40efdbee8b1603fae8682d7cd3c1385
https://doi.org/10.1145/2976749.2978344
https://doi.org/10.1145/2976749.2978344