{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:14:24Z","timestamp":1754482464211},"publisher-location":"Berlin\/Heidelberg","reference-count":13,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540544771"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0023716","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T06:01:03Z","timestamp":1132380063000},"page":"23-32","source":"Crossref","is-referenced-by-count":13,"title":["Verifying temporal properties of sequential machines without building their state diagrams"],"prefix":"10.1007","author":[{"given":"Olivier","family":"Coudert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean Christophe","family":"Madre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Berthet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"J. P. Billon, \u201cPerfect Normal Forms for Discrete Functions\u201d, BULL Research Report N o87019, 1987."},{"key":"4_CR2","unstructured":"J. P. Billon, J. C. Madre, \u201cOriginal Concepts of PRIAM, an Industrial Tool for Efficient Formal Verification of Combinational Circuits\u201d, in The Fusion of Hardware Design and Verification, G. J. Milne Ed., North Holland, 1988."},{"key":"4_CR3","unstructured":"S. Bose, A. Fisher, \u201cAutomatic Verification of Synchronous Circuits Using Symbolic Logic Simulation and Temporal Logic\u201d, in Proc. of the IFIP Int. Workshop, Applied Formal Methods for Correct VLSI Design, Leuven, Nov. 1989."},{"key":"4_CR4","unstructured":"A. Bouajjani, J. C. Fernandez, N. Halbwachs, \u201cAn Executable Temporal Logic for Expressing Safety Properties\u201d, July 1990."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, \u201cGraph-based Algorithms for Boolean Functions Manipulation\u201d, IEEE Transaction on Computers, Vol C35 No8, 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"S. Burch, E. M. Clarke, K. L. McMillan, \u201cSequential Circuit Verification Using Symbolic Model Checking\u201d, in Proc. of Design Automation Conference (DAC), Orlando FL, USA, July 1990.","DOI":"10.1145\/123186.123223"},{"key":"4_CR7","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1146\/annurev.cs.02.060187.001413","volume":"2","author":"E. M. Clarke","year":"1987","unstructured":"E. M. Clarke, O. Grumbreg, \u201cResearch on Automatic Verification of Finite-State Concurrent Systems\u201d, Annual Revue Computing Science, vol. 2, pp 269\u2013290, 1987.","journal-title":"Annual Revue Computing Science"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, J. C. Madre, \u201cVerification of Synchronous Sequential Machines Based on Symbolic Execution\u201d, in Lecture Notes in Computer Science: Automatic Verification Methods for Finite State Systems, Volume 407, J. Sifakis Editor, Springer-Verlag, pp 365\u2013373, June 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"4_CR9","unstructured":"O. Coudert, C. Berthet, J. C. Madre, \u201cVerification of Sequential Machines Using Boolean Functional Vectors\u201d, in Proc. of the IFIP Int. Workshop, Applied Formal Methods for Correct VLSI Design, Leuven, November 1989."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, J. C. Madre, \u201cFormal Boolean Manipulations for the Verification of Sequential Machines\u201d, in Proc. of the First European Design Automation Conference (EDAC), Glasgow, March 1990.","DOI":"10.1109\/EDAC.1990.136620"},{"key":"4_CR11","unstructured":"G. J. Holtzman, \u201cAlgorithms for Automated Protocol Validation\u201d, in Lecture Notes in Computer Science: Automatic Verification Methods for Finite State Systems, Volume 407, J. Sifakis Editor, Springer-Verlag, June 1989."},{"key":"4_CR12","unstructured":"Z. Kovahi, Switching and Finite Automata Theory, McGraw-Hill Book Edition, 1978."},{"key":"4_CR13","unstructured":"J. P. Queille, J. Sifakis, \u201cFairness and Related Properties in Transition Systems\u201d, Acta Informatica, pp 195\u2013220, 1983."}],"container-title":["Lecture Notes in Computer Science","Computer-Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0023716.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:50:13Z","timestamp":1607550613000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0023716"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540544771"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0023716","relation":{},"subject":[]}}