6 papers
The Complexity of Coverability-Like Problems in Elementary Object Systems: Data-Nets to the Rescue
Francesco Di Cosmo, Soumodev Mal, Tephilla Prince
Elementary Object Systems (EOSs) are a model in the nets-within-nets (NWNs) paradigm, where tokens in turn can host standard Petri nets. We study the complexity of coverability-lik…
Verification of Unbounded Client-Server Systems with Distinguishable Clients
Ramchandra Phawade, Tephilla Prince, S Sheerazuddin
Client-server systems are a computing paradigm in concurrent and distributed systems. We deal with unbounded client-server systems (UCS) where all clients are of the same type, int…
Nets-within-Nets through the Lens of Data Nets
Francesco Di Cosmo, Soumodev Mal, Tephilla Prince
Elementary Object Systems (EOSs) are a model in the nets-within-nets (NWNs) paradigm, where tokens in turn can host standard Petri nets. We study the complexity of the reachability…
A Lower Bound on Conservative Elementary Object Systems Coverability
Francesco Di Cosmo, Soumodev Mal, Tephilla Prince
Elementary Object Systems (EOS) are a form of Petri Net (PN) where tokens carry internal PN. This model has been recently proposed for analysis of robustness of Multi Agent Systems…
Bounded Model Checking for Unbounded Client Server Systems
Ramchandra Phawade, Tephilla Prince, S. Sheerazuddin
Bounded model checking (BMC) is an efficient formal verification technique which allows for desired properties of a software system to be checked on bounded runs of an abstract mod…
Formal Verification of Safety Properties Using Interpolation and k-induction
Tephilla Prince, Atif Abdur Rahman, Sheerazuddin Syed
This technical report presents implementation of two symbolic model checking algorithms that use SAT/SMT Solvers, namely interpolation based model checking and k-induction based mo…