VLDB 2026 Research / reviewers in the wild / expert
Matthew Wilding
dblp:55/5887
· DBLP profile ↗
6ranked-venue papers
4as 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 · 4 · 2 first-authorTheory of computation · 4 · 3 first-authorArtificial intelligence and machine learning · 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.
| Computer architecture, parallel and distributed computing, and storage systems
2 papers |
Electronic design automation · 33% Embedded and real-time systems · 33% Performance modeling and evaluation · 33% | |
| Theoretical computer science
3 papers |
Automated reasoning and model checking · 100% | |
| Software engineering, system software, and programming languages
1 paper |
Program verification · 100% |
Topics — the 5 heaviest of 6, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Automated reasoning and model checking › theorem proving
mechanical verification |
0.0 | 2 | 1998 | A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy · CAV 1998 A Mechanically Verified Application for a Mechanically Verified Environment · CAV 1993 |
Electronic design automation › hardware verification and test
hardware verification |
0.0 | 1 | 1998 | Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle · CAV 1998 |
Performance modeling and evaluation › scheduling optimization
optimal scheduling |
0.0 | 1 | 1998 | A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy · CAV 1998 |
Embedded and real-time systems
real-time scheduling |
0.0 | 1 | 1998 | A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy · CAV 1998 |
Automated reasoning and model checking
theorem proving |
0.0 | 1 | 1998 | Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle · CAV 1998 |
Methods — techniques the papers use, named apart from their topics
proof assistant · 0.1theorem proving · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2008 | Efficient execution in an automated reasoning environmentabstractAbstract We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the features supporting this method allow the user to install, in a logically sound way, alternative executable counterparts for logically defined functions. These alternatives are often much more efficient than the logically equivalent terms they replace. These features have been implemented in the ACL2 theorem prover, and we discuss several applications of the features in ACL2. David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Robert W. Sumners, Daron Vroon 0001, Matthew Wilding |
J. Funct. Program. | 9 |
| 2001 | Efficient Simulation of Formal Processor Models
Matthew Wilding, David A. Greve, David S. Hardin |
Formal Methods Syst. Des. | 1 |
| 1998 | Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle
David S. Hardin, Matthew Wilding, David A. Greve |
CAV | 2 |
| 1998 | A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy
Matthew Wilding |
CAV | 1 |
| 1993 | A Mechanically Verified Application for a Mechanically Verified Environment
Matthew Wilding |
CAV | 1 |
| 1991 | Proving Matijasevich's Lemma with a Default Arithmetic Strategy
Matthew Wilding |
J. Autom. Reason. | 1 |