{"data":{"id":"10.4121/21e79524-40c4-4dc1-8108-94e7b6fc6d9f","type":"dois","attributes":{"doi":"10.4121/21e79524-40c4-4dc1-8108-94e7b6fc6d9f","prefix":"10.4121","suffix":"21e79524-40c4-4dc1-8108-94e7b6fc6d9f","identifiers":[],"alternateIdentifiers":[],"creators":[{"name":"Armborst, Lukas","nameType":"Personal","givenName":"Lukas","familyName":"Armborst","nameIdentifiers":[{"nameIdentifier":"0000-0001-7565-0954","nameIdentifierScheme":"https://orcid.org/"}],"affiliation":[]},{"name":"Lathouwers, Sophie","nameType":"Personal","givenName":"Sophie","familyName":"Lathouwers","nameIdentifiers":[{"nameIdentifier":"0000-0002-7544-447X","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: Artifact for iFM 2023 paper \"Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation\""}],"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":"Specifications"},{"subject":"Deductive Verification"},{"subject":"Annotations"},{"subject":"Tool interoperability"}],"contributors":[{"name":"University Of Twente, Faculty Of Electrical Engineering, Mathematics And Computer Science, Formal Methods And Tools (FMT)","nameType":"Organizational","affiliation":[],"contributorType":"Other","nameIdentifiers":[]}],"dates":[{"date":"2023-09-05","dateType":"Issued"}],"language":"en","types":{"ris":"COMP","bibtex":"misc","citeproc":"article","schemaOrg":"SoftwareSourceCode","resourceType":"Software","resourceTypeGeneral":"Software"},"relatedIdentifiers":[],"relatedItems":[],"sizes":[],"formats":["ZIP file that contains a Scala project (consisting of Scala files, Java files, a jar executable, and others) as well as related Python scripts, text files, and Debian Software Package (.deb) files for dependencies"],"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":"We present the Specification Translator, a tool that has been implemented as part of our research titled \"Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation\".hen using deductive verifiers to prove a program’s correctness, users have to write formal specifications.Unfortunately, each tool uses its own specification language for this, which makes it difficult to reuse the specifications.This tool makes this process quicker \u0026amp; easier by automatically translating such specifications in verified Java programs from one specification language to another. It supports the tools Krakatoa, OpenJML and VerCors.The 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. This artifact allows you to reproduce the evaluation discussed in the paper.For more information, we refer to the ReadMe inside the artifact.","descriptionType":"Abstract"}],"geoLocations":[],"fundingReferences":[{"awardTitle":"Mercedes: Maximal Reliability of Concurrent and Distributed Software","funderName":"Dutch Research Council","awardNumber":"639.023.710"}],"xml":"PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0iVVRGLTgiPz4KPHJlc291cmNlIHhtbG5zPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCIgeG1sbnM6eHNpPSJodHRwOi8vd3d3LnczLm9yZy8yMDAxL1hNTFNjaGVtYS1pbnN0YW5jZSIgeHNpOnNjaGVtYUxvY2F0aW9uPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCBodHRwOi8vc2NoZW1hLmRhdGFjaXRlLm9yZy9tZXRhL2tlcm5lbC00LjQvbWV0YWRhdGEueHNkIj4KICA8aWRlbnRpZmllciBpZGVudGlmaWVyVHlwZT0iRE9JIj4xMC40MTIxLzIxRTc5NTI0LTQwQzQtNERDMS04MTA4LTk0RTdCNkZDNkQ5RjwvaWRlbnRpZmllcj4KICA8Y3JlYXRvcnM+CiAgICA8Y3JlYXRvcj4KICAgICAgPGNyZWF0b3JOYW1lIG5hbWVUeXBlPSJQZXJzb25hbCI+THVrYXMgQXJtYm9yc3Q8L2NyZWF0b3JOYW1lPgogICAgICA8Z2l2ZW5OYW1lPkx1a2FzPC9naXZlbk5hbWU+CiAgICAgIDxmYW1pbHlOYW1lPkFybWJvcnN0PC9mYW1pbHlOYW1lPgogICAgICA8bmFtZUlkZW50aWZpZXIgbmFtZUlkZW50aWZpZXJTY2hlbWU9Imh0dHBzOi8vb3JjaWQub3JnLyI+MDAwMC0wMDAxLTc1NjUtMDk1NDwvbmFtZUlkZW50aWZpZXI+CiAgICA8L2NyZWF0b3I+CiAgICA8Y3JlYXRvcj4KICAgICAgPGNyZWF0b3JOYW1lIG5hbWVUeXBlPSJQZXJzb25hbCI+U29waGllIExhdGhvdXdlcnM8L2NyZWF0b3JOYW1lPgogICAgICA8Z2l2ZW5OYW1lPlNvcGhpZTwvZ2l2ZW5OYW1lPgogICAgICA8ZmFtaWx5TmFtZT5MYXRob3V3ZXJzPC9mYW1pbHlOYW1lPgogICAgICA8bmFtZUlkZW50aWZpZXIgbmFtZUlkZW50aWZpZXJTY2hlbWU9Imh0dHBzOi8vb3JjaWQub3JnLyI+MDAwMC0wMDAyLTc1NDQtNDQ3WDwvbmFtZUlkZW50aWZpZXI+CiAgICA8L2NyZWF0b3I+CiAgICA8Y3JlYXRvcj4KICAgICAgPGNyZWF0b3JOYW1lIG5hbWVUeXBlPSJQZXJzb25hbCI+TWFyaWVrZSBIdWlzbWFuPC9jcmVhdG9yTmFtZT4KICAgICAgPGdpdmVuTmFtZT5NYXJpZWtlPC9naXZlbk5hbWU+CiAgICAgIDxmYW1pbHlOYW1lPkh1aXNtYW48L2ZhbWlseU5hbWU+CiAgICAgIDxuYW1lSWRlbnRpZmllciBuYW1lSWRlbnRpZmllclNjaGVtZT0iaHR0cHM6Ly9vcmNpZC5vcmcvIj4wMDAwLTAwMDMtNDQ2Ny0wNzJYPC9uYW1lSWRlbnRpZmllcj4KICAgIDwvY3JlYXRvcj4KICA8L2NyZWF0b3JzPgogIDx0aXRsZXM+CiAgICA8dGl0bGU+U3BlY2lmaWNhdGlvbiBUcmFuc2xhdG9yOiBBcnRpZmFjdCBmb3IgaUZNIDIwMjMgcGFwZXIgIkpvaW5pbmcgRm9yY2VzISBSZXVzaW5nIENvbnRyYWN0cyBmb3IgRGVkdWN0aXZlIFZlcmlmaWVycyB0aHJvdWdoIEF1dG9tYXRpYyBUcmFuc2xhdGlvbiI8L3RpdGxlPgogIDwvdGl0bGVzPgogIDxwdWJsaXNoZXI+NFRVLlJlc2VhcmNoRGF0YTwvcHVibGlzaGVyPgogIDxwdWJsaWNhdGlvblllYXI+MjAyMzwvcHVibGljYXRpb25ZZWFyPgogIDxyZXNvdXJjZVR5cGUgcmVzb3VyY2VUeXBlR2VuZXJhbD0iU29mdHdhcmUiPlNvZnR3YXJlPC9yZXNvdXJjZVR5cGU+CiAgPHN1YmplY3RzPgogICAgPHN1YmplY3Qgc3ViamVjdFNjaGVtZT0iQXVzdHJhbGlhbiBhbmQgTmV3IFplYWxhbmQgU3RhbmRhcmQgUmVzZWFyY2ggQ2xhc3NpZmljYXRpb24gKEFOWlNSQyksIDIwMDgiIGNsYXNzaWZpY2F0aW9uQ29kZT0iMDgwMyI+Q29tcHV0ZXIgU29mdHdhcmU8L3N1YmplY3Q+CiAgICA8c3ViamVjdCBzdWJqZWN0U2NoZW1lPSJBdXN0cmFsaWFuIGFuZCBOZXcgWmVhbGFuZCBTdGFuZGFyZCBSZXNlYXJjaCBDbGFzc2lmaWNhdGlvbiAoQU5aU1JDKSwgMjAwOCIgY2xhc3NpZmljYXRpb25Db2RlPSIwOCI+SW5mb3JtYXRpb24gYW5kIENvbXB1dGluZyBTY2llbmNlczwvc3ViamVjdD4KICAgIDxzdWJqZWN0PlNwZWNpZmljYXRpb25zPC9zdWJqZWN0PgogICAgPHN1YmplY3Q+RGVkdWN0aXZlIFZlcmlmaWNhdGlvbjwvc3ViamVjdD4KICAgIDxzdWJqZWN0PkFubm90YXRpb25zPC9zdWJqZWN0PgogICAgPHN1YmplY3Q+VG9vbCBpbnRlcm9wZXJhYmlsaXR5PC9zdWJqZWN0PgogIDwvc3ViamVjdHM+CiAgPGNvbnRyaWJ1dG9ycz4KICAgIDxjb250cmlidXRvciBjb250cmlidXRvclR5cGU9Ik90aGVyIj4KICAgICAgPGNvbnRyaWJ1dG9yTmFtZSBuYW1lVHlwZT0iT3JnYW5pemF0aW9uYWwiPlVuaXZlcnNpdHkgb2YgVHdlbnRlLCBGYWN1bHR5IG9mIEVsZWN0cmljYWwgRW5naW5lZXJpbmcsIE1hdGhlbWF0aWNzIGFuZCBDb21wdXRlciBTY2llbmNlLCBGb3JtYWwgTWV0aG9kcyBhbmQgVG9vbHMgKEZNVCk8L2NvbnRyaWJ1dG9yTmFtZT4KICAgIDwvY29udHJpYnV0b3I+CiAgPC9jb250cmlidXRvcnM+CiAgPGRhdGVzPgogICAgPGRhdGUgZGF0ZVR5cGU9Iklzc3VlZCI+MjAyMy0wOS0wNTwvZGF0ZT4KICA8L2RhdGVzPgogIDxsYW5ndWFnZT5lbjwvbGFuZ3VhZ2U+CiAgPGZvcm1hdHM+CiAgICA8Zm9ybWF0PlpJUCBmaWxlIHRoYXQgY29udGFpbnMgYSBTY2FsYSBwcm9qZWN0IChjb25zaXN0aW5nIG9mIFNjYWxhIGZpbGVzLCBKYXZhIGZpbGVzLCBhIGphciBleGVjdXRhYmxlLCBhbmQgb3RoZXJzKSBhcyB3ZWxsIGFzIHJlbGF0ZWQgUHl0aG9uIHNjcmlwdHMsIHRleHQgZmlsZXMsIGFuZCBEZWJpYW4gU29mdHdhcmUgUGFja2FnZSAoLmRlYikgZmlsZXMgZm9yIGRlcGVuZGVuY2llczwvZm9ybWF0PgogIDwvZm9ybWF0cz4KICA8dmVyc2lvbj4xPC92ZXJzaW9uPgogIDxyaWdodHNMaXN0PgogICAgPHJpZ2h0cyByaWdodHNVUkk9Imh0dHBzOi8vY3JlYXRpdmVjb21tb25zLm9yZy9saWNlbnNlcy9ieS80LjAvIj5DQyBCWSA0LjA8L3JpZ2h0cz4KICA8L3JpZ2h0c0xpc3Q+CiAgPGRlc2NyaXB0aW9ucz4KICAgIDxkZXNjcmlwdGlvbiBkZXNjcmlwdGlvblR5cGU9IkFic3RyYWN0Ij4mbHQ7cCZndDtXZSBwcmVzZW50IHRoZSBTcGVjaWZpY2F0aW9uIFRyYW5zbGF0b3IsIGEgdG9vbCB0aGF0IGhhcyBiZWVuIGltcGxlbWVudGVkIGFzIHBhcnQgb2Ygb3VyIHJlc2VhcmNoIHRpdGxlZCAiSm9pbmluZyBGb3JjZXMhIFJldXNpbmcgQ29udHJhY3RzIGZvciBEZWR1Y3RpdmUgVmVyaWZpZXJzIHRocm91Z2ggQXV0b21hdGljIFRyYW5zbGF0aW9uIi4mbHQ7L3AmZ3Q7Jmx0O3AmZ3Q7aGVuIHVzaW5nIGRlZHVjdGl2ZSB2ZXJpZmllcnMgdG8gcHJvdmUgYSBwcm9ncmFt4oCZcyBjb3JyZWN0bmVzcywgdXNlcnMgaGF2ZSB0byB3cml0ZSBmb3JtYWwgc3BlY2lmaWNhdGlvbnMuJmx0Oy9wJmd0OyZsdDtwJmd0O1VuZm9ydHVuYXRlbHksIGVhY2ggdG9vbCB1c2VzIGl0cyBvd24gc3BlY2lmaWNhdGlvbiBsYW5ndWFnZSBmb3IgdGhpcywgd2hpY2ggbWFrZXMgaXQgZGlmZmljdWx0IHRvIHJldXNlIHRoZSBzcGVjaWZpY2F0aW9ucy4mbHQ7L3AmZ3Q7Jmx0O3AmZ3Q7VGhpcyB0b29sIG1ha2VzIHRoaXMgcHJvY2VzcyBxdWlja2VyICZhbXA7YW1wOyBlYXNpZXIgYnkgYXV0b21hdGljYWxseSB0cmFuc2xhdGluZyBzdWNoIHNwZWNpZmljYXRpb25zIGluIHZlcmlmaWVkIEphdmEgcHJvZ3JhbXMgZnJvbSBvbmUgc3BlY2lmaWNhdGlvbiBsYW5ndWFnZSB0byBhbm90aGVyLiBJdCBzdXBwb3J0cyB0aGUgdG9vbHMgS3Jha2F0b2EsIE9wZW5KTUwgYW5kIFZlckNvcnMuJmx0Oy9wJmd0OyZsdDtwJmd0O1RoZSB0b29sIHRha2VzIGFuIGFubm90YXRlZCBKYXZhIHByb2dyYW0gYW5kIGEgdGFyZ2V0IHRvb2wgYXMgaW5wdXQuIEl0IHdpbGwgdGhlbiBnZW5lcmF0ZSBhbiBhbm5vdGF0ZWQgSmF2YSBwcm9ncmFtIHdoZXJlIHRoZSBhbm5vdGF0aW9ucyBoYXZlIGJlZW4gdHJhbnNsYXRlZC4mbHQ7L3AmZ3Q7Jmx0O3AmZ3Q7JmFtcDtuYnNwOyZsdDsvcCZndDsmbHQ7cCZndDtUaGlzIGFydGlmYWN0IGFsbG93cyB5b3UgdG8gcmVwcm9kdWNlIHRoZSBldmFsdWF0aW9uIGRpc2N1c3NlZCBpbiB0aGUgcGFwZXIuJmx0Oy9wJmd0OyZsdDtwJmd0O0ZvciBtb3JlIGluZm9ybWF0aW9uLCB3ZSByZWZlciB0byB0aGUgUmVhZE1lIGluc2lkZSB0aGUgYXJ0aWZhY3QuJmx0Oy9wJmd0OzwvZGVzY3JpcHRpb24+CiAgPC9kZXNjcmlwdGlvbnM+CiAgPGZ1bmRpbmdSZWZlcmVuY2VzPgogICAgPGZ1bmRpbmdSZWZlcmVuY2U+CiAgICAgIDxmdW5kZXJOYW1lPkR1dGNoIFJlc2VhcmNoIENvdW5jaWw8L2Z1bmRlck5hbWU+CiAgICAgIDxhd2FyZE51bWJlcj42MzkuMDIzLjcxMDwvYXdhcmROdW1iZXI+CiAgICAgIDxhd2FyZFRpdGxlPk1lcmNlZGVzOiBNYXhpbWFsIFJlbGlhYmlsaXR5IG9mIENvbmN1cnJlbnQgYW5kIERpc3RyaWJ1dGVkIFNvZnR3YXJlPC9hd2FyZFRpdGxlPgogICAgPC9mdW5kaW5nUmVmZXJlbmNlPgogIDwvZnVuZGluZ1JlZmVyZW5jZXM+CjwvcmVzb3VyY2U+","url":"https://data.4tu.nl/datasets/21e79524-40c4-4dc1-8108-94e7b6fc6d9f","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-09-05T08:15:27.000Z","registered":"2023-09-05T08:15:27.000Z","published":"2023","updated":"2023-09-05T08:15:28.000Z"},"relationships":{"client":{"data":{"id":"delft.data4tu","type":"clients"}},"provider":{"data":{"id":"scpr","type":"providers"}},"media":{"data":{"id":"10.4121/21e79524-40c4-4dc1-8108-94e7b6fc6d9f","type":"media"}},"references":{"data":[]},"citations":{"data":[]},"parts":{"data":[]},"partOf":{"data":[]},"versions":{"data":[]},"versionOf":{"data":[]}}}}