Zobrazeno 1 - 10
of 64
pro vyhledávání: '"Kedar S. Namjoshi"'
Autor:
Kedar S. Namjoshi
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 129, Iss Festschrift for Dave Schmidt, Pp 404-416 (2013)
Fully automated verification of concurrent programs is a difficult problem, primarily because of state explosion: the exponential growth of a program state space with the number of its concurrently active components. It is natural to apply a divide a
Externí odkaz:
https://doaj.org/article/0c4d8ab5956546b7b961b83163939933
Autor:
Kedar S. Namjoshi, Nisarg Patel
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995232
In multi-agent settings, such as IoT and robotics, it is necessary to coordinate the actions of independent agents in order to achieve a joint behavior. While it is often easy to specify the desired joint behavior, programming the necessary coordinat
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b088369c7cf7163de966a4427f1133b6
https://doi.org/10.1007/978-3-030-99524-9_3
https://doi.org/10.1007/978-3-030-99524-9_3
Publikováno v:
Proceedings of the ACM on Programming Languages. 4:1-27
This paper presents a method for synthesizing a reactive program to coordinate the actions of a group of other reactive programs so that the combined system satisfies a temporal specification of its desired long-term behavior. Traditionally, reactive
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::25dc7fac11d6973f433273637910a329
https://doi.org/10.1145/3371122
https://doi.org/10.1145/3371122
Publikováno v:
ICRA
This paper describes Resh, a new, statically typed, interpreted programming language and associated runtime for orchestrating multirobot systems. The main features of Resh are: (1) It offloads much of the tedious work of programming such systems away
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::95335cfc93d80aabcaf151dc7008a267
https://doi.org/10.1109/icra48506.2021.9561133
https://doi.org/10.1109/icra48506.2021.9561133
Autor:
Kedar S. Namjoshi, Anton Xue
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030670665
VMCAI
VMCAI
A self-certifying compiler is designed to generate a correctness proof for each optimization performed during compilation. The generated proofs are checked automatically by an independent proof validator. The outcome is formally verified compilation,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3dc31ac0050f4864f7fb2dd2907e6bee
https://doi.org/10.1007/978-3-030-67067-2_7
https://doi.org/10.1007/978-3-030-67067-2_7
Autor:
Kedar S. Namjoshi, Lucas M. Tabajara
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030393212
VMCAI
VMCAI
Compiler optimizations may break or weaken the security properties of a source program. This work develops a translation validation methodology for secure compilation. A security property is expressed as an automaton operating over a bundle of progra
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d02d04f4ceddf6d1fb937dfccd1df8ce
https://doi.org/10.1007/978-3-030-39322-9_1
https://doi.org/10.1007/978-3-030-39322-9_1
Autor:
Chaoqiang Deng, Kedar S. Namjoshi
Publikováno v:
Formal Methods in System Design. 53:166-188
A compiler optimization may be correct and yet be insecure. This work focuses on the common optimization that removes dead (i.e., useless) store instructions from a program. This operation may introduce new information leaks, weakening security while
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5ba2800689afd1e128288f3db60ab459
https://doi.org/10.1007/s10703-017-0313-8
https://doi.org/10.1007/s10703-017-0313-8
Publikováno v:
Computer Aided Verification ISBN: 9783319961446
CAV (1)
CAV (1)
Asynchronous interactions are ubiquitous in computing systems and complicate design and programming. Automatic construction of asynchronous programs from specifications (“synthesis”) could ease the difficulty, but known methods are complex, and i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a8c12be273e79a4747b9f1935fcb17c6
https://doi.org/10.1007/978-3-319-96145-3_20
https://doi.org/10.1007/978-3-319-96145-3_20
Autor:
Richard J. Trefler, Kedar S. Namjoshi
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783319899626
TACAS (2)
TACAS (2)
Model checking large networks of processes is challenging due to state explosion. In many cases, individual processes are isomorphic, but there is insufficient global symmetry to simplify model checking. This work considers the verification of local
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::44be0c390f522eef7aaa71504870930f
https://doi.org/10.1007/978-3-319-89963-3_22
https://doi.org/10.1007/978-3-319-89963-3_22
Publikováno v:
Handbook of Model Checking ISBN: 9783319105741
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::77edb346a48854d7235ea8e342407715
https://doi.org/10.1007/978-3-319-10575-8_12
https://doi.org/10.1007/978-3-319-10575-8_12