BZPEERReading, trust and collaboration for research
Menu

Discover

SearchFind papers, people, topics and opportunities from one place.GraphOpen maps around papers, topics and saved views.

Workspaces

HomeOpen the ranked research feed.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Source author record

S. Arun-Kumar

S. Arun-Kumar appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer ScienceFormal Languages and Automata TheoryProgramming LanguagesDistributed, Parallel, and Cluster ComputingSoftware Engineering

Catalog footprint

What is connected

5works
5topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

5 published item(s)

preprint2016arXiv

Efficient Verification of Concurrent Programs Over TSO Memory Model

We address the problem of efficient verification of multi-threaded programs running over Total Store Order (TSO) memory model. It has been shown that even with finite data domain programs, the complexity of control state reachability under TSO is non-primitive recursive. In this paper, we first present a bounded-buffer verification approach wherein a bound on the size of buffers is placed; verification is performed incrementally by increasing the size of the buffer with each iteration of the verification procedure until the said bound is reached. For programs operating on finite data domains, we also demonstrate the existence of a buffer bound k such that if the program is safe under that bound, then it is also safe for unbounded buffers. We have implemented this technique in a tool ProofTraPar. Our results against memorax [2], a state-of-the-art sound and complete verifier for TSO memory model, have been encouraging.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

From Traces To Proofs: Proving Concurrent Program Safe

Nondeterminism in scheduling is the cardinal reason for difficulty in proving correctness of concurrent programs. A powerful proof strategy was recently proposed [6] to show the correctness of such programs. The approach captured data-flow dependencies among the instructions of an interleaved and error-free execution of threads. These data-flow dependencies were represented by an inductive data-flow graph (iDFG), which, in a nutshell, denotes a set of executions of the concurrent program that gave rise to the discovered data-flow dependencies. The iDFGs were further transformed in to alternative finite automatons (AFAs) in order to utilize efficient automata-theoretic tools to solve the problem. In this paper, we give a novel and efficient algorithm to directly construct AFAs that capture the data-flow dependencies in a concurrent program execution. We implemented the algorithm in a tool called ProofTraPar to prove the correctness of finite state cyclic programs under the sequentially consistent memory model. Our results are encouranging and compare favorably to existing state-of-the-art tools.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Reducing Clocks in Timed Automata while Preserving Bisimulation

Model checking timed automata becomes increasingly complex with the increase in the number of clocks. Hence it is desirable that one constructs an automaton with the minimum number of clocks possible. The problem of checking whether there exists a timed automaton with a smaller number of clocks such that the timed language accepted by the original automaton is preserved is known to be undecidable. In this paper, we give a construction, which for any given timed automaton produces a timed bisimilar automaton with the least number of clocks. Further, we show that such an automaton with the minimum possible number of clocks can be constructed in time that is doubly exponential in the number of clocks of the original automaton.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

A Unifying Approach to Decide Relations for Timed Automata and their Game Characterization

In this paper we present a unifying approach for deciding various bisimulations, simulation equivalences and preorders between two timed automata states. We propose a zone based method for deciding these relations in which we eliminate an explicit product construction of the region graphs or the zone graphs as in the classical methods. Our method is also generic and can be used to decide several timed relations. We also present a game characterization for these timed relations and show that the game hierarchy reflects the hierarchy of the timed relations. One can obtain an infinite game hierarchy and thus the game characterization further indicates the possibility of defining new timed relations which have not been studied yet. The game characterization also helps us to come up with a formula which encodes the separation between two states that are not timed bisimilar. Such distinguishing formulae can also be generated for many relations other than timed bisimilarity.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Inferring Fences in a Concurrent Program Using SC proof of Correctness

Most proof systems for concurrent programs assume the underlying memory model to be sequentially consistent (SC), an assumption which does not hold for modern multicore processors. These processors, for performance reasons, implement relaxed memory models. As a result of this relaxation a program, proved correct on the SC memory model, might execute incorrectly. To ensure its correctness under relaxation, fence instructions are inserted in the code. In this paper we show that the SC proof of correctness of an algorithm, carried out in the proof system of [Sou84], identifies per-thread instruction orderings sufficient for this SC proof. Further, to correctly execute this algorithm on an underlying relaxed memory model it is sufficient to respect only these orderings by inserting fence instructions.

0 citations0 reviewsNo code linkedOpen access