Parallel and distributed bounded model checking of multi-threaded programs
Omar Inverso, Catia Trubiani
Abstract
We introduce a structure-aware parallel technique for context-bounded analysis of concurrent programs. The key intuition consists in decomposing the set of concurrent traces into symbolic subsets that are separately explored by multiple instances of the same decision procedure running in parallel. The decision procedures work on different partitions of the search space without cooperating, whence distribution follows effortlessly. Our experiments on a selection of complex multi-threaded programs show significant analysis speedups and scalability, and greater performance gains than with general-purpose parallel solvers.
Topics & Concepts
Computer scienceScalabilityBounded functionConcurrencyParallel computingIntuitionTheoretical computer scienceModel checkingSet (abstract data type)Distributed computingProgramming languageMathematicsEpistemologyPhilosophyMathematical analysisDatabaseFormal Methods in VerificationSoftware Testing and Debugging TechniquesReal-Time Systems Scheduling