Model checking

There have been 1 topic suggestion tagged with model checking.

Related Tags

Talk Suggestions

Automated Verification of Computational Systems

It was realized in the 1960s that mathematical logic provides a suitable language to formulate properties of programs. This idea was formalized by Hoare who developed Hoare logic as a means to prove program correctness. However, this technique didn't apply directly to concurrent programs. An alternative approach called Temporal Logic was proposed by Amir Pneuli in 1977 which did provide a means to reason about concurrent programs. This topic studies this and then delves into the fundamental ideas behind model checking.

Required Background: Basics of computer science at the level of CS 146, Logic at the level of CS 245.

Possible reference materials for this topic include

Quick links: Google search, arXiv.org search, propose to present a talk

computer science logic model checking