Robert Shostak

Robert Eliot Shostak (born July 26, 1948, in Arlington, Virginia) is an American computer scientist and Silicon Valley entrepreneur.

As part of his senior dissertation work, he designed and built one of the earliest personal computers using discrete RTL logic (microprocessors were not yet available) and a magnetic core memory.

Much of his work there focused on automated theorem proving, and specifically on the development of decision procedure algorithms [5][6][7][8][9] for mechanized proof of the kinds of mathematical formulas that occur frequently in the formal verification of correctness of computer programs.

[10] In collaboration with CSL's Richard L. Schwartz and P. Michael Melliar-Smith, Shostak implemented a semi-automatic theorem prover incorporating some of these decision procedures.

Perhaps Shostak's most notable academic contribution is to have originated the branch of distributed computing known as Byzantine fault tolerance, also called interactive consistency.

The collective results were published in 1979 in the seminal paper, Reaching Agreement in the Presence of Faults,[14] which was awarded the 2005 Edsger W. Dijkstra Prize in Distributed Computing, as well as the 2013 Jean-Claude Laprie Award[13] The same authors helped to popularize the interactive consistency problem in their 1982 paper, The Byzantine Generals Problem,[15] which presents it in the form of a colorful allegory proposed by Lamport.

In the allegory, the computers are replaced by Byzantine generals who needed to coordinate the timing of an attack on an enemy by exchanging messages borne by couriers.

The work on Byzantine agreement has spawned an entire sub-field of distributed computing with hundreds of published papers exploring extensions and applications of the original results.