Publications

Journal and Conference Articles

• Conflict-Tolerant Specifications for Hybrid Systems,
  (with Madhu Gopinathan, S. Ramesh, and Prahladavaradan Sampath),
  (manuscript).

• Dataflow analysis for data-race free programs,
  (with Arnab De and Rupesh Nasre),
  to appear in ESOP 2011.

• A Case Study in Matching Service Descriptions to Implementations in an Existing System,
  (with Hari S. Gupta, Raghavan Komondoor, and Girish M. Rama),
  in ICSM 2010.

• Analysing Message Sequence Graph Specifications
  (with Joy Chakraborty and K. Narayan Kumar)
  in proc. ISoLA 2010, LNCS 6415. Technical Report.

• WOMM: A Weak Operational Memory Model,
  (with Arnab De and Abhik Roychoudhury),
  in proc. ISoLA 2010, LNCS 6415, pages 519-534.

• Equivalence of the Pointwise and Continuous Semantics of First Order Logic with Linear Constraints
  (with Raveendra Holla)
  (manuscript).

• Conflict-Tolerant Real-Time Specifications in Metric Temporal Logic
  (with Sumesh Divakaran and Raj Mohan M.),
  in proc TIME 2010.

• Conflict-Tolerant Specifications in Temporal Logic
  (with Sumesh Divakaran and Raj Mohan M.), in proc. India Software Engineering Conference (ISEC) 2010.
  Technical Report

• Deepak D'Souza, Madhu Gopinathan, S. Ramesh, and Prahladavaradan Sampath: Supervisory control for real-time systems based on conflict-tolerant controllers, in Proc. 5th IEEE Conf. on Automation Science and Engineering (CASE), pages 555--560, 2009.

• On the Decidability of Model-Checking Information Flow Properties
  (with Raveendra Holla, Janardhan Kulkarni, Raghavendra K. Ramesh, Barbara Sprick)
  in ICISS 2008, Hyderabad, pages 26-40.

• Conflict-Tolerant Real-Time Features
  (with Madhu Gopinathan, S. Ramesh, and Prahladavaradan Sampath)
  in 5th Int. Conference on the Quantitative Evaluation of Systems (QEST 2008), 14-17 September 2008, Saint-Malo, France, pages 274-283.

• Eliminating past operators in Metric Temporal Logic
  (with Raj Mohan M and Pavithra Prabhakar)
  in Perspectives in Concurrency, Universities Press, 2008, pages 86--106.

• Java Memory Model aware Software Validation
  (with Arnab De and Abhik Roychoudhury)
  in PASTE'08 Workshop.

• Automata and logics for finitely varying functions
  (with Fabrice Chevalier, Raj Mohan M, and Pavithra Prabhakar)
  in Annals of Pure and Applied Logic, Volume 161, Issue 3, December 2009, Pages 324-336. (Definitive version.) An extended version will also appear as the article Automata and Logics over signals in the review volume "Modern Applications of Automata Theory", IISc-World Scientific Press, 2010.

• Conflict-Tolerant Features
  (with Madhu Gopinathan)
  in proc. 20th Int. Conference on Computer Aided Verification (CAV) 2008, Princeton, pages 227-239. Technical Report.

• Counter-free input-determined timed automata
  (with Fabrice Chevalier and Pavithra Prabhakar),
  in FORMATS 2007, LNCS 4763, pp. 82--97. A Technical Report is also available.

• A decidable temporal logic of repeating values
  (with Stephane Demri and Regis Gascon)
  in Proc. Symposium on Logical Foundations of Computer Science (LFCS) 2007, LNCS 4514, pp. 180--194.

• On continuous timed automata with input-determined guards
  (with Fabrice Chevalier and Pavithra Prabhakar)
  in Proc. FSTTCS 2006, LNCS vol. 4337, pp. 369-380, (2006).

• Checking unwinding conditions for finite state systems
  (with K. R. Raghavendra)
  VERIFY 2006 Workshop (2006).

• On the expressiveness of MTL with past operators
  (with Pavithra Prabhakar)
  in Proc. FORMATS 2006, LNCS 4202, pp. 322-336 (2006).

• Computing complete test graphs for hierarchical systems
  (with Madhu Gopinathan)
  in Proc. IEEE SEFM 2006, pp. 70-79 (2006).

• A unification-based decision procedure for cryptographic protocol analysis
  (with Deepak Bhardwaj)
  Proc. WITS 2006, pp. 221--235 (2006).

• Eventual timed automata
  (with M. Raj Mohan)
  FSTTCS 2005, Springer LNCS 3821, 322--344 (2005). Also available as Technical Report.

• On the expressiveness of MTL in the pointwise and continuous semantics
  (with Pavithra Prabhakar)
  in Formal Methods Letters, Software Tools for Technology Transfer, Vol. 9, No. 1, pp 1--4, Springer (2007).
  Also available as Technical Report.

• An automata-based approach to verifying information flow properties
  (with K R Raghavendra and Barbara Sprick)
  in Proc. ARSPA Workshop 2005, ENTCS vol 135, issue 1 (2005).

• Fault diagnosis using timed automata
  (with Patricia Bouyer and Fabrice Chevalier)
  in Proc. FOSSACS 2005, LNCS 3441, pp. 219--233.

• On timed automata with input-determined guards
  (with Nicolas Tabareau),
  in Proc. FORMATS-FTRTFT 2004, LNCS 3253 (2004).
• Timed control with partial observability
  (with Patricia Bouyer, P. Madhusudan, and Antoine Petit),
  in Proc. 15th Conf. on Computer Aided Verification (CAV 2003), LNCS 2725 (2003).
• Checking consistency of SDL+MSC specifications
  (with Madhavan Mukund),
  in Proc. 10th International SPIN Workshop on Model Checking of Software (SPIN 2003) LNCS 2648 (2003).
• A Logical Characterisation of Event Clock Automata
  in Intl. Journal of Foundations of Computer Science, Vol. 14, No. 4, World Scientific (2003), 625--639.
• An Automata-Theoretic Approach to Constraint LTL,
  (with Stéphane Demri)
  in Proc. 22nd Foundations of Software Technology and Theoretical Computer Science (FSTTCS) LNCS 2256 (2002).
  Journal version in Information and Computation, Vol. 205, issue 3, pp 380--415 (2007).
• Timed control synthesis for external specifications
  (with P. Madhusudan)
  Proc. STACS 2002, LNCS 2285, 2002.
• Product Interval Automata,
  (with P.S.Thiagarajan)
  in Sadhana, Academy Proceedings in Engineering Sciences, Vol. 27, No. 2, Indian Academy of Sciences (2002), 181--208.
• A Logical Characterisation of Event Recording Automata
  Proc. FTRTFT 2000, LNCS 1926, 2000.
• Product Interval Automata: A Subclass of Timed Automata
  (with P. S. Thiagarajan)
  Proceedings of 19th FSTTCS, LNCS 1732, 1999.
• On-the-fly Verification for Product-LTL
  (with P. Madhusudan)
  Proceedings of Seventh National Seminar on Theoretical Computer Science, 1997.




Reports/Thesis

• A Logical Study of Distributed Timed Automata
  Ph.D. Thesis submitted to BITS, Pilani, 2000.
• Distributed Interval Automata: A Subclass of Timed Automata
  (with P. S. Thiagarajan)
  Internal Report TCS-98-3, Chennai Mathematical Institute, 1998.
• On-the-fly Verification for Linear Time Temporal Logic
  M.Phil. Dissertation submitted to BITS, Pilani, 1997.