These papers introduce sequential functions for specifying digital systems like operating systems and networks. The mathematical basis comes from Moore machines, Moore machine products, and
Read more
A claimed validated operating system.
The claim: we have demonstrated the comprehensive formal verification of the seL4 microkernel, with a complete proof chain from precise, formal statements of high-level security
Read moreState machines and circuits
The cross coupled latch is one of the greatest inventions of the 20th century State machine models of timing and circuit design
Read moreDijkstra versus Perlis (updated)
Dijkstra wrote: He [Perlis] published a very obnoxious paper arguing against a mathematical approach to programming cite The paper by De Millo, Lipton and Perlis starts as
Read more