Connecting concrete and abstract programs

• Validating Traces of Distributed Programs Against TLA+ Specifications⋆ - Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, Stephan Merz
• Verifying Software Traces Against a Formal Specification with TLA+ and TLC -- Ron Pressler
• Validating Traces of Distributed Systems Against TLA+ Specifications -- Stephan Merz
• Никита Синяченко, Евгений Чернацкий — TLA+ для эффективного тестирования распределенных систем, Video, Source code
• Model Checking Cache Coherence in System-Level Code - Nicholas Allen and Yang Zhao, Oracle Labs Brisbane, June 2016 PDF
• Modelator is a tool that enables automatic generation of tests from models. Modelator takes TLA+ models as its input and generates tests that can be executed against an implementation of the model.
• Kayfabe: Model-based program testing with TLC - Star Dorminey, Video, PDF
• Интеграция мандатного и ролевого управления доступом и мандатного контроля целостности в верифицированной иерархической модели безопасности операционной системы -- П. Н. Девянин, В. В. Кулямин, А. К. Петренко, А. В. Хорошиловe, И. В. Щепетков
• Model Checking Guided Testing for Distributed Systems