{"data":{"id":"10.6084/m9.figshare.5900260.v1","type":"dois","attributes":{"doi":"10.6084/m9.figshare.5900260.v1","prefix":"10.6084","suffix":"m9.figshare.5900260.v1","identifiers":[],"alternateIdentifiers":[],"creators":[{"name":"Roux, Pierre","nameType":"Personal","givenName":"Pierre","familyName":"Roux","affiliation":[],"nameIdentifiers":[]},{"name":"Iguernlala, Mohamed","nameType":"Personal","givenName":"Mohamed","familyName":"Iguernlala","affiliation":[],"nameIdentifiers":[]},{"name":"Conchon, Sylvain","nameType":"Personal","givenName":"Sylvain","familyName":"Conchon","affiliation":[],"nameIdentifiers":[]}],"titles":[{"title":"A Non-linear Arithmetic Procedure for Control-Command Software Verification"}],"publisher":"figshare","container":{},"publicationYear":2018,"subjects":[{"subject":"Applied Computer Science"},{"subject":"100601 Arithmetic and Logic Structures","subjectScheme":"FOR"},{"subject":"FOS: Electrical engineering, electronic engineering, information engineering","schemeUri":"http://www.oecd.org/science/inno/38235147.pdf","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"FOS: Electrical engineering, electronic engineering, information engineering","subjectScheme":"Fields of Science and Technology (FOS)"}],"contributors":[],"dates":[{"date":"2018-04-13","dateType":"Created"},{"date":"2018-04-13","dateType":"Updated"},{"date":"2018","dateType":"Issued"}],"language":null,"types":{"ris":"DATA","bibtex":"misc","citeproc":"dataset","schemaOrg":"Dataset","resourceType":"Dataset","resourceTypeGeneral":"Dataset"},"relatedIdentifiers":[{"relationType":"IsSupplementTo","relatedIdentifier":"10.1007/978-3-319-89963-3_8","relatedIdentifierType":"DOI"},{"relationType":"IsIdenticalTo","relatedIdentifier":"10.6084/m9.figshare.5900260","relatedIdentifierType":"DOI"}],"relatedItems":[],"sizes":["547793493 Bytes"],"formats":[],"version":null,"rightsList":[{"rights":"Creative Commons Zero v1.0 Universal","rightsUri":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","schemeUri":"https://spdx.org/licenses/","rightsIdentifier":"cc0-1.0","rightsIdentifierScheme":"SPDX"}],"descriptions":[{"description":"This dataset contains data and source code relating to the paper \"A Non-linear Arithmetic Procedure for Control-Command Software Verification\", and enables the replication of the Experimental Results section of the paper. The paper investigated a-posteriori validation methods and their integration into the SMT (Satisfiability Modulo Theories) framework, with a prototype integrated into the Alt-Ergo SMT solver.\u003cbr\u003eA modified version of the Alt-Ergo SMT solver and its sources are provided in the tarball alt-ergo-1.30+osdp.tgz.\u003cbr\u003eThe dataset consists of compressed .deb and .tar files.\u003cbr\u003e\u003cbr\u003eA README file is included which includes both standard installation instructions and instructions for installation without a network.\u003cbr\u003e\u003cbr\u003e\u003cbr\u003e\u003cbr\u003e","descriptionType":"Abstract"}],"geoLocations":[],"fundingReferences":[],"xml":"PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0iVVRGLTgiPz4KPHJlc291cmNlIHhtbG5zPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCIgeG1sbnM6eHNpPSJodHRwOi8vd3d3LnczLm9yZy8yMDAxL1hNTFNjaGVtYS1pbnN0YW5jZSIgeHNpOnNjaGVtYUxvY2F0aW9uPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCBodHRwOi8vc2NoZW1hLmRhdGFjaXRlLm9yZy9tZXRhL2tlcm5lbC00LjEvbWV0YWRhdGEueHNkIj4KICA8aWRlbnRpZmllciBpZGVudGlmaWVyVHlwZT0iRE9JIj4xMC42MDg0L005LkZJR1NIQVJFLjU5MDAyNjAuVjE8L2lkZW50aWZpZXI+CiAgPGNyZWF0b3JzPgogICAgPGNyZWF0b3I+CiAgICAgIDxjcmVhdG9yTmFtZT5QaWVycmUgUm91eDwvY3JlYXRvck5hbWU+CiAgICA8L2NyZWF0b3I+CiAgICA8Y3JlYXRvcj4KICAgICAgPGNyZWF0b3JOYW1lPk1vaGFtZWQgSWd1ZXJubGFsYTwvY3JlYXRvck5hbWU+CiAgICA8L2NyZWF0b3I+CiAgICA8Y3JlYXRvcj4KICAgICAgPGNyZWF0b3JOYW1lPlN5bHZhaW4gQ29uY2hvbjwvY3JlYXRvck5hbWU+CiAgICA8L2NyZWF0b3I+CiAgPC9jcmVhdG9ycz4KICA8dGl0bGVzPgogICAgPHRpdGxlPkEgTm9uLWxpbmVhciBBcml0aG1ldGljIFByb2NlZHVyZSBmb3IgQ29udHJvbC1Db21tYW5kIFNvZnR3YXJlIFZlcmlmaWNhdGlvbjwvdGl0bGU+CiAgPC90aXRsZXM+CiAgPGRlc2NyaXB0aW9ucz4KICAgIDxkZXNjcmlwdGlvbiBkZXNjcmlwdGlvblR5cGU9IkFic3RyYWN0Ij5UaGlzIGRhdGFzZXQgY29udGFpbnMgZGF0YSBhbmQgc291cmNlIGNvZGUgcmVsYXRpbmcgdG8gdGhlIHBhcGVyICJBIE5vbi1saW5lYXIgQXJpdGhtZXRpYyBQcm9jZWR1cmUgZm9yIENvbnRyb2wtQ29tbWFuZCBTb2Z0d2FyZSBWZXJpZmljYXRpb24iLCBhbmQgZW5hYmxlcyB0aGUgcmVwbGljYXRpb24gb2YgdGhlIEV4cGVyaW1lbnRhbCBSZXN1bHRzIHNlY3Rpb24gb2YgdGhlIHBhcGVyLiBUaGUgcGFwZXIgaW52ZXN0aWdhdGVkIGEtcG9zdGVyaW9yaSB2YWxpZGF0aW9uIG1ldGhvZHMgYW5kIHRoZWlyIGludGVncmF0aW9uIGludG8gdGhlIFNNVCAoU2F0aXNmaWFiaWxpdHkgTW9kdWxvIFRoZW9yaWVzKSBmcmFtZXdvcmssIHdpdGggYSBwcm90b3R5cGUgaW50ZWdyYXRlZCBpbnRvIHRoZSBBbHQtRXJnbyBTTVQgc29sdmVyLiZsdDtkaXYmZ3Q7Jmx0O2JyJmd0OyZsdDsvZGl2Jmd0OyZsdDtkaXYmZ3Q7QSBtb2RpZmllZCB2ZXJzaW9uIG9mIHRoZSBBbHQtRXJnbyBTTVQgc29sdmVyIGFuZCBpdHMgc291cmNlcyBhcmUgcHJvdmlkZWQgaW4gdGhlIHRhcmJhbGwgYWx0LWVyZ28tMS4zMCtvc2RwLnRnei4mbHQ7L2RpdiZndDsmbHQ7ZGl2Jmd0OyZsdDticiZndDsmbHQ7L2RpdiZndDsmbHQ7ZGl2Jmd0O1RoZSBkYXRhc2V0IGNvbnNpc3RzIG9mIGNvbXByZXNzZWQgLmRlYiBhbmQgLnRhciBmaWxlcy4mbHQ7YnImZ3Q7Jmx0O2RpdiZndDsmbHQ7YnImZ3Q7Jmx0Oy9kaXYmZ3Q7Jmx0O2RpdiZndDsmbHQ7ZGl2Jmd0O0EgUkVBRE1FIGZpbGUgaXMgaW5jbHVkZWQgd2hpY2ggaW5jbHVkZXMgYm90aCBzdGFuZGFyZCBpbnN0YWxsYXRpb24gaW5zdHJ1Y3Rpb25zIGFuZCBpbnN0cnVjdGlvbnMgZm9yIGluc3RhbGxhdGlvbiB3aXRob3V0IGEgbmV0d29yay4mbHQ7YnImZ3Q7Jmx0Oy9kaXYmZ3Q7Jmx0O2RpdiZndDsmbHQ7YnImZ3Q7Jmx0Oy9kaXYmZ3Q7Jmx0O2RpdiZndDsmbHQ7YnImZ3Q7Jmx0Oy9kaXYmZ3Q7Jmx0O2RpdiZndDsmbHQ7YnImZ3Q7Jmx0Oy9kaXYmZ3Q7Jmx0Oy9kaXYmZ3Q7Jmx0Oy9kaXYmZ3Q7PC9kZXNjcmlwdGlvbj4KICA8L2Rlc2NyaXB0aW9ucz4KICA8c3ViamVjdHM+CiAgICA8c3ViamVjdD5BcHBsaWVkIENvbXB1dGVyIFNjaWVuY2U8L3N1YmplY3Q+CiAgICA8c3ViamVjdCBzY2hlbWVVUkk9Imh0dHA6Ly93d3cuYWJzLmdvdi5hdS9hdXNzdGF0cy9hYnNALm5zZi8wLzZCQjQyN0FCOTY5NkMyMjVDQTI1NzQxODAwMDQ0NjNFIiBzdWJqZWN0U2NoZW1lPSJGT1IiPjEwMDYwMSBBcml0aG1ldGljIGFuZCBMb2dpYyBTdHJ1Y3R1cmVzPC9zdWJqZWN0PgogIDwvc3ViamVjdHM+CiAgPHB1Ymxpc2hlcj5maWdzaGFyZTwvcHVibGlzaGVyPgogIDxwdWJsaWNhdGlvblllYXI+MjAxODwvcHVibGljYXRpb25ZZWFyPgogIDxkYXRlcz4KICAgIDxkYXRlIGRhdGVUeXBlPSJDcmVhdGVkIj4yMDE4LTA0LTEzPC9kYXRlPgogICAgPGRhdGUgZGF0ZVR5cGU9IlVwZGF0ZWQiPjIwMTgtMDQtMTM8L2RhdGU+CiAgPC9kYXRlcz4KICA8cmVzb3VyY2VUeXBlIHJlc291cmNlVHlwZUdlbmVyYWw9IkRhdGFzZXQiPkRhdGFzZXQ8L3Jlc291cmNlVHlwZT4KICA8c2l6ZXM+CiAgICA8c2l6ZT41NDc3OTM0OTMgQnl0ZXM8L3NpemU+CiAgPC9zaXplcz4KICA8cmVsYXRlZElkZW50aWZpZXJzPgogICAgPHJlbGF0ZWRJZGVudGlmaWVyIHJlbGF0ZWRJZGVudGlmaWVyVHlwZT0iRE9JIiByZWxhdGlvblR5cGU9IklzU3VwcGxlbWVudFRvIj4xMC4xMDA3Lzk3OC0zLTMxOS04OTk2My0zXzg8L3JlbGF0ZWRJZGVudGlmaWVyPgogICAgPHJlbGF0ZWRJZGVudGlmaWVyIHJlbGF0ZWRJZGVudGlmaWVyVHlwZT0iRE9JIiByZWxhdGlvblR5cGU9IklzSWRlbnRpY2FsVG8iPjEwLjYwODQvbTkuZmlnc2hhcmUuNTkwMDI2MDwvcmVsYXRlZElkZW50aWZpZXI+CiAgPC9yZWxhdGVkSWRlbnRpZmllcnM+CiAgPHJpZ2h0c0xpc3Q+CiAgICA8cmlnaHRzIHJpZ2h0c1VSST0iaHR0cHM6Ly9jcmVhdGl2ZWNvbW1vbnMub3JnL3B1YmxpY2RvbWFpbi96ZXJvLzEuMC8iPkNDMDwvcmlnaHRzPgogIDwvcmlnaHRzTGlzdD4KPC9yZXNvdXJjZT4=","url":"https://springernature.figshare.com/articles/A_Non-linear_Arithmetic_Procedure_for_Control-Command_Software_Verification/5900260/1","contentUrl":null,"metadataVersion":3,"schemaVersion":"http://datacite.org/schema/kernel-4","source":"mds","isActive":true,"state":"findable","reason":null,"viewCount":1,"viewsOverTime":[{"yearMonth":"2025-10","total":1}],"downloadCount":0,"downloadsOverTime":[{"yearMonth":"2025-10","total":0}],"referenceCount":1,"citationCount":0,"citationsOverTime":[],"partCount":0,"partOfCount":0,"versionCount":0,"versionOfCount":0,"created":"2018-04-13T15:03:08.000Z","registered":"2018-04-13T15:03:09.000Z","published":"2018","updated":"2020-08-30T15:19:37.000Z"},"relationships":{"client":{"data":{"id":"figshare.ars","type":"clients"}},"provider":{"data":{"id":"otjm","type":"providers"}},"media":{"data":{"id":"10.6084/m9.figshare.5900260.v1","type":"media"}},"references":{"data":[{"id":"10.1007/978-3-319-89963-3_8","type":"dois"}]},"citations":{"data":[]},"parts":{"data":[]},"partOf":{"data":[]},"versions":{"data":[]},"versionOf":{"data":[]}}}}