Symbolic Execution in .NET

on YouTube ↗01h 01m

" summary

The talk explains symbolic execution for .NET, describing the theory behind Microsoft IntelliTest and showing how to use symbolic execution for test generation. It presents the V# symbolic virtual machine with examples, demonstrates using SMT solvers to encode and solve puzzles like Sudoku and Minesweeper, and discusses program synthesis as a coming change for software development.

AI-written summary · about

" chapters (7)

1. 0:00Introduction
2. 2:36Why generate tests
3. 11:25How symbolic execution works
4. 20:37Symbolic execution challenges
5. 32:13Using SMT solvers in practice
6. 42:07Sharp test generation engine
7. 50:46Future of symbolic execution

" related talks

• 18mSymbolic Execution Explained: Finding Bugs in Complex Code PathsTim Pohlmann · Sonar Summit 2026
• 20mDerivative-Guided Symbolic ExecutionJulia Belyakova, Zhe Zhou, Suresh Jagannathan, Yongwei Yuan · POPL 2025
• 34mSymbolic Execution for Randomized ProgramsSubhajit Roy, Justin Hsu, Sumit Lahiri, Zachary Susag · OOPSLA 2022
• 24mQSYM : A Practical Concolic Execution Engine Tailored for Hybrid FuzzingInsu Yun · USENIX Security '18
• 43mHydra's Heads – Dmitriy IvanovDmitriy Ivanov · Hydra 2022
• 42mJava debugging tips & tricksMartin Skarsaune · Oredev 2017
• 31mVerified Software at ScalePhilippa Gardner · O'Hearn Fest (POPL 2024)
• 43mOvercoming Broken Window Syndrome Code Verification Techniques for NET DevelopGael Fraiteur · Build Stuff 2024