Automatically testing string solvers
Alexandra Bugariu, Péter Müller
Abstract
SMT solvers are at the basis of many applications, such as program verification, program synthesis, and test case generation. For all these applications to provide reliable results, SMT solvers must answer queries correctly. However, since they are complex, highly-optimized software systems, ensuring their correctness is challenging. In particular, state-of-the-art testing techniques do not reliably detect when an SMT solver is unsound.
Topics & Concepts
Computer scienceCorrectnessProgramming languageSatisfiability modulo theoriesSolverString (physics)Software testingSoftwareSoftware engineeringTheoretical computer sciencePhysicsQuantum mechanicsSoftware Testing and Debugging TechniquesSoftware Reliability and Analysis ResearchSoftware Engineering Research