C S 430

Formal Specification

Construct formal specifications for complex computer systems using mathematical logic. This rigorous process is intellectually enlarging, as it requires students to translate abstract requirements into precise, unambiguous structures that reveal the fundamental nature of a system.

Property Verification

Use formal verification tools to prove critical properties and invariants of system specifications. This pursuit of absolute correctness is spiritually strengthening, as it teaches students to value and seek after provable truths that mirror the consistency of divine laws.

Verification Toolsets

Apply a diverse range of automated tools, such as Model Checkers, SAT solvers, SMT solvers, and Theorem Provers, to identify system vulnerabilities. Mastering these advanced instruments is character building, requiring the patience and meticulous attention to detail necessary to ensure that mission-critical systems are truly safe and reliable.

Correctness and Stewardship

Evaluate the correctness of digital infrastructures to prevent catastrophic failures in real-world applications. Developing the ability to verify that a system does exactly what it is intended to do is a form of stewardship, preparing students for a life of service where they protect the welfare and security of their communities.