Zobrazeno 1 - 10
of 61
pro vyhledávání: '"Carl-Johan H. Seger"'
Autor:
Carl-Johan H. Seger
Publikováno v:
Formal Methods ISBN: 9783030908690
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::89e8d819ad9cc14e4a27e02c49446959
https://doi.org/10.1007/978-3-030-90870-6_38
https://doi.org/10.1007/978-3-030-90870-6_38
Publikováno v:
MEMOCODE
The Internet of Things (IoT) conceives a future where "things" are interconnected by means of suitable information and communication technologies. Unfortunately, recent events have demonstrated the high vulnerability of IoT. One of the main reasons f
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::49ab5eaf6f1390482145b9bbbf1715f2
https://doi.org/10.1109/memocode51338.2020.9315094
https://doi.org/10.1109/memocode51338.2020.9315094
Publikováno v:
MEMOCODE
Finite state machines (FSMs) are at the heart of many digital circuits, in particular microprocessors such as the IoT-oriented Cephalopode processor we are implementing as part of the Octopi project.We frequently encounter two practical difficulties
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e0f4849522df72671cc94a6c035758fc
https://doi.org/10.1109/memocode51338.2020.9315130
https://doi.org/10.1109/memocode51338.2020.9315130
Autor:
Tanmay Haldankar, Dinesh Chhatani, Zurab Khasidashvili, Rakesh Mistry, Carl-Johan H. Seger, Rajkumar Gajavelly, Supratik Chakraborty
Publikováno v:
Formal Methods in System Design. 50:317-352
Symbolic trajectory evaluation (STE) is a model checking technique that has been successfully used to verify many industrial designs. Existing implementations of STE reason at the level of bits, allowing signals in a circuit to take values from a lat
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c7bf08bf618cefb0eb5081af648f462c
https://doi.org/10.1007/s10703-017-0268-9
https://doi.org/10.1007/s10703-017-0268-9
Autor:
Bryant, Randal, Carl-Johan H. Seger
Symbolic trajectory evaluation is a new approach to formal hardware verification combining the circuit modeling capabilities of symbolic logic simulation with some of the analytic methods found in temporal logic model checkers. We have created such a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0428b666a0a4cd63cb8a0f3732a8c6fb
Practical application of formal methods requires more than advanced technology and tools; it requires an appropriate methodology. A verification methodology for data-path-dominated hardware combines model checking and theorem proving in a customizabl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::39ba61a2e0385db45612ee81ac1712e8
https://ora.ox.ac.uk/objects/uuid:c49b364a-8fe1-411e-8cad-930e3ab1a33a
https://ora.ox.ac.uk/objects/uuid:c49b364a-8fe1-411e-8cad-930e3ab1a33a
Autor:
Mark D. Aagaard, Don Syme, Tom Melham, Carl-Johan H. Seger, John O'Leary, Robert B. Jones, Clark Barrett
The Forte formal verification environment for datapath-dominated hardware is described. Forte has proven to be effective in large-scale industrial trials and combines an efficient linear-time logic model-checking algorithm, namely the symbolic trajec
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c1738cf6c88f2bf502b23532f5950857
https://doi.org/10.1109/tcad.2005.850814
https://doi.org/10.1109/tcad.2005.850814
Autor:
Jin Yang, Carl-Johan H. Seger
Publikováno v:
ICCD
Symbolic trajectory evaluation (STE) is a lattice-based model checking technology that uses a form of symbolic simulation. It offers an alternative to 'classical' symbolic model checking that, within its domain of applicability, often is much easier
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6220b98cefaf6e1948f3a794076de9bd
https://doi.org/10.1109/tvlsi.2003.812320
https://doi.org/10.1109/tvlsi.2003.812320
Autor:
Rakesh Mistry, Zurab Khasidashvili, Tanmay Haldankar, Rajkumar Gajavelly, Dinesh Chhatani, Supratik Chakraborty, Carl-Johan H. Seger
Publikováno v:
Computer Aided Verification ISBN: 9783319216676
CAV (2)
CAV (2)
Symbolic trajectory evaluation (STE) is a model checking technique that has been successfully used to verify industrial designs. Existing implementations of STE, however, reason at the level of bits, allowing signals to take values in \(\{0, 1, X\}\)
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::38390e8d6e06293e4e92ea7dc56764a9
https://doi.org/10.1007/978-3-319-21668-3_8
https://doi.org/10.1007/978-3-319-21668-3_8