Demo Data from EDBT 2026 / reviewers in the wild / expert
Sujatha Kashyap
dblp:00/1910
· DBLP profile ↗
3ranked-venue papers
3as first author
0since 2021 · last 2008
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 2 · 2 first-authorTheory of computation · 2 · 2 first-authorDatabases, data management, data science and information retrieval · 1 · 1 first-author
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Theoretical computer science
1 paper |
Automated reasoning and model checking · 100% | |
| Software engineering, system software, and programming languages
1 paper |
Program verification · 100% |
Topics — the 3 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Automated reasoning and model checking › model checking
counterexample generation |
0.1 | 1 | 2008 | Producing Short Counterexamples Using "Crucial Events" · CAV 2008 |
Program verification
model checking |
0.1 | 1 | 2005 | Exploiting predicate structure for efficient reachability detection · ASE 2005 |
Program verification › model checking
partial order reduction |
0.1 | 1 | 2005 | Exploiting predicate structure for efficient reachability detection · ASE 2005 |
Methods — techniques the papers use, named apart from their topics
vector timestamps · 0.1persistent sets · 0.1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2008 | Producing Short Counterexamples Using "Crucial Events"
Sujatha Kashyap, Vijay K. Garg |
CAV | 1 |
| 2005 | Exploiting predicate structure for efficient reachability detectionabstractPartial order (p.o.) reduction techniques are a popular and effective approach for tackling state space explosion in the verification of concurrent systems. These techniques generate a reduced search space that could be exponentially smaller than the complete state space. Their major drawback is that the amount of reduction achieved is highly sensitive to the properties being verified. For the same program, different properties could result in very different amounts of reduction achieved.We present a new approach which combines the benefits of p.o. reduction with the added advantage that the size of the constructed state space is completely independent of the properties being verified. As in p.o. reduction, we use the notion of persistent sets to construct a representative interleaving for each maximal trace of the program. However, we retain concurrency information by assigning vector timestamps to the events in each interleaving. Our approach hinges upon the use of efficient algorithms that parse the encoded concurrency information in the representative interleaving to determine whether a safety violation exists in any interleaving of the corresponding trace. We show that, for some types of predicates, reachability detection can be performed in time that is polynomial in the length of the interleaving. Typically, these predicates exhibit certain characteristics that can be exploited by the detection algorithm.We implemented our algorithms in the popular model checker SPIN, and present experimental results that demonstrate the effectiveness of our techniques. For example, we verified a distributed dining philosophers protocol in 0.03 seconds, using 1.253 MB of memory. SPIN, using traditional p.o. reduction techniques, took 759.71 seconds and 439.116 MB of memory. Sujatha Kashyap, Vijay K. Garg |
ASE | 1 |
| 2005 | Intractability results in predicate detection
Sujatha Kashyap, Vijay K. Garg |
Inf. Process. Lett. | 1 |