Výsledky vyhledávání - "Namjoshi, K.S."

Efficient approximate verification of Promela models via symmetry markers

Autor: Bosnacki, D., Donaldson, A.F., Leuschel, M., Massart, T., Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y.

Publikováno v: Automated Technology for Verification and Analysis ISBN: 9783540755951
ATVA
Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007) 22-25 October 2007, Tokyo, Japan, 300-315
STARTPAGE=300;ENDPAGE=315;TITLE=Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007) 22-25 October 2007, Tokyo, Japan

We present a new verification technique for Promela which exploits state-space symmetries induced by scalarset values used in a model. The technique involves efficiently computing a marker for each state encountered during search. We propose a comple

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ebc24d27f7db0d290ea9b6579da0c93c
https://doi.org/10.1007/978-3-540-75596-8_22

Zobrazit plný text záznamu

Assertion-based proof checking of Chang-Roberts leader election in PVS

Autor: Wesselink, J.W., Romijn, J.M.T., Mooij, A.J., Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y.

Publikováno v: Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007) 22-25 October 2007, Tokyo, Japan, 347-361
STARTPAGE=347;ENDPAGE=361;TITLE=Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007) 22-25 October 2007, Tokyo, Japan
Automated Technology for Verification and Analysis ISBN: 9783540755951
ATVA

We report a case study in automated incremental assertion-based proof checking with PVS. Given an annotated distributed algorithm, our tool ProPar generates the proof obligations for partial correctness, plus a proof script per obligation. ProPar the

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::61f93e0813247a8c2e4f56a3d3f41bf2
https://research.tue.nl/nl/publications/b10cfef0-a464-491b-9350-f99a2a56788f

Zobrazit plný text záznamu

Pruning state spaces with extended beam search

Autor: Torabi Dashti, M., Wijs, A.J., Namjoshi, K.S.

Publikováno v: Proceedings of the 5th International Symposium of Automated Technology for Verification and Analysis, 543-552
STARTPAGE=543;ENDPAGE=552;TITLE=Proceedings of the 5th International Symposium of Automated Technology for Verification and Analysis
Automated Technology for Verification and Analysis ISBN: 9783540755951
ATVA

This paper focuses on using beam search, a heuristic search algorithm, for pruning state spaces while generating. The original beam search is adapted to the state space generation setting and two new search variants are devised. The resulting framewo

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c18f29b3b87abb6b2c5800bd357f5724
https://research.tue.nl/nl/publications/2309bfb7-42d4-4db4-83b8-cf394dc20e7b

Zobrazit plný text záznamu