Demo Data from EDBT 2026 / reviewers in the wild / expert
Tycho Andersen
dblp:08/8296
· DBLP profile ↗
3ranked-venue papers
0as first author
0since 2021 · last 2014
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 3Theory 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 analysis · 68% Program verification · 32% |
Topics — the 5 heaviest of 5, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program analysis › static analysis › abstract interpretation
abstract domain |
0.2 | 1 | 2014 | Abstract Domains of Affine Relations · ACM Trans. Program. Lang. Syst. 2014 |
Program analysis › static analysis
abstract interpretation |
0.2 | 1 | 2014 | Abstract Domains of Affine Relations · ACM Trans. Program. Lang. Syst. 2014 |
Program verification › code-level verification
machine code verification |
0.1 | 1 | 2010 | Directed Proof Generation for Machine Code · CAV 2010 |
Program verification
automated verification |
0.0 | 1 | 2010 | Directed Proof Generation for Machine Code · CAV 2010 |
Program verification
proof generation |
0.0 | 1 | 2010 | Directed Proof Generation for Machine Code · CAV 2010 |
Methods — techniques the papers use, named apart from their topics
linear algebra over modules · 0.2abstract transformers · 0.2directed proof generation · 0.1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2014 | Abstract Domains of Affine RelationsabstractThis article considers some known abstract domains for affine-relation analysis (ARA), along with several variants, and studies how they relate to each other. The various domains represent sets of points that satisfy affine relations over variables that hold machine integers and are based on an extension of linear algebra to modules over a ring (in particular, arithmetic performed modulo 2 w , for some machine-integer width w ). We show that the abstract domains of Müller-Olm/Seidl (MOS) and King/Søndergaard (KS) are, in general, incomparable. However, we give sound interconversion methods. In other words, we give an algorithm to convert a KS element v KS to an overapproximating MOS element v MOS —that is, γ ( v KS ) ⊆ γ ( v MOS —as well as an algorithm to convert an MOS element w MOS to an overapproximating KS element w KS —that is, γ ( w MOS ) ⊆ γ ( w KS ). The article provides insight on the range of options that one has for performing ARA in a program analyzer: —We describe how to perform a greedy, operator-by-operator abstraction method to obtain KS abstract transformers. —We also describe a more global approach to obtaining KS abstract transformers that considers the semantics of an entire instruction, basic block, or other loop-free program fragment. The latter method can yield best abstract transformers, and hence can be more precise than the former method. However, the latter method is more expensive. We also explain how to use the KS domain for interprocedural program analysis using a bit-precise concrete semantics, but without bit blasting. Matt Elder, Junghee Lim, Tushar Sharma 0003, Tycho Andersen, Thomas W. Reps |
ACM Trans. Program. Lang. Syst. | 4 |
| 2011 | Abstract Domains of Affine Relations
Matt Elder, Junghee Lim, Tushar Sharma 0003, Tycho Andersen, Thomas W. Reps |
SAS | 4 |
| 2010 | Directed Proof Generation for Machine Code
Aditya V. Thakur, Junghee Lim, Akash Lal, Amanda Burton, Evan Driscoll, Matt Elder, Tycho Andersen, Thomas W. Reps |
CAV | 7 |