Michael Rawson

44 papers A* 3A 4B 11Journal 17Unranked 9
YearRankTypeTitle / Venue / Authors
2026 J jnl
Constraint Learning for Non-confluent Proof Search.
CoRR
Michael Rawson, Clemens Eisenhofer, Laura Kovács
2026 J jnl
Finding Connections via Satisfiability Solving.
CoRR
Clemens Eisenhofer, Michael Rawson, Laura Kovács
2026 J jnl
Lean on Vampire Proofs (Short Paper).
CoRR
Jonas Bodingbauer, Márton Hajdú, Laura Kovács, Axel Polaczek, Michael Rawson
2025 J jnl
Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo.
CoRR
Anja Petkovic Komel, Michael Rawson, Martin Suda
2025 B conf
Constraint Learning for Non-confluent Proof Search.
TABLEAUX
Michael Rawson, Clemens Eisenhofer, Laura Kovács
2025 J jnl
Divide and Conquer: A Compositional Approach to Game-Theoretic Security.
Proc. ACM Program. Lang.
Ivana Bocevska, Anja Petkovic Komel, Laura Kovács, Sophie Rain, Michael Rawson
2025 A* conf
Expressive Power of Temporal Message Passing.
AAAI
Przemyslaw Andrzej Walega, Michael Rawson
2025 B conf
Finding Connections via Satisfiability Solving.
TABLEAUX
Clemens Eisenhofer, Michael Rawson, Laura Kovács
2025 B conf
Game Modeling of Blockchain Protocols.
iFM
Sophie Rain, Anja Petkovic Komel, Michael Rawson, Laura Kovács
2025 A conf
Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories.
CADE
Michael Rawson, Andrei Voronkov, Johannes Schoisswohl, Anja Petkovic Komel
2025 J jnl
SAT solving for variants of first-order subsumption.
Formal Methods Syst. Des.
Robin Coutelier, Jakob Rath, Michael Rawson, Armin Biere, Laura Kovács
2025 — conf
The Vampire Diary.
CAV (3)
Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
2025 J jnl
The Vampire Diary.
CoRR
Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
2024 A* conf
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model.
SP
Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson
2024 J jnl
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model.
IACR Cryptol. ePrint Arch.
Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson
2024 J jnl
Expressive Power of Temporal Message Passing.
CoRR
Przemyslaw Andrzej Walega, Michael Rawson
2024 — conf
Reducibility Constraints in Superposition.
IJCAR (1)
Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov
2024 B conf
Rewriting and Inductive Reasoning.
LPAR
Márton Hajdú, Laura Kovács, Michael Rawson
2024 J jnl
Rewriting and Inductive Reasoning.
CoRR
Márton Hajdú, Laura Kovács, Michael Rawson
2024 J jnl
SAT Solving for Variants of First-Order Subsumption.
CoRR
Robin Coutelier, Jakob Rath, Michael Rawson, Armin Biere, Laura Kovács
2024 J jnl
SAT-Based Subsumption Resolution.
CoRR
Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath
2024 B conf
Scaling CheckMate for Game-Theoretic Security.
LPAR
Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovács, Michael Rawson
2024 J jnl
Scaling Game-Theoretic Security Reasoning.
CoRR
Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovács, Michael Rawson
2024 J jnl
Spanning Matrices via Satisfiability Solving.
CoRR
Clemens Eisenhofer, Michael Rawson, Laura Kovács
2024 J jnl
Superposition with Delayed Unification.
CoRR
Ahmed Bhayat, Johannes Schoisswohl, Michael Rawson
2023 A* conf
CheckMate: Automated Game-Theoretic Security Reasoning.
CCS
Lea Salome Brugger, Laura Kovács, Anja Petkovic Komel, Sophie Rain, Michael Rawson
2023 J jnl
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model.
CoRR
Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson
2023 — conf
Embedding the Connection Calculus in Satisfiability Modulo Theories.
AReCCa@TABLEAUX
Clemens Eisenhofer, Laura Kovács, Michael Rawson
2023 B conf
Lemmas: Generation, Selection, Application.
TABLEAUX
Michael Rawson, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel
2023 J jnl
Lemmas: Generation, Selection, Application.
CoRR
Michael Rawson, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel
2023 B conf
Non-Classical Logics in Satisfiability Modulo Theories.
TABLEAUX
Clemens Eisenhofer, Ruba Alassaf, Michael Rawson, Laura Kovács
2023 A conf
SAT-Based Subsumption Resolution.
CADE
Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath
2023 A conf
Superposition with Delayed Unification.
CADE
Ahmed Bhayat, Johannes Schoisswohl, Michael Rawson
2022 — conf
Reuse of Introduced Symbols in Automatic Theorem Provers (short paper).
PAAR@IJCAR
Michael Rawson, Martin Suda, Petra Hozzová, Giles Reger
2022 B conf
The Rapid Software Verification Framework.
FMCAD
Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovács, Giles Reger
2022 — conf
The Vampire Approach to Induction (short paper).
PAAR@IJCAR
Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov
2021 B conf
A Multithreaded Vampire with Shared Persistent Grounding.
FMCAD
Michael Rawson, Giles Reger
2021 B conf
Eliminating Models During Model Elimination.
TABLEAUX
Michael Rawson, Giles Reger
2021 — conf
On Evaluating Theorem Provers.
ARCADE@CADE
Michael Rawson, Giles Reger
2021 B conf
lazyCoP: Lazy Paramodulation Meets Neurally Guided Search.
TABLEAUX
Michael Rawson, Giles Reger
2020 — conf
Directed Graph Networks for Logical Reasoning (Extended Abstract).
PAAR+SC²@IJCAR
Michael Rawson, Giles Reger
2019 — conf
A Neurally-Guided, Parallel Theorem Prover.
FroCos
Michael Rawson, Giles Reger
2019 A conf
Old or Heavy? Decaying Gracefully with Age/Weight Shapes.
CADE
Michael Rawson, Giles Reger
2018 — conf
Dynamic Strategy Priority: Empower the Strong and Abandon the Weak.
PAAR@FLoC
Michael Rawson, Giles Reger