In computer science, specifically software engineering and hardware engineering, Formal Methods are a particular kind of mathematically rigorous techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages, automata theory, discrete event dynamic system and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification.
—Wikipedia, “Formal methods“
Verified AI is the goal of achieving strong, ideally provable assurances of correctness and trustworthiness of AI systems with respect to mathematically specified requirements. Five challenge areas for verified AI: Environment modelling, Formal specification, Modeling learning systems, Scalable formal engines, and Correct-by-construction design.
Toward Verified Artificial Intelligence Read More
“Light Blue Touchpaper” is the blog of the University of Cambridge Computer Laboratory and is written by researchers in the Security Group. Read here brief and timely essays on recent developments and topics related to computer security.
Light Blue Touchpaper Read More