Demo Data from EDBT 2026 / reviewers in the wild / expert
Thomas Braibant
dblp:19/1989
· DBLP profile ↗
8ranked-venue papers
6as first author
0since 2021 · last 2014
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 6 · 5 first-authorSoftware engineering, systems software and programming languages · 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 · 46% Memory systems · 27% Processor architecture and microarchitecture · 27% | |
| Software engineering, system software, and programming languages
1 paper |
Program verification · 100% |
Topics — the 6 heaviest of 8, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Electronic design automation › hardware verification and test
formal verification |
0.2 | 1 | 2013 | Formal Verification of Hardware Synthesis · CAV 2013 |
Electronic design automation
hardware verification and test |
0.2 | 1 | 2013 | Formal Verification of Hardware Synthesis · CAV 2013 |
Processor architecture and microarchitecture
instruction set architecture |
0.1 | 1 | 2009 | The semantics of x86-CC multiprocessor machine code · POPL 2009 |
Memory systems › memory consistency
memory consistency model |
0.1 | 1 | 2009 | The semantics of x86-CC multiprocessor machine code · POPL 2009 |
Processor architecture and microarchitecture › instruction set architecture › CISC
x86 |
0.1 | 1 | 2009 | The semantics of x86-CC multiprocessor machine code · POPL 2009 |
Memory systems › memory consistency › memory consistency model
x86 memory model |
0.1 | 1 | 2009 | The semantics of x86-CC multiprocessor machine code · POPL 2009 |
Methods — techniques the papers use, named apart from their topics
axiomatic semantics · 0.2
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2014 | Compositional Computational Reflection
Gregory Malecha, Adam Chlipala, Thomas Braibant |
ITP | 3 |
| 2014 | Implementing and Reasoning About Hash-consed Data Structures in Coq
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
J. Autom. Reason. | 1 |
| 2013 | Formal Verification of Hardware Synthesis
Thomas Braibant, Adam Chlipala |
CAV | 1 |
| 2013 | Implementing Hash-Consed Structures in Coq
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
ITP | 1 |
| 2011 | Coquet: A Coq Library for Verifying Hardware
Thomas Braibant |
CPP | 1 |
| 2011 | Tactics for Reasoning Modulo AC in Coq
Thomas Braibant, Damien Pous |
CPP | 1 |
| 2010 | An Efficient Coq Tactic for Deciding Kleene Algebras
Thomas Braibant, Damien Pous |
ITP | 1 |
| 2009 | The semantics of x86-CC multiprocessor machine codeabstractMultiprocessors are now dominant, but real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, usually described only in ambiguous prose, leading to widespread confusion. Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave |
POPL | 6 |