{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:01:30Z","timestamp":1729641690566,"version":"3.28.0"},"reference-count":53,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1109\/memcod.2003.1210081","type":"proceedings-article","created":{"date-parts":[[2004,1,23]],"date-time":"2004-01-23T23:33:03Z","timestamp":1074900783000},"page":"3-9","source":"Crossref","is-referenced-by-count":1,"title":["Executable computational logics: combining formal methods and programming language based system design"],"prefix":"10.1109","author":[{"given":"J.","family":"Meseguer","sequence":"first","affiliation":[]}],"member":"263","reference":[{"key":"ref39","first-page":"275","article-title":"General logics","author":"meseguer","year":"1989","journal-title":"Logic Colloquium'87"},{"key":"ref38","article-title":"Microprocessor specification in Hawk","author":"matthews","year":"1988","journal-title":"Proceedings of the International Conference on Computer Languages"},{"journal-title":"Computer-Aided Reasoning An Approach","year":"2000","author":"kaufmann","key":"ref33"},{"journal-title":"Computer-Aided Reasoning ACL2 Case Sudies","year":"2000","author":"kaufmann","key":"ref32"},{"key":"ref31","article-title":"Stochastic process algebras: A new approach to performance modeling","author":"hillston","year":"1998","journal-title":"Systems Modeling and Computer Simulation"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569951"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00357-7"},{"key":"ref36","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/3-540-65306-6_17","article-title":"Petri nets in performance analysis: An introduction","volume":"1491","author":"marsan","year":"1998","journal-title":"Lecture Notes in Computer Science Lectures on Petri Nets I Basic Models"},{"key":"ref35","first-page":"36","article-title":"Stochastic Petri nets: An elementary intro-duction","volume":"424","author":"marsan","year":"1990","journal-title":"Advances in Petri Nets 1989 Lecture Notes In Computer Science"},{"key":"ref34","article-title":"Probabilistic rewrite theories: Unifying models, logics and tools","author":"kumar","year":"2003","journal-title":"Manuscript"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2001.989799"},{"key":"ref27","first-page":"128","article-title":"Verifying a simple pipe lined microprocessor using Maude","author":"harman","year":"2001","journal-title":"Recent Trends in Algebraic Development Techniques volume 2267 of Lecture Notes in Computer Science"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_24"},{"key":"ref2","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","article-title":"Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems","author":"alur","year":"1993","journal-title":"Workshop on Theory of Hybrid Systems"},{"key":"ref1","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","article-title":"Verifying continuous-time Markov chains","volume":"1102","author":"aziz","year":"1996","journal-title":"Eighth International Conference on Computer Aided Verification CAV"},{"journal-title":"Formal Foundations for the Design of Rasteri-ration Algorithms and Architectures","year":"1990","author":"eker","key":"ref20"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3544-9_13"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44881-0_3"},{"journal-title":"CafeOBJ Report","year":"1998","author":"futatsugi","key":"ref24"},{"journal-title":"Report on the programming language Haskell Technical report","year":"1990","key":"ref23"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3658-0_5"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6541-0_2"},{"key":"ref51","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1007\/3-540-56863-8_61","article-title":"Interval timed coloured Petri nets and their analysis","author":"van der aalst","year":"1993","journal-title":"Application and Theory of Petri Nets 1993"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00366-8"},{"journal-title":"Rewriting Logic as a Semantic Framework for Modular Structural Operational Semantics","year":"2001","author":"verdejo","key":"ref52"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44881-0_15"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450556-9\/50061-7"},{"key":"ref14","first-page":"165","article-title":"Temporal logics for the specification of perfor-mance and reliability","author":"de alfaro","year":"1997","journal-title":"Symposium on Theoretical Aspects of Computer Science"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"ref16","article-title":"Coherence checker and completion tools for Maude specifications","author":"dur\u00e1n","year":"2000","journal-title":"Manuscript Computer Science Lab-oratory SRI International"},{"key":"ref17","article-title":"Termination checker and Knuth-Bendix completion tools for Maude equational specifications","author":"dur\u00e1n","year":"2000","journal-title":"Manuscript Computer Science Lab-oratory SRI International"},{"key":"ref18","article-title":"A Church-Rosser checker tool for Maude equational specifications","author":"dur\u00e1n","year":"2000","journal-title":"Manuscript Computer Science Lab-oratory SRI International"},{"key":"ref19","article-title":"The Maude LTL model checker","author":"eker","year":"2002","journal-title":"Proc 4th Int Workshop Rewriting Logic Its Applications"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"ref3","article-title":"The theory of timed automata","author":"alur","year":"1991","journal-title":"Real Time Theory in Practice volume 600 of Lecture Notes in Computer Science"},{"key":"ref6","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60692-0_70","article-title":"Model checking of probabilistic and nondeterministic systems","volume":"15","author":"bianco","year":"1995","journal-title":"FSTTCS Foundations of Software Technology and Theoretical Computer Science"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050046"},{"journal-title":"Maude como marco semántico ejecutable","year":"2003","author":"braga","key":"ref8"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00358-9"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_30"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_22"},{"journal-title":"Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic","year":"2000","author":"olveczky","key":"ref46"},{"key":"ref45","article-title":"Formal models of java at the jvm level- a survey from the ac12 perspective","author":"moore","year":"2002","journal-title":"Proc Workshop on Formal Techniques for Java Programs in association with ECOOP 2001"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00363-2"},{"key":"ref47","article-title":"Real-Time Maude: a tool for simulating and analyzing real-time and hybrid sys-tems","author":"olveczky","year":"2000","journal-title":"ENTCS"},{"key":"ref42","article-title":"Research directions in rewriting logic","author":"meseguer","year":"1997","journal-title":"Computational Logic NATO Advanced Study Institute"},{"key":"ref41","first-page":"18","article-title":"Membership algebra as a logical framework for equational specification","author":"meseguer","year":"1998","journal-title":"Proc WADT'97"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_2"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35520-7_5"}],"event":{"name":"2003 1st IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2003)","start":{"date-parts":[[2003,6,24]]},"location":"Mont Saint Michel, France","end":{"date-parts":[[2003,6,26]]}},"container-title":["First ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2003. MEMOCODE '03. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8593\/27232\/01210081.pdf?arnumber=1210081","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,9]],"date-time":"2018-04-09T00:55:01Z","timestamp":1523235301000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1210081\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"references-count":53,"URL":"https:\/\/doi.org\/10.1109\/memcod.2003.1210081","relation":{},"subject":[],"published":{"date-parts":[[2003]]}}}