Temporal Logic, Hardware Verification, and Automatic        Theorem Proving
{'Code': '05010400', 'Directorate': {'Abbreviation': 'CSE', 'LongName': 'Direct For Computer & Info Scie & Enginr'}, 'Division': {'Abbreviation': 'CCF', 'LongName': 'Division of Computing and Communication Foundations'}}
{'SignBlockName': 'name not available', 'PO_EMAI': None, 'PO_PHON': None}
This work comprises several research projects in logics of programs and         program verification.  All of the projects are directed towards                 providing tools that will make automatic verification feasible for a            wider class of programs.                                                                                                                                        The first three projects involve an approach to verifying finite state          concurrent systems called temporal logic model checking.  This                  procedure will determine if a finite-state concurrent system satisfies          its specification in a propositional temporal logic by methodically             searching the global state graph generated by the concurrent system.            It has been used successfully to find subtle errors in published                designs of tricky self-timed circuits.  The first project is to develop         ways of handling the state explosion problem that may occur with this           type of verification.  Another project is to extend the temporal logic          and its verification procedure to allow operators defined by automata           on infinite tapes.  This is of practical importance since a frequent            criticism of temporal logic is its expressive power compared to                 automata.  The third project involves actually using model checking             techniques for the automatic verification of hardware controllers.  The         main problem in this case is to develop methods of extracting state             machines from circuits under realistic timing models.                                                                                                           The last project is the development of a parallel resolution theorem            prover to run on Sequent and Encore multiprocessors.  It is already             well underway.  Since interest primarily in problems caused by                  concurrency, one can use a fairly simple theorem proving strategy based         on linear resolution/model elimination.  Clauses are maintained                 according to some heuristic function in a heap data structure that              permits parallel inserts and deletions.  A prototype implementation of          the full system should be running in the next few months.  Experiments          with other ways of organizing the theorem prover and with more                  complicated theorem proving strategies will follow.
{'FirstName': 'Edmund', 'LastName': 'Clarke', 'PI_MID_INIT': 'M', 'PI_SUFX_NAME': 'Jr.', 'PI_FULL_NAME': 'Edmund M Clarke', 'EmailAddress': 'emc@cs.cmu.edu', 'NSF_ID': '000240921', 'StartDate': '03/01/1988', 'EndDate': None, 'RoleCode': 'Principal Investigator'}
{'Name': 'Carnegie-Mellon University', 'CityName': 'PITTSBURGH', 'ZipCode': '152133815', 'PhoneNumber': '4122688746', 'StreetAddress': '5000 FORBES AVE', 'StreetAddress2': None, 'CountryName': 'United States', 'StateName': 'Pennsylvania', 'StateCode': 'PA', 'CONGRESSDISTRICT': '18', 'CONGRESS_DISTRICT_ORG': 'PA18', 'ORG_UEI_NUM': 'U3NKNFLNQ613', 'ORG_LGL_BUS_NAME': 'CARNEGIE MELLON UNIVERSITY', 'ORG_PRNT_UEI_NUM': 'U3NKNFLNQ613'}
{'Name': None, 'CityName': None, 'StateCode': None, 'ZipCode': None, 'StreetAddress': None, 'CountryCode': None, 'CountryName': None, 'StateName': None, 'CountryFlag': None, 'CONGRESSDISTRICT': None, 'CONGRESS_DISTRICT_PERF': '""'}
{'Code': '2875', 'Text': 'SYSTEM SOFTWARE'}
{'url': 'https://www.nsf.gov/awardsearch/download?DownloadFileName=1987&All=true', 'xml': '8722633.xml'}