Ultimate GemCutter and the Axes of Generalization (Competition Contribution)

Dominik Klumpp,Daniel Dietsch,Matthias Heizmann,Frank Schuessele, Marcel Ebbinghaus,Azadeh Farzan,Andreas Podelski

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT II（2022）

引用 6|浏览31

暂无评分

摘要

ULTIMATE GEMCUTTER verifies concurrent programs using the CEGAR paradigm, by generalizing from spurious counterexample traces to larger sets of correct traces. We integrate classical CEGAR generalization with orthogonal generalization across interleavings. Thereby, we are able to prove correctness of programs otherwise out-of-reach for interpolation-based verification. The competition results show significant advantages over other concurrency approaches in the ULTIMATE family.

查看译文

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要