Ultimate GemCutter and the Axes of Generalization
Dominik Klumpp, Daniel Dietsch, Matthias Heizmann, Frank Schüssele, Marcel Ebbinghaus, Azadeh Farzan, Andreas Podelski
Abstract
Abstract 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.
Topics & Concepts
GeneralizationCorrectnessComputer scienceCounterexampleSpurious relationshipConcurrencyInterpolation (computer graphics)Theoretical computer scienceAlgorithmProgramming languageArtificial intelligenceDiscrete mathematicsMathematicsMachine learningImage (mathematics)Mathematical analysisFormal Methods in VerificationSecurity and Verification in ComputingLogic, programming, and type systems