Demo Data from SIGIR 2026 / reviewers in the wild / expert
David Espinosa
dblp:77/4852
· DBLP profile ↗
4ranked-venue papers
0as first author
0since 2021 · last 2007
0000-0002-9938-4686ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 3Systems, architecture and hardware · 1Theory of computation · 1
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.
| Software engineering, system software, and programming languages
2 papers |
Program verification · 100% |
Topics — the 6 heaviest of 6, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program verification › program logic
hoare logic |
0.1 | 1 | 2007 | Enforcing resource bounds via static verification of dynamic checks · ACM Trans. Program. Lang. Syst. 2007 |
Program verification › quantitative verification
resource bound verification |
0.1 | 1 | 2007 | Enforcing resource bounds via static verification of dynamic checks · ACM Trans. Program. Lang. Syst. 2007 |
Program verification › quantitative verification
resource verification |
0.1 | 1 | 2007 | Enforcing resource bounds via static verification of dynamic checks · ACM Trans. Program. Lang. Syst. 2007 |
Program verification
static verification |
0.1 | 1 | 2007 | Enforcing resource bounds via static verification of dynamic checks · ACM Trans. Program. Lang. Syst. 2007 |
Program verification › code-level verification
java verification |
0.1 | 1 | 2005 | JVer: A Java Verifier · CAV 2005 |
Program verification
dynamic verification |
0.0 | 1 | 2007 | Enforcing resource bounds via static verification of dynamic checks · ACM Trans. Program. Lang. Syst. 2007 |
Methods — techniques the papers use, named apart from their topics
static analysis · 0.1linear inequalities · 0.1hoare logic · 0.1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2007 | Enforcing resource bounds via static verification of dynamic checksabstractWe show how to limit a program's resource usage in an efficient way, using a novel combination of dynamic checks and static analysis. Usually, dynamic checking is inefficient due to the overhead of checks, while static analysis is difficult and rejects many safe programs. We propose a hybrid approach that solves these problems. We split each resource-consuming operation into two parts. The first is a dynamic check, called reserve. The second is the actual operation, called consume, which does not perform any dynamic checks. The programmer is then free to hoist and combine reserve operations. Combining reserve operations reduces their overhead, while hoisting reserve operations ensures that the program does not run out of resources at an inconvenient time. A static verifier ensures that the program reserves resources before it consumes them. This verification is both easier and more flexible than an a priori static verification of resource usage. We present a sound and efficient static verifier based on Hoare logic and linear inequalities. As an example, we present a version of tar written in Java. Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee 0001, George C. Necula |
ACM Trans. Program. Lang. Syst. | 2 |
| 2005 | JVer: A Java Verifier
Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee 0001, George C. Necula |
CAV | 2 |
| 2005 | Enforcing Resource Bounds via Static Verification of Dynamic Checks
Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee 0001, George C. Necula |
ESOP | 2 |
| 1994 | Fast Parallel Solution of Fixed Point Equations for the Performance Evaluation of Circuit-Switched Networks
Albert G. Greenberg, Andrew M. Odlyzko, Jennifer Rexford, David Espinosa |
Perform. Evaluation | 4 |