Publications
Journal and Conference Articles
-
Kondo: Efficient Provenance-Driven Data Debloating
Aniket Modi, Rohan Tikmany, Tanu Malik, Raghavan Komondoor, Ashish
Gehani, Deepak D'Souza.
40th IEEE International Conference on Data Engineering (ICDE 2024).
-
Weakest Precondition Inference for Non-Deterministic Linear Array
Programs
Sumanth Prabhu, Deepak D'Souza, Supratik Chakraborty, Venkatesh R, and
Grigory Fedyukovich.
30th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS 2024).
-
Maximal Quantified Precondition Synthesis for Linear Array Loops
Sumanth Prabhu, Grigory Fedyukovich, and Deepak D'Souza.
32nd European Symposium on Programming Languages (ESOP 2024).
-
Symbolic Fixpoint Algorithms for Logical LTL Games
Stanly Samuel, Deepak D'Souza, and K V Raghavan.
International Conference on Automated Software Engineering (ASE 2023).
-
Data-Driven Learning of Strong Conjunctive Invariants
Arkesh Thakkar and Deepak D'Souza.
Formal Methods in Computer-Aided Design (FMCAD 2023).
-
Verification of Camera-Based Autonomous Systems.
Habeeb. P, Nabarun Deka, Deepak D'Souza, Kamal Lodaya and Pavithra Prabhakar.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2023.
-
Static Executes-Before Analysis for Event Driven Programs.
Rekha Pai, Abhishek Uppar, Akshatha Shenoy, Pranshul Kushwaha, Deepak D'Souza.
ESEC/FSE 2022.
-
Static Race Detection for Periodic Programs.
Varsha P Suresh,
Rekha Pai,
Sujit Kumar Chakrabarti,
Deepak D'Souza,
Meenakshi D'Souza.
ESOP 2022.
-
On the Expressiveness of TPTL in the Pointwise and Continous Semantics.
Raveendra Holla, Nabarun Deka, Deepak D'Souza.
FSTTCS 2021.
-
GenSys: A Scalable Fixed-point Engine for Maximal Controller Synthesis
over Infinite State Spaces.
Stanly Samuel, Deepak D'Souza, Raghavan Komondoor.
FSE Demo Track 2021.
- Specification Synthesis with Constrained Horn Clauses.
Sumanth Prabhu, Grigory Fedyukovich, Kumar Madhukar, Deepak
D'Souza.
PLDI 2021 (Distinguished Paper Award).
-
Static analysis for detecting high-level races in RTOS kernels.
Rekha Pai, Abhishek Singh, Deepak D'Souza, Meenakshi D'Souza, Prathibha Prakash.
Formal Methods in Systems Design (FMSD), 58(1-2): 294-321, 2021.
-
Static Race Detection for RTOS Applications.
Rishi Tulsyan, Rekha Pai, Deepak D'Souza.
FSTTCS 2020.
-
Verification of a Generative Separation Kernel.
Inzemamul Haque, Deepak D'Souza, P. Habeeb, Arnab Kundu, Ganesh Babu.
ATVA 2020, LNCS 12302, Spinger.
-
Verifying Band Convergence for Sampled Control Systems.
P. Ezudheen, Zahra Afzal, Pavithra Prabhakar, Deepak D'Souza, and Meenakshi D'Souza.
NASA Formal Methods (NFM) 2020.
-
Static Analysis for Detecting High-Level Races in RTOS Kernels.
Abhishek Singh, Rekha Pai, Deepak D'Souza, Meenakshi D'Souza.
Formal Methods Symposium (FM) 2019, LNCS 11800, Springer.
-
Data Races and Static Analysis for Interrupt-Driven Kernels.
Nikita Chopra, Rekha Pai, Deepak D'Souza.
ESOP 2019, LNCS 11423, Springer.
-
Horn-ICE learning for synthesizing invariants and contracts,
P. Ezudheen, Daniel Neider, Deepak D'Souza, Pranav Garg, P. Madhusudan.
PACMPL 2 (OOPSLA), 131:1-131:25, 2018.
- A Thread-Local Semantics and its Efficient Sequential Abstractions for Race-Free Programs,
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetsky.
24th Static Analysis Symposium (SAS) 2017.
-
Detecting all High-Level Dataraces in an RTOS Kernel,
Suvam Mukherjee, S. Arun Kumar, Deepak D'Souza.
Proc. 18th VMCAI, 2017.
-
An optimization based approach for matching applications with textual models,
Tejas Patil, Raghavan Komondoor, Deepak D'Souza and Indrajit Bhattacharya.
Proc. 32nd ICSME, 2016.
-
Model-checking trace-based information flow properties for infinite-state systems.
Deepak D'Souza and Raghavendra K. R.
Journal of Computer Security, vol 24(5): 617-643, 2016.
-
Refinement-Based Verification of the FreeRTOS Scheduler in VCC.
Sumesh Divakaran, Deepak D'Souza, Anirudh Kushwah, Prahladavaradan Sampath, Nigamanth Sridhar, and Jim Woodcock
Proc. ICFEM 2015, LNCS 9407, 170-186 (2015).
-
Using formal reasoning on a model of tasks for FreeRTOS,
Shu Cheng, Jim Woodcock, and Deepak D'Souza,
in Formal Aspects of Computing, volume 27, issue 1, pp 167-192, Jan 2015.
-
A Multi-Core Version of FreeRTOS
Verified for Datarace and Deadlock Freedom,
(with Prakash Chandrasekaran, Shibu Kumar K B, Remish L. Minz, and Lomesh Meshram),
in proc. 12th ACM-IEEE International Conference on Formal Methods and
Models for System Design (MEMOCODE) 2014.
-
Efficient Refinement Checking in VCC,
(with Sumesh Divakaran and Nigamanth Sridhar),
in proc. VSTTE 2014, LNCS 8471.
-
Using relationships for matching textual domain models with existing code.,
(with Raghavan Komondoor, Indrajit Bhattacharya, and Sachin Kale),
in proc. WCRE 2013, pp. 371-380, 2013.
-
A compositional hierarchical monitoring
automaton construction for LTL,
(with Raj Mohan M.),
in proc. ICTAC 2012, LNCS vol. 7521.
-
Temporal Logics of Repeating Values
(with Stephane Demri and Regis Gascon),
Journal of Logic and Computation,
volume 22, issue 5, pp. 1059-1096 (2012).
-
Model-checking bisimulation-based information flow properties for infinite state systems,
(with Raghavendra K. R.),
in proc. ESORICS, LNCS vol. 7459 (2012).
-
Scalable Flow-Sensitive Pointer Analysis for
Java with Strong Updates
(with Arnab De),
in proc. ECOOP 2012, LNCS 7313.
-
Conflict-Tolerant Specifications for
Hybrid Systems,
(with Madhu Gopinathan, S. Ramesh, and Prahladavaradan Sampath),
Journal of IISc, Vol. 93, No. 3, 2013.
-
Dataflow analysis for data-race free programs,
(with Arnab De and Rupesh Nasre),
in Proc. ESOP 2011, LNCS 6602, 2011.
-
Model-checking trace-based information flow properties,
Deepak D'Souza, Raveendra Holla, K. R. Raghavendra, and Barbara Sprick,
Journal of Computer Security, Vol 19, Issue 1, pp 101-138, 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