Linear-time temporal logic guided greybox fuzzing
Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, Abhik Roychoudhury
2022Proceedings of the 44th International Conference on Software Engineering29 citationsDOIOpen Access PDF
Abstract
Software model checking as well as runtime verification are verification techniques which are widely used for checking temporal properties of software systems. Even though they are property verification techniques, their common usage in practice is in "bug finding", that is, finding violations of temporal properties. Motivated by this observation and leveraging the recent progress in fuzzing, we build a greybox fuzzing framework to find violations of Linear-time Temporal Logic (LTL) properties.
Topics & Concepts
Fuzz testingComputer scienceLinear temporal logicTemporal logicModel checkingProgramming languageComputation tree logicSoftwareFormal verificationSoftware verificationProperty (philosophy)Software engineeringSoftware systemSoftware constructionEpistemologyPhilosophySoftware Testing and Debugging TechniquesFormal Methods in VerificationAdvanced Software Engineering Methodologies