Ruzica Piskac Research Group

Yale University

How can formal methods and automated reasoning improve software reliability and trustworthiness in real-world systems? The ROSE group develops program synthesis and software verification techniques using decision procedures and automated reasoning to certify program correctness. Researchers build tools and apply automated reasoning to software configuration, firewall repair, and synthesis of verifiable code snippets. Projects use theorem proving, SMT decision procedures, and synthesis pipelines to detect and repair software bugs and configuration errors. The group combines formal approaches with applied security and cryptography to prove properties of programs and protocols.