Ultimate Taipan and Race Detection in Ultimate
Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schüssele, Andreas Podelski
Abstract
Abstract Ultimate Taipan integrates trace abstraction with algebraic program analysis on path programs. Taipan supports data race checking in concurrent programs through a reduction to reachability checking. Though the subsequent verification is not tuned for data race checking, the results are encouraging.
Topics & Concepts
ReachabilityComputer scienceProgramming languageModel checkingTRACE (psycholinguistics)AbstractionRace (biology)Reduction (mathematics)Theoretical computer scienceMathematicsPhilosophyEpistemologyBotanyGeometryBiologyLinguisticsFormal Methods in VerificationDistributed systems and fault toleranceLogic, programming, and type systems