Publications:

  • Predictable Verification using Intrinsic Definitions
    Adithya Murali, Cody Rivera, P. Madhusudan
    PLDI 2024, Copenhagen, Denmark.
    ACM Europe Best Paper Award

  • CONJUNCT: Learning Inductive Invariants to Prove Unbounded Instruction Safety Against Microarchitectural Timing Attacks
    Sushant Dinesh, P. Madhusudan, Christopher W. Fletcher
    IEEE Symposium on Security and Privacy, San Francisco, USA, 2024.

  • Perception Contracts for Safety of ML-enabled Systems
    Angello Astorga, Chiao Hsieh, P. Madhusudan, Sayan Mitra
    OOPSLA 2023, Cascais, Portugal, October 2023, Proc. of the ACM on Programming Languages (PACMPL).
    Also 100th Conference paper!

  • Complete First-Order Reasoning for Properties of Functional Programs
    Adithya Murali, Lucas Pena, Ranjit Jhala, P. Madhusudan
    OOPSLA 2023, Cascais, Portugal, October 2023, Proc. of the ACM on Programming Languages (PACMPL).
    Full Version

  • Languages With Decidable Learning: A Meta-Theorem
    Paul Krogmeier, P. Madhusudan
    OOPSLA 2023, Cascais, Portugal, October 2023, Proc. of the ACM on Programming Languages (PACMPL).
    Distinguished Paper Award

  • Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
    Adithya Murali, Lucas Pena, Eion Blanchard, Christof Loding, P. Madhusudan
    OOPSLA, 2022, Auckland, New Zealand. Proceedings of the ACM on Programming Languages (PACMPL).

  • Synthesizing Axiomatizations using Reasoning and Logic Learning
    Zhengyao Lin, Paul Krogmeier, Adithya Murali, P. Madhusudan
    OOPSLA, 2022, Auckland, New Zealand. Proceedings of the ACM on Programming Languages (PACMPL).

  • Composing Neural Learning and Symbolic Reasoning with an Application to Visual Discrimination
    Adithya Murali, Atharva Sehgal, Paul Krogmeier, P. Madhusudan
    31st Int'l Joint Conference on Artificial Intelligence (IJCAI), Vienna, Austria, 2022.

  • Learning Formulas in Finite Variable Logics
    Paul Krogmeier, P. Madhusudan
    Proc. ACM Program. Lang. 6, : 1-28, Conf. on Principles of Programming Languages (POPL), Philadelphia, USA, 2022.
    Distinguished Paper Award
    Talk by Paul Krogmeier (click on Media on page)

  • Synthesizing contracts correct modulo a test generator
    Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan, Tao Xie
    Proc. ACM Program. Lang. 5, ACM SIGPLAN Conf. on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH; OOPSLA): 1-27 (2021)

  • A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines
    Daniel Neider, P. Madhusudan, Shambwaditya Saha, Pranav Garg, Daejun Park
    Journal of Automated Reasoning, Volume 64(7): 1523-1552 (2020)

  • Decidable Synthesis of Programs with Uninterpreted Functions
    Paul Krogmeier, Umang Mathur, Adithya Murali, P. Madhusudan, Mahesh Viswanathan
    32nd Int'l Conf. on Computer Aided Verification (CAV), Los Angeles, USA, 2020, LNCS 12225, Springer.

  • A First Order Logic with Frames
    Christof Loding, P. Madhusudan, Adithya Murali, Lucas Pena
    ESOP 2020.

  • What's Decidable About Program Verification Modulo Axioms?
    Umang Mathur, P. Madhusudan, Mahesh Viswanathan
    26th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2020

  • Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
    Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, Mahesh Viswanathan
    Principles of Programming Languages (POPL), 2020.

    •

    2019 and earlier

  • Reachability in Concurrent Uninterpreted Programs
    Salvatore La Torre, P. Madhusudan
    39th Int'l Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019).

  • Kaizen: Building a Verified and Performant Blockchain System,
    Faria Kalim, Karl Palmskog, Jayasi Mehar, Adithya Murali, Indranil Gupta, P. Madhusudan.
    Proc. Formal Methods in Computer-Aided Design (FMCAD), 2019.

  • Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants
    Daniel Neider, Shambwaditya Saha, Pranav Garg, and P. Madhusudan
    Proc. of 26th Static Analysis Symposium (SAS), 2019.

  • Learning Stateful Preconditions Modulo a Test Generator
    Angello Astorga, P. Madhusudan, Shambwaditya Saha, Shiyu Wang, Tao Xie
    Proc. of Programming Languages Design and Implementation (PLDI), 2019.

  • Decidable Verification of Uninterpreted Programs
    Umang Mathur, P. Madhusudan, Mahesh Viswanathan
    Proceedings of Principles of Programming Languages (POPL), 2019.
    Published in Proc. ACM Program. Lang., Vol. 3, POPL, Article 46, January 2019.
    Talk at POPL by Umang Mathur

    • 2018

  • Horn-ICE Learning for Synthesizing Invariants and Contracts
    D. D'Souza, P. Ezudheen, P. Garg, P. Madhusudan and D. Neider
    Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA 2018.

  • Lagrange's theorem for binary squares,
    P. Madhusudan, Dirk Nowotka, Aayush Rajasekaran, and Jeffrey Shallit,
    43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018),
    Best paper award

  • A Decidable Fragment of Second Order Logic With Applications to Synthesis
    P. Madhusudan, Umang Mathur, Shambwaditya Saha, Mahesh Viswanathan
    7th EACSL Annual Conference on Computer Science Logic, CSL 2018.

  • Invariant Synthesis for Incomplete Verification Engines
    Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha, Daejun Park.
    International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2018.

  • Foundations for Natural Proofs and Quantifier Elimination
    Christof Loding, P. Madhusudan, Lucas Pena.
    45th ACM SIGPLAN Symp. on Principles of Programming Languages (POPL '18) 2018.

    • 2017

  • Efficient Incrementalized Runtime Checking of Linear Measures on Lists
    Alex Gyori, Pranav Garg, Edgar Pek, P. Madhusudan
    10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017).

  • Compositional Synthesis of Piece-Wise Functions by Learning Classifiers
    P. Madhusudan, Daniel Neider, Shambwaditya Saha
    Accepted to appear in ACM Transactions on Computational Logic

    • 2016

  • Abstract Learning Frameworks for Synthesis
    Christof Loding, P. Madhusudan, Daniel Neider.
    22nd Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016, ETAPS 2016, Eindhoven, The Netherlands.

  • Synthesizing Piece-wise Functions by Learning Classifiers
    P. Madhusudan, Daniel Neider, Shambwaditya Saha
    22nd Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016, ETAPS 2016, Eindhoven, The Netherlands.

  • Learning Invariants using Decision Trees and Implication Counterexamples
    Pranav Garg, Daniel Neider, P. Madhusudan, and Dan Roth

    Annual Symposium on Principles of Programming Languages (POPL), St. Petersburg, Florida, USA, 2016.

    • 2015

  • Quantified Data Automata for Linear Data Structures. A Register Automaton Model with Applications to Learning Invariants of Programs Manipulating Arrays and Lists
    Formal Methods in System Design (FMSD) 47(1) 2015. Invited article as a special issue for the Computer Aided Verification conference.
    Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider

  • Alchemist: Learning Guarded Affine Functions
    Shambwaditya Saha, Pranav Garg, and P. Madhusudan
    27th Int'l Conf. on Computer Aided Verification, 2015, San Fransisco, USA (CAV 2015)

  • NETGEN: Synthesizing Data-plane configurations for Network Policies
    Shambwaditya Saha, M. Prabhu, P. Madhusudan
    1st ACM SIGCOMM Symp. on Software Defined Networking Research (SOSR'15), Santa Clara, USA.
    Paper (PDF)

    • 2014

  • Natural Proofs for Asynchronous Programs using Almost-Synchronous Reductions
    Ankush Desai, Pranav Garg, P. Madhusudan
    ACM SIGPLAN Int'l Conf. on Object Oriented Prog. Sys. Languages & Applications (OOPSLA 2014), part of SPLASH 2014, USA.
    Paper PDF

  • ICE: A Robust Learning Framework for Synthesizing Invariants
    Pranav Garg, Christof Loeding, P. Madhusudan, and Daniel Neider
    26th Int'l Conf. on Computer Aided Verification, 2014, Vienna, Austria (CAV 2014)
    Paper PDF

  • VAC - Verifier of Administrative Role-based Access Control Policies
    Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen and Gennaro Parlato.
    26th Int'l Conf. on Computer Aided Verification, 2014, Vienna, Austria (CAV 2014)
    Paper PDF

  • Natural Proofs for Data Structure Manipulation in C using Separation Logic
    Edgar Pek, Xiaokang Qiu, P. Madhusudan
    35th ACM SIGPLAN Programming Language Design and Implementation (PLDI 2014)
    Paper PDF

  • Online Learning versus Blended Learning: An Exploratory Study
    Cross, Ashok, Bala, Cutrell, Datha, Kumar, Kumar, Madhusudan, Prakash, Rajamani, Sangameswaran, Sharma, Thies.
    Work in Progress paper, First ACM Conference on Learning at Scale
    Paper PDF

    •

    2013

  • Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists
    Pranav Garg, P. Madhusudan, and Gennaro Parlato
    20th Static Analysis Symposium (SAS), 2013.
    Paper PDF

  • Learning Universally Quantified Invariants of Linear Data Structures
    Pranav Garg, Christof Loeding, P. Madhusudan, and Daniel Neider
    25th Int'l Conf. on Computer Aided Verification (CAV), 2013.
    Paper PDF

  • Natural Proofs for Structure, Data, and Separation
    Xiaokang Qiu, Pranav Garg, and Andrei Stefanescu, P. Madhusudan
    ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), 2013.
    Paper PDF and Supplementary material

  • Verifying Security Invariants in ExpressOS
    Haohui Mai, Edgar Pek, Hui Xue, Samuel T. King, and P. Madhusudan
    18th Int'l Conf. on Architectural Support for Prog. Lang. and Operating Sys. (ASPLOS), 2013
    PDF

  • Policy Analysis for Self-administrated role-based access control
    Anna Lisa Ferrara, P. Madhusudan, and Gennaro Parlato
    19th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2013
    PDF

    • 2012

  • Predicting Null-Pointer Dereferences in Concurrent Programs
    with Azadeh Farzan , Niloofar Razavi, and Francesco Sorrentino
    20th ACM SIGSOFT Int'l Symp on Foundations of Software Engineering (FSE), 2012.
    PDF

  • Security Analysis of Role-based Access Control through Program Verification
    with Gennaro Parlato and Anna Lisa Ferrara
    25th IEEE Computer Security Foundations Symposium (CSF).
    Harvard University, Cambridge MA, USA, 2012.
    PDF
    See the associated VAC Tool page.

  • Analyzing Temporal Role Based Access Control Models
    with Emre Uzun, Vijay Atluri, Shamik Sural, Jaideep Vaidya, Gennaro Parlato, and Anna Lisa Ferrara
    17th ACM Symposium on Access Control Models and Technologies (SACMAT)
    Newark, USA, 2012.

  • Reachability under Contextual Locking
    with Mahesh Viswanathan and Rohit Chadha
    Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012, Tallinn, Estonia.
    PDF

  • Recursive Proofs for Inductive Tree Data-structures
    with Xiaokang Qiu and Andrei Stefanescu
    Principles of Programming Languages (POPL), 2012, Philadelphia.
    PDF

    • 2011

  • Vetting browser extensions for security vulnerabilities with VEX
    with Sruthi Bandhakavi, Nandit Tiku, Wyatt Pittman, Sam King, and Marianne Winslett
    Research Highlights
    Communications of the ACM (CACM), Vol. 54, Issue 9, September 2011.

  • Synthesizing Reactive Programs
    20th Conference on Computer Science Logic (CSL), Bergen, Norway, 2011.
    PDF

  • Efficient algorithms for deciding properties of heaps using STRAND
    with Xiaokang Qiu
    Static Analysis Symposium (SAS) 2011, Venice, Italy.
    PDF

  • Compositionality entails Sequentializability
    with Pranav Garg
    Int'l Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2011.
    PDF

  • Thread Contracts for Safe Parallelism
    with Rajesh Karmani and Brandon Moore
    16th ACM SIGPLAN Annual Symp. on Principles and Practice of Parallel Programming (PPoPP 2011).
    PDF

  • Decidable Logics Combining Heap Structures and Data
    with Gennaro Parlato and Xiaokang Qiu
    ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages (POPL), 2011
    PDF

  • The Tree Width of Auxiliary Storage
    with Gennaro Parlato
    ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages (POPL), 2011
    PDF
    See also Technical Report. that has more proofs.

    • 2010

  • PENELOPE: Weaving Threads to Expose Atomicity Violations
    with Azadeh Farzan and Francesco Sorrentino
    ACM SIGSOFT Int'l Symp. on the Foundations of Software Engineering (FSE), Santa Fe, New Mexico, USA, November 2010.
    PDF

  • VEX: Vetting Browser Extensions For Security Vulnerabilities
    with Sruthi Bandhakavi, Sam King, and Marianne Winslett
    Proc. of USENIX Security Symposium. Washington D.C, USA, August 2010.
    *** Best paper award ***
    See the VEX Website for details on the tool.
    PDF

  • Model-checking Parameterized Concurrent Programs using Linear Interfaces
    with Salvatore La Torre and Gennaro Parlato
    To appear in 22nd Int'l Conf. on Computer Aided Verification (CAV), 2010, Edinburgh, UK.
    PDF

  • The language theory of bounded context-switching
    with Salvatore La Torre and Gennaro Parlato
    9th Latin American Theoretical Informatics Symposium (LATIN), Oaxaca, Mexico, 2010.
    PDF.

    • 2009

  • Query automata for nested words
    with Mahesh Viswanathan
    34th International Symposium on Mathematical Foundations of Computer Science (MFCS), High Tatras, Slovakia, 2009.
    PDF.

  • Meta-analysis for Atomicity Violations under Nested Locking
    with Azadeh Farzan and Francesco Sorrentino
    Computer Aided Verification (CAV), Grenoble, France, 2009.
    PDF.

  • Reducing Context-bounded Concurrent Reachability to Sequential Reachability
    with Salvatore La Torre and Gennaro Parlato
    Computer Aided Verification (CAV), Grenoble, France, 2009.
    PDF.

  • Analyzing Recursive Programs using a Fixed-point Calculus
    with Salvatore La Torre and Gennaro Parlato
    ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI)
    Dublin, Ireland, 2009.
    PDF.
    See also the Getafix page for the tool and experiments

  • The Complexity of Predicting Atomicity Violations
    with Azadeh Farzan
    Int'l Conf. on Tools and Algorithms for the Construction & Analysis of Systems (TACAS)
    York, UK, 2009.
    PDF.
    Slides: Powerpoint, PDF

  • Adding nesting structure to words.
    with R. Alur
    Journal of the ACM (JACM), Vol. 56(3), pages 1-43, ACM, 2009.
    PDF.

  • CANDID: Dynamic Candidate Evaluations for Automatic Prevention of SQL Injection Attacks
    with Prithvi Bisht and V.N. Venkatakrishnan.
    ACM Transactions on Information and System Security (TISSEC), 2009.
    PDF.

    • 2008

  • Parallel Computing at Illinois: The UPCRC Agenda
    with S. Adve, V. Adve, G. Agha, M.I. Frank, M.J. Garzaran, J.H.Hart, W.W. Hwu, R.E. Johnson, L.V. Kale, R. Kumar, D. Marinov, K. Nahrstedt, D. Padua, S. Patel, G. Rosu, D. Roth, M.Snir, J. Torrellas, C. Zilles
    Whitepaper PDF.

  • A Formal Framework for Reflective Database Access Control Policies
    with Lars Olson and Carl Gunter.
    15th ACM Conference on Computer and Communications Security (CCS)
    Alexandria, USA, 2008.
    PDF.

  • An Infinite Automaton Characterization of Double Exponential Time
    with Gennaro Parlato and Salvatore La Torre.
    17th EACSL Annual Conference on Computer Science Logic
    Bertinoro, Italy, 2008.
    Conference version, More complete version with an appendix

  • Monitoring Atomicity in Concurrent Programs
    with Azadeh Farzan
    Computer Aided Verification (CAV), Princeton, USA, 2008.
    PDF.

  • Context-Bounded Analysis of Concurrent Queue Systems
    with Gennaro Parlato and Salvatore La Torre.
    Tools and Algorithms for the Construction and Analysis of Systems
    (TACAS), Budapest, Hungary, 2008.
    PDF.

    • 2007

  • CANDID: Preventing SQL Injection Attacks using Dynamic Candidate Evaluations
    with Sruthi Bandhakavi, Prithvi Bisht and V.N. Venkatakrishnan.
    14th ACM Conference on Computer and Communications Security (CCS)
    Alexandria, USA, 2007.
    PDF.

  • A Robust Class of Context-Sensitive Languages
    with Gennaro Parlato and Salvatore La Torre.
    22nd IEEE Symp. on Logic in Computer Science (LICS)
    Wroclaw, Poland, 2007.
    PDF.

  • Visibly Pushdown Automata for Streaming XML
    with Viraj Kumar and Mahesh Viswanathan.
    Int'l World Wide Web Conference (WWW)
    Alberta, Canada, 2007.
    PDF.

  • Causal Dataflow Analysis for Concurrent Programs
    with Azadeh Farzan.
    Tools and Algorithms for the Construction and Analysis of Systems
    (TACAS), Braga, Portugal, 2007.
    PDF.

    • 2006

  • Minimization, Learning, and Conformance Testing of Boolean Programs
    with Viraj Kumar and Mahesh Viswanathan.
    Int'l Conf on Concurrency Theory (CONCUR), Bonn, Germany, 2006.
    PDF.

  • Causal Atomicity
    with Azadeh Farzan.
    Computer Aided Verification (CAV), Seattle, USA, 2006.
    PDF.

  • Languages of nested trees
    with Rajeev Alur and Swarat Chaudhuri.
    Computer Aided Verification (CAV), Seattle, USA, 2006.
    PDF.

  • Adding Nesting Structure to Words
    with Rajeev Alur.
    Developments in Language Theory (DLT), Santa Barbara, USA, 2006.
    PDF.

  • Modular Strategies for Recursive Game Graphs
    with Rajeev Alur and Salvatore La Torre.
    Theoretical Computer Science, Special Issue for TACAS 2003
    Volume 354, Issue 2, 28 March 2006, Pages 230-249.
    PDF; Link to journal article

  • A Fixpoint Calculus for Local and Global Program Flows
    with Rajeev Alur and Swarat Chaudhuri.
    Principles of Programming Languages (POPL), Charleston, USA, 2006.
    Postscript, PDF.

    • 2005

  • The MSO Theory of Connectedly Communicating Processes
    with Yang Shaofa and P.S. Thiagarajan.
    Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2005
    Postscript, PDF.

  • Congruences for visibly pushdown languages
    with Rajeev Alur, Viraj Kumar and Mahesh Viswanathan.
    Int'l Coll. on Automata, Lang. and Prog. (ICALP), Lisboa, Portugal, 2005.
    Postscript, PDF.

  • Symbolic Compositional Verification by Learning Assumptions
    with Rajeev Alur and Wonhong Nam.
    Computer Aided Verification (CAV), Edinburgh, UK, 2005.
    Postscript, PDF.

  • Symbolic Computational Techniques for Solving Games
    with Rajeev Alur and Wonhong Nam.
    Journal version of BMC'03 paper,
    International Journal on Software Tools for Technology Transfer (STTT)
    February, 2005, © Springer-Verlag
    Postscript of prelim version, Paper on Springer's site

  • On-the-fly reachability and cycle detection for recursive state machines
    with Rajeev Alur, Swarat Chaudhuri, and Kousha Etessami.
    TACAS '05, April 4-8, Edinburgh, UK.
    Postscript

  • Perturbed timed automata
    with Rajeev Alur and Salvatore La Torre.
    Hybrid Systems: Computation and Control (HSCC),
    Zurich, Switzerland, 2005.
    Postscript, PDF

  • Synthesis of Interface Specifications for Java Classes
    (Version 2, July 2004: See the JIST page)
    with Rajeev Alur, Pavol Cerny and Wonhong Nam.
    32nd ACM SIGPLAN-SIGACT Symp. on Principles of Prog. Languages,
    POPL'05, Long Beach, California, USA, Jan 2005.
    Postscript, PDF

    • 2004

  • Visibly pushdown games
    with Christof Loeding and Olivier Serre.
    Foundations of Software Tech. and Theoretical Comp. Sc. (FSTTCS),
    Chennai, India, 2004.
    Postscript

  • Decision problems for timed automata: A Survey
    with Rajeev Alur
    4th Int'l School Formal Methods for the design of
    computer, communication and software systems: Real Time (SFM-04:RT),
    Bertinoro, Italy, 2004. LNCS © Springer-Verlag
    Postscript

  • Optimal Reachability for Weighted Timed Games
    with Rajeev Alur and Mikhail Bernadsky.
    ICALP, 31st Int'l Colloquium on Automata, Languages and Programming,
    Turku, Finland, 2004. LNCS © Springer-Verlag
    Abstract, PDF

  • Visibly pushdown languages
    with Rajeev Alur.
    STOC, Symp. on Theory of Computing, Chicago, USA, 2004.
    Abstract, PDF

  • A Temporal Logic for Nested Calls and Returns
    with Rajeev Alur and K. Etessami.
    TACAS, Barcelona, Spain, 2004. LNCS © Springer-Verlag
    Abstract, Postscript

    • 2003

  • Playing Games with Boxes and Diamonds
    with Rajeev Alur and Salvatore La Torre.
    CONCUR, Marseilles, France, 2003, LNCS © Springer-Verlag
    Abstract, Postscript

  • Symbolic Computational Techniques for Solving Games
    with Rajeev Alur and Wonhong Nam.
    Bounded Model Checking Workshop, Boulder, Colorado, USA, 2003,
    Electronic Notes in Theoretical Computer Science, Vol 89, Issue 4.
    Abstract, Postscript, PDF

  • Modular Strategies for Infinite Games on Recursive Graphs
    with Rajeev Alur and Salvatore La Torre.
    CAV, Boulder, Colorado, USA, 2003, LNCS © Springer-Verlag
    Abstract, Postscript

  • Timed Control with Partial Observability
    with Deepak D'Souza, Patricia Bouyer and Antoine Petit.
    CAV, Boulder, Colorado, USA, 2003, LNCS © Springer-Verlag
    Abstract, Postscript

  • Model-checking Trace Event Structures
    LICS, Ottawa, Canada, 2003, © IEEE
    Abstract, Postscript

  • Modular Strategies for Recursive Game Graphs
    with Rajeev Alur and Salvatore La Torre.
    9th TACAS, Warsaw, Poland, 2003, LNCS © Springer-Verlag
    Abstract, Postscript

    • 2002

  • Dynamic Message Sequence Charts
    with Martin Leucker and Supratik Mukhopadhyay.
    22nd FSTTCS, Kanpur, India, 2002, LNCS © Springer-Verlag
    Abstract, Postscript

  • A Decidable Class of Asynchronous Distributed Controllers
    with P.S. Thiagarajan.
    CONCUR, Brno, Czech Republic, 2002, LNCS 2421 © Springer-Verlag
    Abstract, Postscript

  • Timed Control Synthesis for External Specifications
    with Deepak D'Souza, CMI.
    STACS, Antibes - Juan les Pins, France, 2002,
    LNCS 2285 © Springer-Verlag
    Abstract, Postscript

  • Branching-time controllers for discrete event systems
    with P.S. Thiagarajan, CMI.
    CONCUR '98 Special Issue, Theoretical Computer Science,
    274 1-2 (2002) © Elsevier Sceince
    Abstract, Postscript, PDF (actual journal version)

    • 2001

  • Control and Synthesis of Open Reactive Systems
    Ph.D. thesis, November 2001
    Abstract, Postscript, PDF

  • Beyond Message Sequence Graphs
    with B. Meenakshi.
    21st FSTTCS, Bangalore, India, 2001, LNCS 2245 © Springer-Verlag
    Abstract, Postscript

  • Reasoning about Sequential and Branching Behaviours of Message Sequence Graphs
    28th ICALP, Crete, Greece, 2001, LNCS 2076 © Springer-Verlag
    Abstract, Postscript

  • Distributed Controller Synthesis for Local Specifications
    with P.S. Thiagarajan.
    28th ICALP, Crete, Greece, 2001, LNCS 2076 © Springer-Verlag
    Abstract, Postscript

    • Before 2000

  • Open systems in reactive environments: Control and Synthesis
    with Orna Kupferman, P.S. Thiagarajan, Moshe Vardi.
    11th CONCUR, Penn. State Univ., USA, 2000, LNCS 1877 © Springer-Verlag
    Abstract, Postscript

  • Controllers for discrete event systems via morphisms
    with P.S. Thiagarajan, CMI.
    9th CONCUR, Nice, France, 1998, LNCS 1466 © Springer-Verlag
    Abstract, Postscript

  • On-the-fly verification of Product-LTL
    with Deepak D'Souza, CMI.
    National Seminar on Theoretical Computer Science, Madras, June '97.
    Abstract, Postscript

  • An on-the-fly algorithm for linear-time temporal logic
    M.Sc. thesis, 1994
    Abstract, Postscript