Faculty Research & Scholarly Work
Enabling Developers to Write Provably Correct Software
Computer code is the foundation of today’s
Shaping Artificial Intelligence through the Humanities and Social Sciences Artificial Intelligence (AI) is making a profound impact on how society functions, affecting our civil liberties, safety and security, health care and learning. Dietrich College launched a new AI website to show how the college’s researchers and scholars are applying and influencing AI where humanity and technology meet.
technology. As software becomes an increasingly pervasive part of our lives, we need ways to ensure that critical software systems remain free of certain classes of defects and vulnerabilities.
Jeremy Avigad , a professor in the Philosophy Department, is part of a team of CMU researchers that received a Defense Advanced Research Projects Agency (DARPA) research grant from the Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) program to make it possible for non-experts to formally prove that their code is correct, reliable and secure. The researchers are developing a tool called Verus for mathematically proving the correctness, reliability and security of code written in the Rust programming language. To discharge those proofs, Verus uses various reasoning engines, including the Lean theorem prover and Satisfaction Modulo Theory (SMT) solvers.
VISIT DIETRICH COLLEGE’S AI WEBSITE
25
2024 YEAR IN REVIEW
Made with FlippingBook Digital Publishing Software