| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Thu, 14 Aug 2025 13:12:00 GMT
access-control-allow-origin: *
strict-transport-security: max-age=31556952
etag: W/"689de0a0-163e"
expires: Mon, 29 Dec 2025 11:22:34 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: EB25:318CF6:8A6712:9B83A2:69526222
accept-ranges: bytes
age: 0
date: Mon, 29 Dec 2025 11:12:34 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210023-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767006754.494146,VS0,VE209
vary: Accept-Encoding
x-fastly-request-id: 657b75aeb28667ddddc97439724d36fa55b31a87
content-length: 2539
Kedar Namjoshi
Producing good software is challenging. My research develops methods to simplify program construction while providing precise guarantees of correctness and security. Much of my research is driven by a fascinating interplay between the deductive and algorithmic approaches to program verification. Deductive methods formalize intuitive patterns of reasoning. Those patterns can be automated and used to guide correct program construction. Conversely, algorithmic methods such as model checking can be modified to generate deductive proofs that justify their results.
|
I work in computer science at Bell Labs.
My research is on simplifying the construction of provably correct and secure programs.
Address: Room 2B-435, 600-700 Mountain Avenue, Murray Hill, NJ 07974, USA
My research is on simplifying the construction of provably correct and secure programs.
Contact
E-mail: kedar.namjoshi AT nokia-bell-labs.comAddress: Room 2B-435, 600-700 Mountain Avenue, Murray Hill, NJ 07974, USA
Producing good software is challenging. My research develops methods to simplify program construction while providing precise guarantees of correctness and security. Much of my research is driven by a fascinating interplay between the deductive and algorithmic approaches to program verification. Deductive methods formalize intuitive patterns of reasoning. Those patterns can be automated and used to guide correct program construction. Conversely, algorithmic methods such as model checking can be modified to generate deductive proofs that justify their results.
Research Highlights
- Parameterized Protocol Verification: Cutoff theorems make it possible to show that a protocol is correct for all configurations by checking only a few small instances.
- Program Equivalence: Well-founded bisimulations simplify proofs of equivalence between programs, which is useful for establishing the correctness of pipelined machines and optimizing compilers.
- Abstraction: Linkages between deductive proofs, model checking, and abstraction lead to fast, incremental program analysis.
- Modular Reasoning: Divide-and-conquer methods tackle state explosion in the analysis of large concurrent programs, while new symmetry principles further speed up modular analysis.
- Self-Certification: Run-time certificates formally guarantee the correctness of complex software -- model checkers, optimizing compilers, and network OS's.
- Synthesis: Automatically generated programs coordinate groups of software agents, guiding them towards a desired joint behavior.