1 citations · 1 across the 8 of their papers we have counts for
9 papers
Consistent Updates for Scalable Microservices
Devora Chait-Roth, Kedar S. Namjoshi, Thomas Wies
Online services are commonly implemented with a scalable microservice architecture, where isomorphic workers process client requests, recording persistent state in a backend data s…
Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework
Yuan Xia, Akanksha Atrey, Fadoua Khmaissia +1
This paper investigates the logical reasoning capabilities of large language models (LLMs). For a precisely defined yet tractable formulation, we choose the conceptually simple but…
Constructing Trustworthy Smart Contracts
Devora Chait-Roth, Kedar S. Namjoshi
Smart contracts form the core of Web3 applications. Contracts mediate the transfer of cryptocurrency, making them irresistible targets for hackers. We introduce ASP, a system aimed…
Atomicity and Abstraction for Cross-Blockchain Interactions
Huaixi Lu, Akshay Jajoo, Kedar S. Namjoshi
A blockchain facilitates secure and atomic transactions between mutually untrusting parties on that chain. Today, there are multiple blockchains with differing interfaces and secur…
The Resh Programming Language for Multirobot Orchestration
Martin Carroll, Kedar S. Namjoshi, Itai Segall
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)…
Witnessing Secure Compilation
Kedar S. Namjoshi, Lucas M. Tabajara
Compiler optimizations are designed to improve run-time performance while preserving input-output behavior. Correctness in this sense does not necessarily preserve security: it is…
Synthesis of coordination programs from linear temporal logic
Suguman Bansal, Kedar S. Namjoshi, Yaniv Sa'ar
This paper presents a method for synthesizing a reactive program which coordinates the actions of a group of other reactive programs, so that the combined system satisfies a tempor…
Symmetry Reduction for the Local Mu-Calculus
Kedar S. Namjoshi, Richard J. Trefler
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 s…
Model Checking in Bits and Pieces
Kedar S. Namjoshi
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…