Zobrazeno 1 - 8
of 8
pro vyhledávání: '"Parthasarathy, Gaurav"'
Autor:
Dardinier, Thibault, Sammler, Michael, Parthasarathy, Gaurav, Summers, Alexander J., Müller, Peter
Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3. The resulting IVL program is then verified using an existing back-end
Externí odkaz:
http://arxiv.org/abs/2407.20002
Autor:
Parthasarathy, Gaurav, Dardinier, Thibault, Bonneau, Benjamin, Müller, Peter, Summers, Alexander J.
Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end generates pro
Externí odkaz:
http://arxiv.org/abs/2404.03614
Publikováno v:
Proc. ACM Program. Lang. 7, OOPSLA1, Article 102 (April 2023)
Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (bounded) inlining and about loops via (bounded) unrolling does not req
Externí odkaz:
http://arxiv.org/abs/2208.10456
Autor:
Dardinier, Thibault, Parthasarathy, Gaurav, Weeks, Noé, Summers, Alexanders J., Müller, Peter
The magic wand $\mathbin{-\!\!*}$ (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A footprint of a magic wand formula $A \
Externí odkaz:
http://arxiv.org/abs/2205.11325
A program verifier produces reliable results only if both the logic used to justify the program's correctness is sound, and the implementation of the program verifier is itself correct. Whereas it is common to formally prove soundness of the logic, t
Externí odkaz:
http://arxiv.org/abs/2105.14381
This includes the artifact submitted to the OOPSLA 2023 artifact evaluation committee for the paper "Verification-Preserving Inlining in Automatic Separation Logic Verifiers" We have installed all required dependencies on an Ubuntu 20.04 VirtualBox v
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::200656264bfdeaf1e3372c522a9278fc
This is the artifact submitted to the CAV 2021 artifact evaluation committee for the paper "Formally Validating a Practical Verification Condition Generator". We tested the (Ubuntu 20.04) virtual machine using Virtual Box 6.1. The Login should be aut
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2984c52f24dee556f7c87d3575706e09
Autor:
Jung, Ralf, Lepigre, Rodolphe, Parthasarathy, Gaurav, Rapoport, Marianna, Timany, Amin, Dreyer, Derek, Jacobs, Bart
Early in the development of Hoare logic, Owicki and Gries introduced auxiliary variables as a way of encoding information about the history of a program’s execution that is useful for verifying its correctness. Over a decade later, Abadi and Lampor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2217266e3f74901cae1ac934eac05c91