{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T13:59:40Z","timestamp":1756994380269,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":15,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T00:00:00Z","timestamp":1602028800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["VO 937\/28-2, BE 2334\/7-2, UL 433\/1-2"],"award-info":[{"award-number":["VO 937\/28-2, BE 2334\/7-2, UL 433\/1-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,7]]},"DOI":"10.1145\/3372020.3391566","type":"proceedings-article","created":{"date-parts":[[2020,9,12]],"date-time":"2020-09-12T20:02:05Z","timestamp":1599940925000},"page":"77-86","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Relational Test Tables"],"prefix":"10.1145","author":[{"given":"Alexander","family":"Weigl","sequence":"first","affiliation":[{"name":"Karlsruhe Institute for Technology, Karlsruhe"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute for Technology, Karlsruhe"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suhyun","family":"Cha","sequence":"additional","affiliation":[{"name":"Technical University of Munich, Munich"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernhard","family":"Beckert","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute for Technology, Karlsruhe"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Birgit","family":"Vogel-Heuser","sequence":"additional","affiliation":[{"name":"Technical University of Munich, Munich"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Juan Manuel Crespo, and C\u00e9sar Kunz","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe , Juan Manuel Crespo, and C\u00e9sar Kunz . 2011 . Relational Verification Using Product Programs. In FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings (Lecture Notes in Computer Science), Michael J. Butler and Wolfram Schulte (Eds.), Vol. 6664 . Springer , 200--214. https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17 10.1007\/978-3-642-21437-0_17 Gilles Barthe, Juan Manuel Crespo, and C\u00e9sar Kunz. 2011. Relational Verification Using Product Programs. In FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings (Lecture Notes in Computer Science), Michael J. Butler and Wolfram Schulte (Eds.), Vol. 6664. Springer, 200--214. https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17"},{"key":"e_1_3_2_1_2_1","volume-title":"Verifying Relational Properties using Trace Logic. CoRR abs\/1906.09899","author":"Barthe Gilles","year":"2019","unstructured":"Gilles Barthe , Renate Eilers , Pamina Georgiou , Bernhard Gleiss , Laura Kov\u00e1cs , and Matteo Maffei . 2019. Verifying Relational Properties using Trace Logic. CoRR abs\/1906.09899 ( 2019 ). arXiv:1906.09899 http:\/\/arxiv.org\/abs\/1906.09899 Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kov\u00e1cs, and Matteo Maffei. 2019. Verifying Relational Properties using Trace Logic. CoRR abs\/1906.09899 (2019). arXiv:1906.09899 http:\/\/arxiv.org\/abs\/1906.09899"},{"key":"e_1_3_2_1_3_1","volume-title":"IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings (Lecture Notes in Computer Science), Nadia Polikarpova and Steve Schneider (Eds.)","volume":"10510","author":"Beckert Bernhard","year":"2017","unstructured":"Bernhard Beckert , Suhyun Cha , Mattias Ulbrich , Birgit Vogel-Heuser , and Alexander Weigl . 2017 . Generalised Test Tables: A Practical Specification Language for Reactive Systems. In Integrated Formal Methods - 13th International Conference , IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings (Lecture Notes in Computer Science), Nadia Polikarpova and Steve Schneider (Eds.) , Vol. 10510 . Springer, 129--144. https:\/\/doi.org\/10.1007\/978-3-319-66845-1_9 10.1007\/978-3-319-66845-1_9 Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel-Heuser, and Alexander Weigl. 2017. Generalised Test Tables: A Practical Specification Language for Reactive Systems. In Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings (Lecture Notes in Computer Science), Nadia Polikarpova and Steve Schneider (Eds.), Vol. 10510. Springer, 129--144. https:\/\/doi.org\/10.1007\/978-3-319-66845-1_9"},{"key":"e_1_3_2_1_4_1","volume-title":"ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings (Lecture Notes in Computer Science), Michael J. Butler, Sylvain Conchon, and Fatiha Za\u00efdi (Eds.)","volume":"9407","author":"Beckert Bernhard","year":"2015","unstructured":"Bernhard Beckert , Mattias Ulbrich , Birgit Vogel-Heuser , and Alexander Weigl . 2015 . Regression Verification for Programmable Logic Controller Software. In Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods , ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings (Lecture Notes in Computer Science), Michael J. Butler, Sylvain Conchon, and Fatiha Za\u00efdi (Eds.) , Vol. 9407 . Springer, 234--251. https:\/\/doi.org\/10.1007\/978-3-319-25423-4_15 10.1007\/978-3-319-25423-4_15 Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, and Alexander Weigl. 2015. Regression Verification for Programmable Logic Controller Software. In Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings (Lecture Notes in Computer Science), Michael J. Butler, Sylvain Conchon, and Fatiha Za\u00efdi (Eds.), Vol. 9407. Springer, 234--251. https:\/\/doi.org\/10.1007\/978-3-319-25423-4_15"},{"key":"e_1_3_2_1_5_1","volume-title":"Pascale Le Gall, and Virgile Prevosto","author":"Blatter Lionel","year":"2017","unstructured":"Lionel Blatter , Nikolai Kosmatov , Pascale Le Gall, and Virgile Prevosto . 2017 . RPP : Automatic Proof of Relational Properties by Self-composition. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I (Lecture Notes in Computer Science), Axel Legay and Tiziana Margaria (Eds .), Vol. 10205 . 391--397. https:\/\/doi.org\/10.1007\/978-3-662-54577-5_22 10.1007\/978-3-662-54577-5_22 Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, and Virgile Prevosto. 2017. RPP: Automatic Proof of Relational Properties by Self-composition. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I (Lecture Notes in Computer Science), Axel Legay and Tiziana Margaria (Eds.), Vol. 10205. 391--397. https:\/\/doi.org\/10.1007\/978-3-662-54577-5_22"},{"key":"e_1_3_2_1_6_1","volume-title":"7th International Conference, FMCAD 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings. IEEE Computer Society, 173--180","author":"Aaron","year":"2007","unstructured":"Aaron R. Bradley and Zohar Manna. 2007. Checking Safety by Inductive Generalization of Counterexamples to Induction. In Formal Methods in Computer-Aided Design , 7th International Conference, FMCAD 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings. IEEE Computer Society, 173--180 . https:\/\/doi.org\/10.1109\/FAMCAD. 2007 .15 10.1109\/FAMCAD.2007.15 Aaron R. Bradley and Zohar Manna. 2007. Checking Safety by Inductive Generalization of Counterexamples to Induction. In Formal Methods in Computer-Aided Design, 7th International Conference, FMCAD 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings. IEEE Computer Society, 173--180. https:\/\/doi.org\/10.1109\/FAMCAD.2007.15"},{"volume-title":"Computer Aided Verification (CAV) (LNCS 8559)","author":"Cavada Roberto","key":"e_1_3_2_1_7_1","unstructured":"Roberto Cavada , Alessandro Cimatti , Michele Dorigatti , Alberto Griggio , Alessandro Mariotti , Andrea Micheli , Sergio Mover , Marco Roveri , and Stefano Tonetta . 2014. The nuXmv Symbolic Model Checker . In Computer Aided Verification (CAV) (LNCS 8559) . Springer , 334--342. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. 2014. The nuXmv Symbolic Model Checker. In Computer Aided Verification (CAV) (LNCS 8559). Springer, 334--342."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1515\/auto-2018-0028"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_2_1_10_1","volume-title":"Hyperproperties. In Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008","author":"Michael","year":"2008","unstructured":"Michael R. Clarkson and Fred B. Schneider. 2008 . Hyperproperties. In Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008 , Pittsburgh, Pennsylvania, USA , 23-25 June 2008 . IEEE Computer Society, 51--65. https:\/\/doi.org\/10.1109\/CSF.2008.7 10.1109\/CSF.2008.7 Michael R. Clarkson and Fred B. Schneider. 2008. Hyperproperties. In Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008. IEEE Computer Society, 51--65. https:\/\/doi.org\/10.1109\/CSF.2008.7"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2016.7733717"},{"key":"e_1_3_2_1_14_1","volume-title":"Schmitt","author":"Scheben Christoph","year":"2014","unstructured":"Christoph Scheben and Peter H . Schmitt . 2014 . Efficient Self-composition for Weakest Precondition Calculi. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings (Lecture Notes in Computer Science), Cliff B.Jones, Pekka Pihlajasaari, and Jun Sun (Eds.), Vol. 8442 . Springer , 579--594. https:\/\/doi.org\/10.1007\/978-3-319-06410-9_39 10.1007\/978-3-319-06410-9_39 Christoph Scheben and Peter H. Schmitt. 2014. Efficient Self-composition for Weakest Precondition Calculi. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings (Lecture Notes in Computer Science), Cliff B.Jones, Pekka Pihlajasaari, and Jun Sun (Eds.), Vol. 8442. Springer, 579--594. https:\/\/doi.org\/10.1007\/978-3-319-06410-9_39"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISAM.2016.7750714"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2729973"}],"event":{"name":"FormaliSE '20: 8th International Conference on Formal Methods in Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Seoul Republic of Korea","acronym":"FormaliSE '20"},"container-title":["Proceedings of the 8th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372020.3391566","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372020.3391566","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:19Z","timestamp":1750203859000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372020.3391566"}},"subtitle":["A Practical Specification Language for Evolution and Security"],"short-title":[],"issued":{"date-parts":[[2020,10,7]]},"references-count":15,"alternative-id":["10.1145\/3372020.3391566","10.1145\/3372020"],"URL":"https:\/\/doi.org\/10.1145\/3372020.3391566","relation":{},"subject":[],"published":{"date-parts":[[2020,10,7]]},"assertion":[{"value":"2020-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}