| 词条 | Robert Shostak |
| 释义 |
| name = Robert E. Shostak | image = Robert-shostak-2019-thumbnail.jpg | image_size = | alt = | caption = | birth_date = | birth_place = Arlington County, Virginia | death_date = | death_place = | residence = Portola Valley, California | citizenship = United States | nationality = American | fields = Computer Science | workplaces = | alma_mater = A.B., A.M., Ph.D. Harvard | doctoral_advisor = | academic_advisors = | doctoral_students = | notable_students = | known_for = {{Plainlist|
| author_abbrev_bot = | author_abbrev_zoo = | influences = | influenced = | awards = {{Plainlist|
| signature = | signature_alt = | footnotes = | spouse = | module = }} Robert Eliot Shostak is an American computer scientist and Silicon Valley entrepreneur. He is most noted academically for his seminal work in the branch of distributed computing known as Byzantine Fault Tolerance. He is also known for co-authoring the Paradox Database, and most recently, the founding of Vocera Communications, a company that makes wearable, Star Trek-like communication badges. Shostak has authored more than forty academic papers and patents, and was editor of the 7th Conference on Automated Deduction. He has Erdős number 2 through his collaboration with Kenneth Kunen.[1] Shostak is a brother of Seth Shostak, who is Senior Astronomer at the SETI Institute and who frequently appears on television and radio. EducationRobert Shostak grew up in Arlington, Virginia. He studied mathematics and computer science at Harvard College, graduating in 1970 with high honors. 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.[2] He continued at Harvard to earn his A.M. degree and Ph.D. in Computer Science in 1974. While at Harvard he was awarded the Detur Book Prize, and fellowships from IBM and the National Science Foundation. CareerAfterwards, Shostak joined the research staff in the Computer Science Lab (CSL) at SRI International (formerly the Stanford Research Institute) in Menlo Park, California. Much of his work there focused on automated theorem proving, and specifically on the development of decision procedure algorithms [3][4][5][6][7] for mechanized proof of the kinds of mathematical formulas that occur frequently in the formal verification of correctness of computer programs.[8] 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.[9] The prover was used to verify correctness properties of an abstract specification of the SIFT (for Software Implemented Fault Tolerance) operating system and was later incorporated into SRIís Prototype Verification System. The work was published in the paper, SIFT: Design and analysis of a fault-tolerant computer for aircraft control[10] This paper was awarded the 2014 Jean-Claude Laprie Award in Dependable Computing[11] established by the IFIP Subgroup 10.4 on Dependable Computing. Interactive Consistency and Byzantine Fault TolerancePerhaps Shostak's most notable academic contribution is to have originated the branch of distributed computing known as Byzantine fault tolerance, also called interactive consistency. This work was also conducted in connection with the SIFT project at SRI. SIFT was conceived by John H. Wensley, who proposed using a network of general-purpose computers to reliably control an aircraft even if some of those computers were faulty. The computers would exchange messages as to the current time and state of the aircraft (each would have its own sensors and clock), and would thereby reach a consensus. At the outset, it was unknown how many computers would be necessary to reach consensus if some n of them were faulty, and possibly acting in a 'malicious' manner to thwart consensus. Shostak formalized the problem mathematically and proved that for n faulty computers, no fewer than 3n+1 computers in total were needed for any algorithm that could guarantee consensus, or what he termed interactive consistency. He also devised an algorithm for n = 1, proving that four computers were sufficient using two rounds of message passing. His colleague Marshall Pease then generalized the result by constructing an algorithm for 3n+1 computers that works for all n > 0, thus showing that 3n+1 are sufficient as well as necessary. Leslie Lamport later joined the CSL, and showed that if messages could be digitally signed, then only 3n are needed. The collective results were published in 1979 in the seminal paper, Reaching Agreement in the Presence of Faults,[12] which was awarded the 2005 Edsger W. Dijkstra Prize in Distributed Computing, as well as the 2013 Jean-Claude Laprie Award[11] The same authors helped to popularize the interactive consistency problem in their 1982 paper, The Byzantine Generals Problem,[13] 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 original formulation incorporated Albanian rather than Byzantine generals, but Jack Goldberg, the head of CSL, suggested that this might be interpreted as what might now be called cultural appropriation, hence the name was changed to Byzantine on the theory that this might be less likely to cause offense.) 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. One of the most interesting of these is in the implementation of blockchains, in which interactive consistency is sought among a distributed network of computers.[14] Blockchains underpin the integrity of cryptocurrencies such as Bitcoin. Entrepreneurial venturesIn 1984, Shostak and his colleague Richard Schwartz founded a Silicon Valley start-up company called Ansa Software. The company was financed by Ben Rosen of Sevin Rosen. Its product, a PC database called Paradox, was launched in 1985, and was among the first database products to run on IBM personal computers. Its user interface was based on Query by Example, a graphical method of formulating queries that had been conceived by Moshe Zloof at the IBM Watson Research Center. In September, 1987, Ansa Software was purchased by Borland International, which subsequently launched multiple Windows versions. A community of users still exists after more than thirty years. As of this writing, a third-party DOS version is still available for 64-bit Windows. Shostak is also founder of Vocera Communications, which he started in March, 2000. The product, which facilitates hands-free communication among members of teams in hospitals and other enterprises, features wearable, speech-enabled badges much like Star Trek Communication Badges.[15] The company went public in 2012 (NYSE:VCRA)[16] and has a market capitalization of close to $1B as of this writing. Shostak served as CTO and chief architect until he retired in 2013, and was a board member until the company IPO. Selected patents
References1. ^{{cite journal|author=W. W. Bledsoe|authorlink=|author2=Kenneth Kunen|author3=Robert E. Shostak|year=1985|title=Completeness Results for Inequality Provers|url=|journal=Artificial Intelligence|location=|publisher=|volume=27|issue=3|pages=255–288|doi=10.1016/0004-3702(85)90015-3|id=|accessdate=}} {{Authority control}}{{DEFAULTSORT:Shostak, Robert}}2. ^{{Cite web|url=http://id.lib.harvard.edu/alma/990039139110203941/catalog|title=SIC: a small inexpensive digital Computer|last=Shostak|first=Robert|date=1970|website=|archive-url=|archive-date=|dead-url=|access-date=}} 3. ^{{cite journal|author=Robert E. Shostak|authorlink=|year=1977|title=On the SUP-INF Method for Proving Presburger Formulas|url=|journal=Journal of the ACM|location=|publisher=|volume=24|issue=4|pages=529–543|doi=10.1145/322033.322034|id=|accessdate=}} 4. ^{{cite journal|author=Robert E. Shostak|authorlink=|year=1978|title=An Algorithm for Reasoning About Equality|url=|journal=Communications of the ACM|location=|publisher=|volume=21|issue=7|pages=583–585|doi=10.1145/359545.359570|id=|accessdate=}} 5. ^{{cite journal|author=Robert E. Shostak|authorlink=|year=1979|title=A Practical Decision Procedure for Arithmetic with Function Symbols|url=|journal=Journal of the ACM|location=|publisher=|volume=26|issue=2|pages=351–360|doi=10.1145/322123.322137|id=|accessdate=}} 6. ^{{cite journal|author=Robert E. Shostak|authorlink=|year=1981|title=Deciding Linear Inequalities by Computing Loop Residues|url=|journal=Journal of the ACM|location=|publisher=|volume=28|issue=4|pages=351–360|doi=|id=|accessdate=}} 7. ^{{cite journal|author=Robert E. Shostak|authorlink=|year=1984|title=Deciding Combinations of Theories|url=|journal=Journal of the ACM|location=|publisher=|volume=31|issue=1|pages=1–12|doi=10.1145/2422.322411|id=|accessdate=}} 8. ^{{Cite book|title=Mechanizing proof : computing, risk, and trust|last=A.|first=MacKenzie, Donald|date=2001|publisher=MIT Press|isbn=978-0262133937|location=Cambridge, Mass.|pages=268–272|oclc=45835532}} 9. ^{{Cite journal|last=Shostak|first=Robert E.|last2=Shostak|first2=Richard L.|last3=Melliar-Smith|first3=P. Michael|date=1982|editor-last=Loveland|editor-first=Donald|title=STP: A Mechanized Logic for Specification and Verifications|url=|journal=Proceeding of the 6th Conference on Automated Deduction|publisher=Springer, Berlin, Heidelberg|volume=|pages=32–49|via=}} 10. ^{{Cite journal|last=Wensley|first=John H.|last2=Lamport|first2=L.|last3=Goldberg|first3=J.|last4=Green|first4=M. W.|last5=Levitt|first5=K. N.|last6=Melliar-Smith|first6=P. M.|last7=Shostak|first7=R. E|last8=Weinstock|first8=C. B.|date=October 1978|editor5-last=|title=SIFT: Design and analysis of a fault-tolerant computer for aircraft control|url=|journal=Proceedings of the IEEE|volume=66|issue=10|pages=1240–1255|via=|doi=10.1109/PROC.1978.11114}} 11. ^1 {{Cite web|url=http://jclaprie-award.dependability.org/|title=The Jean-Claude Laprie Award|website=jclaprie-award.dependability.org|access-date=2019-02-21}} 12. ^{{cite journal|author=M. Pease|authorlink=|author2=R. Shostak|author3=L. Lamport|year=1979|title=Reaching Agreement in the Presence of Faults|url=|journal=Journal of the ACM|location=|publisher=|volume=27|issue=2|pages=228–234|doi=10.1145/322186.322188|id=|accessdate=|citeseerx=10.1.1.68.4044}} 13. ^{{cite journal|author=L. Lamport|authorlink=|author2=R. Shostak|author3=M. Pease|year=1982|title=The Byzantine Generals Problem|url=|journal=ACM Transactions on Programming Languages and Systems |location=|publisher=|volume=4|issue=1|pages=382–401|doi=10.1145/357172.357176|id=|accessdate=|citeseerx=10.1.1.64.2312}} 14. ^{{Cite book|title=Mastering blockchain : distributed ledgers, decentralization and smart contracts explained|last=Imran|first=Bashir|publisher=|isbn=9781787129290|location=Birmingham, UK|pages=12, 30|oclc=981928401|date = 2017-03-17}} 15. ^{{Cite news|url=https://www.forbes.com/2004/03/16/cx_ah_0316chips.html#4293808629d1|title=Your Trekkie Communicator is Ready|last=Hesseldahl|first=Arik|date=March 16, 2004|work=Forbes Magazine|access-date=}} 16. ^{{Cite journal|last=Gallagher|first=Dan|date=March 28, 2012|title=Vocera Communications jumps on IPO debut|url=https://www.marketwatch.com/story/vocera-communications-jumps-on-ipo-debut-2012-03-28|journal=MarketWatch|volume=|pages=|via=}} 8 : Harvard College alumni|American computer scientists|Dijkstra Prize laureates|Researchers in distributed computing|SRI International people|Formal methods people|Year of birth missing (living people)|Living people |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。