С*: Унификация программирования и проверки в рамках С

Компьютерные науки > Языки программирования [представлены 3 апреля 2025 года] Название: C*: Унифицированное программирование и проверка в C View PDF HTML (экспериментальное) резюме: Обеспечение правильной функциональности системного программного обеспечения с учетом его критического и низкоуровневого характера является одним из главных направлений официальных исследований по проверке и приложений. Несмотря на достижения в области средств проверки, традиционные программисты редко участвуют в проверке своих собственных кодов, что ведет к увеличению расходов на разработку и техническое обслуживание проверенного программного обеспечения. Одним из ключевых препятствий для участия программистов в практике проверки является разрыв между условиями и парадигмами, связанными с разработкой программ и проверкой, что ограничивает доступность и проверку в режиме реального времени. Мы представляем С*, интегрированный в доказательства языковой дизайн для программ С. C* расширяет C с помощью проверочных возможностей, приводимых в движение двигателем символического исполнения и ядром в виде КЖК. Она позволяет осуществлять проверку в реальном масштабе времени, позволяя программистам устанавливать блоки с кодом ввода доказательств и содействовать интерактивному обновлению текущего состояния доказательства. Его экспрессивная и широкораспространимая поддержка позволяет пользователям создавать многоразовые библиотеки логических определений, теорем и программируемой автоматизации доказательств.…