{"data":{"id":"10.4121/21820458","type":"dois","attributes":{"doi":"10.4121/21820458","prefix":"10.4121","suffix":"21820458","identifiers":[],"alternateIdentifiers":[],"creators":[{"name":"Lathouwers, Sophie","nameType":"Personal","givenName":"Sophie","familyName":"Lathouwers","nameIdentifiers":[{"nameIdentifier":"0000-0002-7544-447X","nameIdentifierScheme":"https://orcid.org/"}],"affiliation":[]},{"name":"Armborst, Lukas","nameType":"Personal","givenName":"Lukas","familyName":"Armborst","nameIdentifiers":[{"nameIdentifier":"0000-0001-7565-0954","nameIdentifierScheme":"https://orcid.org/"}],"affiliation":[]},{"name":"Huisman, Marieke","nameType":"Personal","givenName":"Marieke","familyName":"Huisman","nameIdentifiers":[{"nameIdentifier":"0000-0003-4467-072X","nameIdentifierScheme":"https://orcid.org/"}],"affiliation":[]}],"titles":[{"title":"Specification Translator: Tool to Translate Specifications for Deductive Verifiers"}],"publisher":"4TU.ResearchData","container":{},"publicationYear":2023,"subjects":[{"subject":"Computer Software","subjectScheme":"Australian and New Zealand Standard Research Classification (ANZSRC), 2008","classificationCode":"0803"},{"subject":"FOS: Computer and information sciences","schemeUri":"http://www.oecd.org/science/inno/38235147.pdf","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"Information and Computing Sciences","subjectScheme":"Australian and New Zealand Standard Research Classification (ANZSRC), 2008","classificationCode":"08"},{"subject":"Deductive verification"},{"subject":"Specifications"},{"subject":"Annotations"},{"subject":"Specification languages"},{"subject":"Semantics"},{"subject":"Translation"}],"contributors":[{"name":"University Of Twente, Faculty Of Electrical Engineering, Mathematics And Computer Science (EEMCS), Formal Methods And Tools","nameType":"Organizational","affiliation":[],"contributorType":"Other","nameIdentifiers":[]}],"dates":[{"date":"2023-06-19","dateType":"Issued"}],"language":"en","types":{"ris":"COMP","bibtex":"misc","citeproc":"article","schemaOrg":"SoftwareSourceCode","resourceType":"Software","resourceTypeGeneral":"Software"},"relatedIdentifiers":[],"relatedItems":[],"sizes":[],"formats":["1) ZIP file that contains Scala files, Java files, Python scripts, text files, JAR file, 2) Markdown (md) file, 3) Virtual Machine in .ova format"],"version":"1","rightsList":[{"rights":"Creative Commons Attribution 4.0 International","rightsUri":"https://creativecommons.org/licenses/by/4.0/legalcode","schemeUri":"https://spdx.org/licenses/","rightsIdentifier":"cc-by-4.0","rightsIdentifierScheme":"SPDX"}],"descriptions":[{"description":"\u003cstrong\u003eAbout the Specification Translator\u003c/strong\u003eThe Specification Translator is a tool that has been implemented as part of our research titled \"Join Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation\". This tool will translate specifications in verified Java programs from one specification language into another. It supports the tools Krakatoa, OpenJML and VerCors.\u003cbr\u003eThe tool takes an annotated Java program and a target tool as input. It will then generate an annotated Java program where the annotations have been translated.\u003cbr\u003e\u003cstrong\u003eWhat's included in this artifact?\u003c/strong\u003eThis artifact contains the following things:- specification-translator.zip: A directory containing the Specification Translator tool as well as the examples used for the evaluation.- SpecTranslatorArtifact.ova: A Virtual Machine with the Specification Translator tool, as well as the OpenJML and VerCors verifiers. It also contains the examples used for the evaluation and a script to reproduce the evaluation.\u003cbr\u003eYou can use the Virtual Machine to reproduce the evaluation including verification after translation.If you just want to use the Specification Translator or have a look at the input/output files of the evaluation, then the zip file is sufficient.\u003cbr\u003e\u003cstrong\u003eLicense information\u003c/strong\u003eThe Specification Translator tool is shared under the CC-BY 4.0 license.The verifiers in the VM, as well as the examples and case studies used for the evaluation, are \u003cstrong\u003enot\u003c/strong\u003e licensed under the CC-BY 4.0 but under their original licenses which have been included.","descriptionType":"Abstract"}],"geoLocations":[],"fundingReferences":[{"awardTitle":"Mercedes: Maximal Reliability of Concurrent and Distributed Software","funderName":"Dutch Research Council","awardNumber":"639.023.710"}],"xml":"PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0iVVRGLTgiPz4KPHJlc291cmNlIHhtbG5zPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCIgeG1sbnM6eHNpPSJodHRwOi8vd3d3LnczLm9yZy8yMDAxL1hNTFNjaGVtYS1pbnN0YW5jZSIgeHNpOnNjaGVtYUxvY2F0aW9uPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCBodHRwOi8vc2NoZW1hLmRhdGFjaXRlLm9yZy9tZXRhL2tlcm5lbC00LjQvbWV0YWRhdGEueHNkIj4KICA8aWRlbnRpZmllciBpZGVudGlmaWVyVHlwZT0iRE9JIj4xMC40MTIxLzIxODIwNDU4PC9pZGVudGlmaWVyPgogIDxjcmVhdG9ycz4KICAgIDxjcmVhdG9yPgogICAgICA8Y3JlYXRvck5hbWUgbmFtZVR5cGU9IlBlcnNvbmFsIj5Tb3BoaWUgTGF0aG91d2VyczwvY3JlYXRvck5hbWU+CiAgICAgIDxnaXZlbk5hbWU+U29waGllPC9naXZlbk5hbWU+CiAgICAgIDxmYW1pbHlOYW1lPkxhdGhvdXdlcnM8L2ZhbWlseU5hbWU+CiAgICAgIDxuYW1lSWRlbnRpZmllciBuYW1lSWRlbnRpZmllclNjaGVtZT0iaHR0cHM6Ly9vcmNpZC5vcmcvIj4wMDAwLTAwMDItNzU0NC00NDdYPC9uYW1lSWRlbnRpZmllcj4KICAgIDwvY3JlYXRvcj4KICAgIDxjcmVhdG9yPgogICAgICA8Y3JlYXRvck5hbWUgbmFtZVR5cGU9IlBlcnNvbmFsIj5MdWthcyBBcm1ib3JzdDwvY3JlYXRvck5hbWU+CiAgICAgIDxnaXZlbk5hbWU+THVrYXM8L2dpdmVuTmFtZT4KICAgICAgPGZhbWlseU5hbWU+QXJtYm9yc3Q8L2ZhbWlseU5hbWU+CiAgICAgIDxuYW1lSWRlbnRpZmllciBuYW1lSWRlbnRpZmllclNjaGVtZT0iaHR0cHM6Ly9vcmNpZC5vcmcvIj4wMDAwLTAwMDEtNzU2NS0wOTU0PC9uYW1lSWRlbnRpZmllcj4KICAgIDwvY3JlYXRvcj4KICAgIDxjcmVhdG9yPgogICAgICA8Y3JlYXRvck5hbWUgbmFtZVR5cGU9IlBlcnNvbmFsIj5NYXJpZWtlIEh1aXNtYW48L2NyZWF0b3JOYW1lPgogICAgICA8Z2l2ZW5OYW1lPk1hcmlla2U8L2dpdmVuTmFtZT4KICAgICAgPGZhbWlseU5hbWU+SHVpc21hbjwvZmFtaWx5TmFtZT4KICAgICAgPG5hbWVJZGVudGlmaWVyIG5hbWVJZGVudGlmaWVyU2NoZW1lPSJodHRwczovL29yY2lkLm9yZy8iPjAwMDAtMDAwMy00NDY3LTA3Mlg8L25hbWVJZGVudGlmaWVyPgogICAgPC9jcmVhdG9yPgogIDwvY3JlYXRvcnM+CiAgPHRpdGxlcz4KICAgIDx0aXRsZT5TcGVjaWZpY2F0aW9uIFRyYW5zbGF0b3I6IFRvb2wgdG8gVHJhbnNsYXRlIFNwZWNpZmljYXRpb25zIGZvciBEZWR1Y3RpdmUgVmVyaWZpZXJzPC90aXRsZT4KICA8L3RpdGxlcz4KICA8cHVibGlzaGVyPjRUVS5SZXNlYXJjaERhdGE8L3B1Ymxpc2hlcj4KICA8cHVibGljYXRpb25ZZWFyPjIwMjM8L3B1YmxpY2F0aW9uWWVhcj4KICA8cmVzb3VyY2VUeXBlIHJlc291cmNlVHlwZUdlbmVyYWw9IlNvZnR3YXJlIj5Tb2Z0d2FyZTwvcmVzb3VyY2VUeXBlPgogIDxzdWJqZWN0cz4KICAgIDxzdWJqZWN0IHN1YmplY3RTY2hlbWU9IkF1c3RyYWxpYW4gYW5kIE5ldyBaZWFsYW5kIFN0YW5kYXJkIFJlc2VhcmNoIENsYXNzaWZpY2F0aW9uIChBTlpTUkMpLCAyMDA4IiBjbGFzc2lmaWNhdGlvbkNvZGU9IjA4MDMiPkNvbXB1dGVyIFNvZnR3YXJlPC9zdWJqZWN0PgogICAgPHN1YmplY3Qgc3ViamVjdFNjaGVtZT0iQXVzdHJhbGlhbiBhbmQgTmV3IFplYWxhbmQgU3RhbmRhcmQgUmVzZWFyY2ggQ2xhc3NpZmljYXRpb24gKEFOWlNSQyksIDIwMDgiIGNsYXNzaWZpY2F0aW9uQ29kZT0iMDgiPkluZm9ybWF0aW9uIGFuZCBDb21wdXRpbmcgU2NpZW5jZXM8L3N1YmplY3Q+CiAgICA8c3ViamVjdD5EZWR1Y3RpdmUgdmVyaWZpY2F0aW9uPC9zdWJqZWN0PgogICAgPHN1YmplY3Q+U3BlY2lmaWNhdGlvbnM8L3N1YmplY3Q+CiAgICA8c3ViamVjdD5Bbm5vdGF0aW9uczwvc3ViamVjdD4KICAgIDxzdWJqZWN0PlNwZWNpZmljYXRpb24gbGFuZ3VhZ2VzPC9zdWJqZWN0PgogICAgPHN1YmplY3Q+U2VtYW50aWNzPC9zdWJqZWN0PgogICAgPHN1YmplY3Q+VHJhbnNsYXRpb248L3N1YmplY3Q+CiAgPC9zdWJqZWN0cz4KICA8Y29udHJpYnV0b3JzPgogICAgPGNvbnRyaWJ1dG9yIGNvbnRyaWJ1dG9yVHlwZT0iT3RoZXIiPgogICAgICA8Y29udHJpYnV0b3JOYW1lIG5hbWVUeXBlPSJPcmdhbml6YXRpb25hbCI+VW5pdmVyc2l0eSBvZiBUd2VudGUsIEZhY3VsdHkgb2YgRWxlY3RyaWNhbCBFbmdpbmVlcmluZywgTWF0aGVtYXRpY3MgYW5kIENvbXB1dGVyIFNjaWVuY2UgKEVFTUNTKSwgRm9ybWFsIE1ldGhvZHMgYW5kIFRvb2xzPC9jb250cmlidXRvck5hbWU+CiAgICA8L2NvbnRyaWJ1dG9yPgogIDwvY29udHJpYnV0b3JzPgogIDxkYXRlcz4KICAgIDxkYXRlIGRhdGVUeXBlPSJJc3N1ZWQiPjIwMjMtMDYtMTk8L2RhdGU+CiAgPC9kYXRlcz4KICA8bGFuZ3VhZ2U+ZW48L2xhbmd1YWdlPgogIDxmb3JtYXRzPgogICAgPGZvcm1hdD4xKSBaSVAgZmlsZSB0aGF0IGNvbnRhaW5zIFNjYWxhIGZpbGVzLCBKYXZhIGZpbGVzLCBQeXRob24gc2NyaXB0cywgdGV4dCBmaWxlcywgSkFSIGZpbGUsIDIpIE1hcmtkb3duIChtZCkgZmlsZSwgMykgVmlydHVhbCBNYWNoaW5lIGluIC5vdmEgZm9ybWF0PC9mb3JtYXQ+CiAgPC9mb3JtYXRzPgogIDx2ZXJzaW9uPjE8L3ZlcnNpb24+CiAgPHJpZ2h0c0xpc3Q+CiAgICA8cmlnaHRzIHJpZ2h0c1VSST0iaHR0cHM6Ly9jcmVhdGl2ZWNvbW1vbnMub3JnL2xpY2Vuc2VzL2J5LzQuMC8iPkNDIEJZIDQuMDwvcmlnaHRzPgogIDwvcmlnaHRzTGlzdD4KICA8ZGVzY3JpcHRpb25zPgogICAgPGRlc2NyaXB0aW9uIGRlc2NyaXB0aW9uVHlwZT0iQWJzdHJhY3QiPiZsdDtwJmd0OyZsdDtzdHJvbmcmZ3Q7QWJvdXQgdGhlIFNwZWNpZmljYXRpb24gVHJhbnNsYXRvciZsdDsvc3Ryb25nJmd0OyZsdDsvcCZndDsmbHQ7cCZndDtUaGUgU3BlY2lmaWNhdGlvbiBUcmFuc2xhdG9yIGlzIGEgdG9vbCB0aGF0IGhhcyBiZWVuIGltcGxlbWVudGVkIGFzIHBhcnQgb2Ygb3VyIHJlc2VhcmNoIHRpdGxlZCAiSm9pbiBGb3JjZXMhIFJldXNpbmcgQ29udHJhY3RzIGZvciBEZWR1Y3RpdmUgVmVyaWZpZXJzIHRocm91Z2ggQXV0b21hdGljIFRyYW5zbGF0aW9uIi4gVGhpcyB0b29sIHdpbGwgdHJhbnNsYXRlIHNwZWNpZmljYXRpb25zIGluIHZlcmlmaWVkIEphdmEgcHJvZ3JhbXMgZnJvbSBvbmUgc3BlY2lmaWNhdGlvbiBsYW5ndWFnZSBpbnRvIGFub3RoZXIuIEl0IHN1cHBvcnRzIHRoZSB0b29scyBLcmFrYXRvYSwgT3BlbkpNTCBhbmQgVmVyQ29ycy4mbHQ7L3AmZ3Q7Jmx0O3AmZ3Q7Jmx0O2JyJmd0OyZsdDsvcCZndDsmbHQ7cCZndDtUaGUgdG9vbCB0YWtlcyBhbiBhbm5vdGF0ZWQgSmF2YSBwcm9ncmFtIGFuZCBhIHRhcmdldCB0b29sIGFzIGlucHV0LiBJdCB3aWxsIHRoZW4gZ2VuZXJhdGUgYW4gYW5ub3RhdGVkIEphdmEgcHJvZ3JhbSB3aGVyZSB0aGUgYW5ub3RhdGlvbnMgaGF2ZSBiZWVuIHRyYW5zbGF0ZWQuJmx0Oy9wJmd0OyZsdDtwJmd0OyZsdDticiZndDsmbHQ7L3AmZ3Q7Jmx0O3AmZ3Q7Jmx0O3N0cm9uZyZndDtXaGF0J3MgaW5jbHVkZWQgaW4gdGhpcyBhcnRpZmFjdD8mbHQ7L3N0cm9uZyZndDsmbHQ7L3AmZ3Q7Jmx0O3AmZ3Q7VGhpcyBhcnRpZmFjdCBjb250YWlucyB0aGUgZm9sbG93aW5nIHRoaW5nczombHQ7L3AmZ3Q7Jmx0O3AmZ3Q7LSBzcGVjaWZpY2F0aW9uLXRyYW5zbGF0b3IuemlwOiBBIGRpcmVjdG9yeSBjb250YWluaW5nIHRoZSBTcGVjaWZpY2F0aW9uIFRyYW5zbGF0b3IgdG9vbCBhcyB3ZWxsIGFzIHRoZSBleGFtcGxlcyB1c2VkIGZvciB0aGUgZXZhbHVhdGlvbi4mbHQ7L3AmZ3Q7Jmx0O3AmZ3Q7LSBTcGVjVHJhbnNsYXRvckFydGlmYWN0Lm92YTogQSBWaXJ0dWFsIE1hY2hpbmUgd2l0aCB0aGUgU3BlY2lmaWNhdGlvbiBUcmFuc2xhdG9yIHRvb2wsIGFzIHdlbGwgYXMgdGhlIE9wZW5KTUwgYW5kIFZlckNvcnMgdmVyaWZpZXJzLiBJdCBhbHNvIGNvbnRhaW5zIHRoZSBleGFtcGxlcyB1c2VkIGZvciB0aGUgZXZhbHVhdGlvbiBhbmQgYSBzY3JpcHQgdG8gcmVwcm9kdWNlIHRoZSBldmFsdWF0aW9uLiZsdDsvcCZndDsmbHQ7cCZndDsmbHQ7YnImZ3Q7Jmx0Oy9wJmd0OyZsdDtwJmd0O1lvdSBjYW4gdXNlIHRoZSBWaXJ0dWFsIE1hY2hpbmUgdG8gcmVwcm9kdWNlIHRoZSBldmFsdWF0aW9uIGluY2x1ZGluZyB2ZXJpZmljYXRpb24gYWZ0ZXIgdHJhbnNsYXRpb24uJmx0Oy9wJmd0OyZsdDtwJmd0O0lmIHlvdSBqdXN0IHdhbnQgdG8gdXNlIHRoZSBTcGVjaWZpY2F0aW9uIFRyYW5zbGF0b3Igb3IgaGF2ZSBhIGxvb2sgYXQgdGhlIGlucHV0L291dHB1dCBmaWxlcyBvZiB0aGUgZXZhbHVhdGlvbiwgdGhlbiB0aGUgemlwIGZpbGUgaXMgc3VmZmljaWVudC4mbHQ7L3AmZ3Q7Jmx0O3AmZ3Q7Jmx0O2JyJmd0OyZsdDsvcCZndDsmbHQ7cCZndDsmbHQ7c3Ryb25nJmd0O0xpY2Vuc2UgaW5mb3JtYXRpb24mbHQ7L3N0cm9uZyZndDsmbHQ7L3AmZ3Q7Jmx0O3AmZ3Q7VGhlIFNwZWNpZmljYXRpb24gVHJhbnNsYXRvciB0b29sIGlzIHNoYXJlZCB1bmRlciB0aGUgQ0MtQlkgNC4wIGxpY2Vuc2UuJmx0Oy9wJmd0OyZsdDtwJmd0O1RoZSB2ZXJpZmllcnMgaW4gdGhlIFZNLCBhcyB3ZWxsIGFzIHRoZSBleGFtcGxlcyBhbmQgY2FzZSBzdHVkaWVzIHVzZWQgZm9yIHRoZSBldmFsdWF0aW9uLCBhcmUgJmx0O3N0cm9uZyZndDtub3QmbHQ7L3N0cm9uZyZndDsgbGljZW5zZWQgdW5kZXIgdGhlIENDLUJZIDQuMCBidXQgdW5kZXIgdGhlaXIgb3JpZ2luYWwgbGljZW5zZXMgd2hpY2ggaGF2ZSBiZWVuIGluY2x1ZGVkLiZsdDsvcCZndDs8L2Rlc2NyaXB0aW9uPgogIDwvZGVzY3JpcHRpb25zPgogIDxmdW5kaW5nUmVmZXJlbmNlcz4KICAgIDxmdW5kaW5nUmVmZXJlbmNlPgogICAgICA8ZnVuZGVyTmFtZT5EdXRjaCBSZXNlYXJjaCBDb3VuY2lsPC9mdW5kZXJOYW1lPgogICAgICA8YXdhcmROdW1iZXI+NjM5LjAyMy43MTA8L2F3YXJkTnVtYmVyPgogICAgICA8YXdhcmRUaXRsZT5NZXJjZWRlczogTWF4aW1hbCBSZWxpYWJpbGl0eSBvZiBDb25jdXJyZW50IGFuZCBEaXN0cmlidXRlZCBTb2Z0d2FyZTwvYXdhcmRUaXRsZT4KICAgIDwvZnVuZGluZ1JlZmVyZW5jZT4KICA8L2Z1bmRpbmdSZWZlcmVuY2VzPgo8L3Jlc291cmNlPg==","url":"https://data.4tu.nl/datasets/a85a3b8a-db37-496b-860a-d3cbc988dc9d","contentUrl":null,"metadataVersion":0,"schemaVersion":"http://datacite.org/schema/kernel-4","source":"api","isActive":true,"state":"findable","reason":null,"viewCount":0,"viewsOverTime":[],"downloadCount":0,"downloadsOverTime":[],"referenceCount":0,"citationCount":0,"citationsOverTime":[],"partCount":0,"partOfCount":0,"versionCount":0,"versionOfCount":0,"created":"2023-06-19T12:59:09.000Z","registered":"2023-06-19T12:59:10.000Z","published":"2023","updated":"2023-06-19T12:59:10.000Z"},"relationships":{"client":{"data":{"id":"delft.data4tu","type":"clients"}},"provider":{"data":{"id":"scpr","type":"providers"}},"media":{"data":{"id":"10.4121/21820458","type":"media"}},"references":{"data":[]},"citations":{"data":[]},"parts":{"data":[]},"partOf":{"data":[]},"versions":{"data":[]},"versionOf":{"data":[]}}}}