{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T10:49:36Z","timestamp":1648896576752},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1993,6,1]],"date-time":"1993-06-01T00:00:00Z","timestamp":738892800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1993,6]]},"DOI":"10.1007\/bf01384134","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T06:04:39Z","timestamp":1112421879000},"page":"259-276","source":"Crossref","is-referenced-by-count":5,"title":["A unified framework for describing and verifying hardware synchronous sequential systems"],"prefix":"10.1007","volume":"2","author":[{"given":"Ghislaine","family":"Thuau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bachir","family":"Berkane","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"O. Coudert, C. Berthet, and J.C. Madre. Verification of sequential machines using boolean functional vectors. In Proc. of the IFIP International Workshop, Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, 1989."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"A. Ghosh, S. Devadas, and A.R. Newton. Verification of interacting sequential circuits. In 27th ACM\/IEEE Design Automaton Conference, Orlando, 1990.","DOI":"10.1145\/123186.123260"},{"key":"CR3","volume-title":"Workshop on Designing Correct Circuits","author":"G. Thuau","year":"1990","unstructured":"G. Thuau and D. Pilaud. Using the declarative language Lustre for circuit verification. In Workshop on Designing Correct Circuits, Springer-Verlag Publisher, Oxford, England, 1990."},{"key":"CR4","unstructured":"S. Burch, E.M. Clarke, and K.L. McMillan. Symbolic model checking: 1020 States and Beyond. In Proc. of LICS, 1990."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"G.V. Bochmann. Hardware specification with temporal logic: An example. InIEEE Transactions on Computers, c-31, n(3): 1982.","DOI":"10.1109\/TC.1982.1675978"},{"key":"CR6","unstructured":"O. Coudert, and J.C. Madre. Verifying temporal properties of sequential circuits without building their state diagrams. InComputer-Aided Verification, E.M. Clarke and R.P. Kurshan, (eds.). DIMACS series, 1990."},{"key":"CR7","unstructured":"M. Fujita, and H. Fujisawa. Specification, verification and synthesis of control circuits with propositional temporal logic. In Proc. of the Ninth IFIP on CHDL, Washington, DC, 1989."},{"key":"CR8","unstructured":"Z. Ha?El, and R.P. Kurshan. Automatic verification of finite-state concurent systems. In Proc. of Workshop on Automatic Verification Methods for Finite-State Systems, Grenoble, France, 1989."},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"O. Coudert and J.C. Madre. A unified framework for the formal verification of sequential circuits. In Proc. of ICCAD, Santa Clara, 1990.","DOI":"10.1109\/ICCAD.1990.129859"},{"key":"CR10","volume-title":"V\u00e9rification des Syst\u00e8mes Mat\u00e9riels Num\u00e9riques S\u00e9quentiels Synchrones: Application du Language Lustre et de ?Outil de V\u00e9rification Lesar","author":"B. Berkane","year":"1992","unstructured":"B. Berkane.V\u00e9rification des Syst\u00e8mes Mat\u00e9riels Num\u00e9riques S\u00e9quentiels Synchrones: Application du Language Lustre et de ?Outil de V\u00e9rification Lesar Ph.D. thesis, Institut National Polytechnique de Grenoble, France, 1992."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language LUSTRE. InIEEE Special Issue on Synchronous Languages, 1992.","DOI":"10.1109\/5.97300"},{"key":"CR12","series-title":"Technical Report Spectre","volume-title":"On the verification of safety properties","author":"A. Bouajjani","year":"1990","unstructured":"A. Bouajjani, J.C. Fernandez, and N. Halbwachs On the verification of safety properties. Technical Report Spectre, IMAG, Grenoble, France, 1990."},{"key":"CR13","volume-title":"Compilation Efficace d'un Langage D\u00e9claratif Synchrone: le G\u00e9n\u00e9rateur de Code Lustre V3","author":"P. Raymond","year":"1991","unstructured":"P. Raymond.Compilation Efficace d'un Langage D\u00e9claratif Synchrone: le G\u00e9n\u00e9rateur de Code Lustre V3. Ph.D. thesis, Institut National Polytechnique de Grenoble, France, 1991."},{"key":"CR14","unstructured":"T.L. Booth.Sequential Machines and Automata Theory. Wiley, (ed.), New York, 1967."},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Caspi, D. Pilaud, F. Ouabdesselam, and A. C. Glory. Specifying, programming and verifying real-time systems, using a synchronous declarative language. In Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, Springer Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_18"},{"key":"CR16","unstructured":"C. Ratel.D\u00e9finition et R\u00e9alisation d'un outil de V\u00e9rification Formelle de Programmes Lustre: le Syst\u00e9me Lesar. Ph.D. thesis, Universit\u00e9 Joseph Fourier de Grenoble, 1992."},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"K.J. Supowit, S.J. Friedman. A new method for verifying sequential circuits. In Proc. of the 23rd Design Automation Conference, 1986.","DOI":"10.1109\/DAC.1986.1586089"},{"key":"CR18","unstructured":"A. Bouajjani, J.C. Fernandez, and N. Halbwachs. Minimal state graph generation. InDIMACS Series in Discrete Mathematics and Theorical Computer Science, 3, 1990."},{"key":"CR19","series-title":"Technical Report","volume-title":"Extraction des propri\u00e9t\u00e9s temporelles d'un chronogramme","author":"B. Berkane","year":"1992","unstructured":"B. Berkane, and G. Thuau. Extraction des propri\u00e9t\u00e9s temporelles d'un chronogramme. Technical Report, IMAG, Grenoble, 1992."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384134.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384134\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384134","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:30:01Z","timestamp":1586190601000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384134"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,6]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993,6]]}},"alternative-id":["BF01384134"],"URL":"https:\/\/doi.org\/10.1007\/bf01384134","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,6]]}}}