Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA
Felix A. Wolf, Malte Schwerhoff, Peter Müller
2021年份
10被引次数
7顶会引用
问问这篇 Paper
问问你的智能体。
Lune 读过与它相关的顶会 Paper，每个回答都会注明依据哪几篇。
引用它的顶会 Paper7
- Diaframe: automated verification of fine-grained concurrent programs in IrisIke Mulder, Robbert Krebbers, Herman GeuversPLDI 2022 · 被引用 27 次
- A concurrent program logic with a future and historyRoland Meyer, Thomas Wies, Sebastian WolffOOPSLA 2022 · 被引用 9 次
- Proof Automation for Linearizability in Separation LogicIke Mulder, Robbert KrebbersOOPSLA 2023 · 被引用 8 次
- A Proof Recipe for Linearizability in Relaxed Memory Separation LogicSunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung 等PLDI 2024 · 被引用 4 次
- Beyond Backtracking: Connections in Fine-Grained Concurrent Separation LogicIke Mulder, Lukasz Czajka, Robbert KrebbersPLDI 2023 · 被引用 2 次
相关 Paper
- QMaude: Quantitative Specification and Verification in Rewriting LogicRubén Rubio, Narciso Martí-Oliet, Isabel Pita, Alberto VerdejoFM 2023 · 被引用 11 次
- On Extending Incorrectness Logic with Backwards ReasoningFreek Verbeek, Md Syadus Sefat, Zhoulai Fu, Binoy RavindranPOPL 2025 · 被引用 1 次
- Formal Semantics and Formally Verified Validation for Temporal PlanningMohammad Abdulaziz, Lukas KollerAAAI 2022 · 被引用 4 次
- Verification of ORM-based Controllers by Summary InferenceGeetam Chawla, Navneet Aman, Raghavan Komondoor, Ashish Bokil 等ICSE 2022 · 被引用 2 次
- Verifying Secure Speculation in Isabelle/HOLMatt Griffin, Brijesh DongolFM 2021 · 被引用 6 次
