Browsing by Advisor "D'Souza, Deepak"

Now showing items 1-11 of 11

    • Access Path Based Dataflow Analysis For Sequential And Concurrent Programs 

      Arnab De, * (2016-09-14)
      In this thesis, we have developed a flow-sensitive data flow analysis framework for value set analyses for Java-like languages. Our analysis frame work is based on access paths—a variable followed by zero or more field ...

    • Analysing Message Sequence Graph Specifications 

      Chakraborty, Joy (2011-03-29)
      Message Sequence Charts are a visual representation of the system specification which shows how all the participating processes are interacting with each other. Message Sequence Graphs provide modularity by easily allowing ...

    • Boolean Functional Synthesis using Gated Continuous Logic Networks 

      Raja, Ravi
      Boolean Functional Synthesis (BFS) is a well-known challenging problem in the domain of automated program synthesis from logical specifications. This problem aims to synthesize a Boolean function that is correct-by-construction ...

    • Conflict-Tolerant Features 

      Gopinathan, Madhu (2010-12-07)
      Large, software intensive systems are typically developed using a feature oriented development paradigm in which feature specifications are derived from domain requirements and features are implemented to satisfy such ...

    • Efficient Static Analyses for Concurrent Programs 

      Mukherjee, Suvam (2018-06-29)
      Concurrent programs are pervasive owing to the increasing adoption of multi-core systems across the entire computing spectrum. However, the large set of possible program behaviors make it difficult to write correct and ...

    • Learning Invariants for Verification of Programs and Control Systems 

      Ezudheen, P
      Deductive verification techniques in the style of Floyd and Hoare have the potential to give us concise, compositional, and scalable proofs of the correctness of various kinds of software systems like programs and control ...

    • Model-Checking Infinite-State Systems For Information Flow Security Properties 

      Raghavendra, K R (2017-02-16)
      Information flow properties are away of specifying security properties of systems ,dating back to the work of Goguen and Meseguer in the eighties. In this framework ,a system is modeled as having high-level (or confidential)events ...

    • A Refinement-Based Methodology for Verifying Abstract Data Type Implementations 

      Divakaran, Sumesh (2018-06-21)
      This thesis is about techniques for proving the functional correctness of Abstract Data Type (ADT) implementations. We provide a framework for proving the functional correctness of imperative language implementations of ...

    • Specification Synthesis with Constrained Horn Clauses 

      Sumanth Prabhu, S
      Many practical problems in software development, verification and testing rely on specifications. The problem of specification synthesis is to automatically find relational constraints for undefined functions, called ...

    • A Theoretical Study of the Synergy and Lazy Annotation Algorithms 

      Jayaram, Sampath (2018-04-03)
      Given a program with assertions, the assertion checking problem is to tell whether there is an execution of the program that violates one of the assertions. One approach to this problem is to explore different paths towards ...

    • Verification of a Generative Separation Kernel 

      Haque, Inzemamul
      A Separation Kernel is a small specialized microkernel that provides a sand-boxed execution environment for a given set of processes (also called \subjects"). The subjects may communicate only via declared memory channels, ...