Non-Termination Proving: 100 Million LoC and Beyond

## Контекст В современной программной инженерии становится все важнее обеспечивать надежность и стабильность больших программных систем. Одной из сложных проблем, с которой сталкиваются разработчики, является поиск места неограниченного выполнения программы (неотмененность). Традиционные подходы к этой задаче либо неэффективны, либо неточны при работе с масштабными кодовыми базами, где количество строк кода достигает миллионов. Недостаточное обнаружение неотмененности может привести к серьезным проблемам, таким как потребление неограниченных ресурсов, сбои в системах и даже критические сбои в критически важных приложениях. Необходимо разработать новые методы, позволяющие эффективно и аккуратно обнаруживать неотмененность в больших кодовых базах. ## Метод Наше исследование основывается на использовании прообразных техник для доказательства неотмененности в программах. Мы реализовали наш подход в инструменте Pulse Infinite, который работает на основе **композиционной** и **под-представительской** методологии. **Композиционная** методология позволяет разбивать программу на меньшие компоненты, что упрощает обработку и увеличивает масштабность. **Под-представительская** техника гарантирует, что результаты доказательства неотмененности являются точными, даже при ограниченном представлении программы. Мы применяем Pulse Infinite к более чем 100 миллионам строк кода (LoC), написанных на языках C, C++ и Hack, чтобы определить возможные места неотмененности. Это позволяет использовать инструмент в реальных программных системах, где традиционные подходы не могут быть применены с достаточной точностью. ## Результаты Мы применили Pulse Infinite к более чем 100 миллионам строк кода, составляющих программные системы, написанные на C, C++ и Hack. Инструмент смог обнаружить более 30 новых мест неотмененности, которые ранее не были обнаружены любыми другими методами. Это приводит к улучшению **стандарта золота** в области обнаружения неотмененности в больших кодовых базах. Эксперименты показали, что Pulse Infinite эффективно обнаруживает проблемы, которые могут привести к неограниченному выполнению программ, даже в условиях огромных кодовых баз. Эти результаты демонстрируют значительное потенциал инструмента для применения в промышленных системах. ## Значимость Проблема неотмененности является критической для многих областей, где необходимо обеспечивать надежность и эффективность программ. Наш инструмент Pulse Infinite может использоваться в сферах, таких как финансовые системы, космическая отрасль, автоматизированные системы, где недостаточное обнаружение неотмененности может привести к критическим потерям. Одним из основных преи