Demonstration venue · read-only. Every page can be browsed; the buttons that would change it are switched off. Create an account to run TaxoReview on your own data.

Tommy Schneider

dblp:278/0465 · DBLP profile ↗
← Back
1ranked-venue papers
0as first author
0since 2021 · last 2020
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 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
1 paper
Program analysis · 100%

Topics — the 2 heaviest of 2, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Program analysis › constraint solving
model counting
0.412020
MCBAT: a practical tool for model counting constraints on bounded integer arrays · ESEC/SIGSOFT FSE 2020
Program analysis
quantitative program analysis
0.412020
MCBAT: a practical tool for model counting constraints on bounded integer arrays · ESEC/SIGSOFT FSE 2020

Methods — techniques the papers use, named apart from their topics

integer lattice point enumeration · 0.4barvinok's algorithm · 0.4array theory reduction · 0.4
YearPublicationVenuePosition
2020 MCBAT: a practical tool for model counting constraints on bounded integer arrays
abstract
Model counting procedures for data structures are crucial for advancing the field of automated quantitative program analysis. We present a tool for Model Counting for Bounded Array Theory (MCBAT). MCBAT works on quantified integer array constraints in which all arrays have a finite length. We employ reductions from the theory of arrays to uninterpreted functions and linear integer arithmetic (LIA). Once reduced to LIA, we leverage Barvinok's polynomial time integer lattice point enumeration algorithm. Finally, we present a case study demonstrating applicability to automated quantitative program analysis. MCBAT is available for immediate use as a Docker image and the source code is freely available in our Github repository.
Abtin Molavi, Mara Downing, Tommy Schneider, Lucas Bang
ESEC/SIGSOFT FSE3