Cristiá, Maximiliano; De Luca, Guido; Luna, Carlos An automatically verified prototype of the Android permissions system. (English) Zbl 07702723 J. Autom. Reasoning 67, No. 2, Paper No. 17, 24 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Cristiá} et al., J. Autom. Reasoning 67, No. 2, Paper No. 17, 24 p. (2023; Zbl 07702723) Full Text: DOI arXiv
Baxter, James; Cavalcanti, Ana; Gazda, Maciej; Hierons, Robert M. Testing using CSP models: time, inputs, and outputs. (English) Zbl 07672676 ACM Trans. Comput. Log. 24, No. 2, Paper No. 17, 40 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{J. Baxter} et al., ACM Trans. Comput. Log. 24, No. 2, Paper No. 17, 40 p. (2023; Zbl 07672676) Full Text: DOI
Silva, Luciano; Oliveira, Marcel Automatic generation of verified concurrent hardware using VHDL. (English) Zbl 1528.68053 Lima, Lucas (ed.) et al., Formal methods: foundations and applications. 25th Brazilian symposium, SBMF 2022, virtual event, December 6–9, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13768, 55-72 (2022). MSC: 68N15 68Q60 68Q85 PDFBibTeX XMLCite \textit{L. Silva} and \textit{M. Oliveira}, Lect. Notes Comput. Sci. 13768, 55--72 (2022; Zbl 1528.68053) Full Text: DOI
Bischopink, Christopher; Olderog, Ernst-Rüdiger Spatial and timing properties in highway traffic. (English) Zbl 07719828 Seidl, Helmut (ed.) et al., Theoretical aspects of computing – ICTAC 2022. 19th international colloquium, Tbilisi, Georgia, September 27–29, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13572, 114-131 (2022). MSC: 68Qxx PDFBibTeX XMLCite \textit{C. Bischopink} and \textit{E.-R. Olderog}, Lect. Notes Comput. Sci. 13572, 114--131 (2022; Zbl 07719828) Full Text: DOI
Akgün, Özgür; Frisch, Alan M.; Gent, Ian P.; Jefferson, Christopher; Miguel, Ian; Nightingale, Peter Conjure: automatic generation of constraint models from problem specifications. (English) Zbl 07570882 Artif. Intell. 310, Article ID 103751, 27 p. (2022). MSC: 68Txx PDFBibTeX XMLCite \textit{Ö. Akgün} et al., Artif. Intell. 310, Article ID 103751, 27 p. (2022; Zbl 07570882) Full Text: DOI
Baxter, James; Ribeiro, Pedro; Cavalcanti, Ana Sound reasoning in tock-CSP. (English) Zbl 1483.68223 Acta Inf. 59, No. 1, 125-162 (2022); correction ibid. 59, No. 2-3, 283 (2022). MSC: 68Q85 PDFBibTeX XMLCite \textit{J. Baxter} et al., Acta Inf. 59, No. 1, 125--162 (2022; Zbl 1483.68223) Full Text: DOI
Alshareef, Hanaa; Stucki, Sandro; Schneider, Gerardo Refining privacy-aware data flow diagrams. (English) Zbl 1522.68188 Calinescu, Radu (ed.) et al., Software engineering and formal methods. 19th international conference, SEFM 2021, virtual event, December 6–10, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13085, 121-140 (2021). MSC: 68P27 PDFBibTeX XMLCite \textit{H. Alshareef} et al., Lect. Notes Comput. Sci. 13085, 121--140 (2021; Zbl 1522.68188) Full Text: DOI
Dovier, Agostino; Formisano, Andrea; Pontelli, Enrico; Tardivo, Fabio {CUDA}: set constraints on GPUs. (English) Zbl 1490.68080 Rend. Ist. Mat. Univ. Trieste 53, Paper No. 24, 27 p. (2021). MSC: 68N30 03B70 03E75 68N17 68W10 PDFBibTeX XMLCite \textit{A. Dovier} et al., Rend. Ist. Mat. Univ. Trieste 53, Paper No. 24, 27 p. (2021; Zbl 1490.68080) Full Text: DOI
Cristiá, Maximiliano; Rossi, Gianfranco \(\{\mathit{log}\}\): set formulas as programs. (English) Zbl 1490.68079 Rend. Ist. Mat. Univ. Trieste 53, Paper No. 23, 24 p. (2021). MSC: 68N30 03B70 03E20 03E75 68N15 68N17 68Q60 68V15 PDFBibTeX XMLCite \textit{M. Cristiá} and \textit{G. Rossi}, Rend. Ist. Mat. Univ. Trieste 53, Paper No. 23, 24 p. (2021; Zbl 1490.68079) Full Text: DOI arXiv
Leuschel, Michael Spot the difference: a detailed comparison between B and Event-B. (English) Zbl 07495058 Raschke, Alexander (ed.) et al., Logic, computation and rigorous methods. Essays dedicated to Egon Börger on the occasion of his 75th birthday. Cham: Springer. Lect. Notes Comput. Sci. 12750, 147-172 (2021). MSC: 68-XX 03-XX PDFBibTeX XMLCite \textit{M. Leuschel}, Lect. Notes Comput. Sci. 12750, 147--172 (2021; Zbl 07495058) Full Text: DOI
Banach, Richard; Zhu, Huibiao Moded and continuous abstract state machines. (English) Zbl 07495052 Raschke, Alexander (ed.) et al., Logic, computation and rigorous methods. Essays dedicated to Egon Börger on the occasion of his 75th birthday. Cham: Springer. Lect. Notes Comput. Sci. 12750, 29-62 (2021). MSC: 68-XX 03-XX PDFBibTeX XMLCite \textit{R. Banach} and \textit{H. Zhu}, Lect. Notes Comput. Sci. 12750, 29--62 (2021; Zbl 07495052) Full Text: DOI
Aït-Ameur, Yamine; Laleau, Régine; Méry, Dominique; Singh, Neeraj Kumar Towards leveraging domain knowledge in state-based formal methods. (English) Zbl 07495050 Raschke, Alexander (ed.) et al., Logic, computation and rigorous methods. Essays dedicated to Egon Börger on the occasion of his 75th birthday. Cham: Springer. Lect. Notes Comput. Sci. 12750, 1-13 (2021). MSC: 68-XX 03-XX PDFBibTeX XMLCite \textit{Y. Aït-Ameur} et al., Lect. Notes Comput. Sci. 12750, 1--13 (2021; Zbl 07495050) Full Text: DOI
Cristiá, Maximiliano; Rossi, Gianfranco An automatically verified prototype of the Tokeneer ID station specification. (English) Zbl 07461267 J. Autom. Reasoning 65, No. 8, 1125-1151 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Cristiá} and \textit{G. Rossi}, J. Autom. Reasoning 65, No. 8, 1125--1151 (2021; Zbl 07461267) Full Text: DOI arXiv
Foster, Simon; Nemouchi, Yakoub; Gleirscher, Mario; Wei, Ran; Kelly, Tim Integration of formal proof into unified assurance cases with Isabelle/SACM. (English) Zbl 1522.68717 Formal Asp. Comput. 33, No. 6, 855-884 (2021). MSC: 68V15 68V20 PDFBibTeX XMLCite \textit{S. Foster} et al., Formal Asp. Comput. 33, No. 6, 855--884 (2021; Zbl 1522.68717) Full Text: DOI arXiv
Cristiá, Maximiliano; Rossi, Gianfranco Automated reasoning with restricted intensional sets. (English) Zbl 07432188 J. Autom. Reasoning 65, No. 6, 809-890 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Cristiá} and \textit{G. Rossi}, J. Autom. Reasoning 65, No. 6, 809--890 (2021; Zbl 07432188) Full Text: DOI arXiv
Foster, Simon; Ye, Kangfeng; Cavalcanti, Ana; Woodcock, Jim Automated verification of reactive and concurrent programs by calculation. (English) Zbl 1518.68206 J. Log. Algebr. Methods Program. 121, Article ID 100681, 34 p. (2021). MSC: 68Q60 68N30 68Q85 PDFBibTeX XMLCite \textit{S. Foster} et al., J. Log. Algebr. Methods Program. 121, Article ID 100681, 34 p. (2021; Zbl 1518.68206) Full Text: DOI arXiv
Cristiá, Maximiliano; Rossi, Gianfranco Automated proof of Bell-LaPadula security properties. (English) Zbl 07356979 J. Autom. Reasoning 65, No. 4, 463-478 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Cristiá} and \textit{G. Rossi}, J. Autom. Reasoning 65, No. 4, 463--478 (2021; Zbl 07356979) Full Text: DOI arXiv
Jackson, Marcel; Stokes, Tim Override and update. (English) Zbl 1454.08004 J. Pure Appl. Algebra 225, No. 3, Article ID 106532, 17 p. (2021). MSC: 08A70 03B35 20M20 03B70 68V15 PDFBibTeX XMLCite \textit{M. Jackson} and \textit{T. Stokes}, J. Pure Appl. Algebra 225, No. 3, Article ID 106532, 17 p. (2021; Zbl 1454.08004) Full Text: DOI arXiv
Ribeiro, Pedro A unary semigroup trace algebra. (English) Zbl 07578347 Fahrenberg, Uli (ed.) et al., Relational and algebraic methods in computer science. 18th international conference, RAMiCS 2020, Palaiseau, France, October 26–29, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12062, 270-285 (2020). MSC: 68Qxx PDFBibTeX XMLCite \textit{P. Ribeiro}, Lect. Notes Comput. Sci. 12062, 270--285 (2020; Zbl 07578347) Full Text: DOI Link
Guttmann, Walter Verifying the correctness of disjoint-set forests with Kleene relation algebras. (English) Zbl 07578339 Fahrenberg, Uli (ed.) et al., Relational and algebraic methods in computer science. 18th international conference, RAMiCS 2020, Palaiseau, France, October 26–29, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12062, 134-151 (2020). MSC: 68Qxx PDFBibTeX XMLCite \textit{W. Guttmann}, Lect. Notes Comput. Sci. 12062, 134--151 (2020; Zbl 07578339) Full Text: DOI
Lahouij, Aida; Hamel, Lazhar; Graiet, Mohamed; el Ayeb, Béchir An Event-B based approach for cloud composite services verification. (English) Zbl 1458.68014 Formal Asp. Comput. 32, No. 4-6, 361-393 (2020). MSC: 68M11 68Q60 PDFBibTeX XMLCite \textit{A. Lahouij} et al., Formal Asp. Comput. 32, No. 4--6, 361--393 (2020; Zbl 1458.68014) Full Text: DOI
Kahl, Wolfram Calculational relation-algebraic proofs in the teaching tool CalcCheck. (English) Zbl 1462.68217 J. Log. Algebr. Methods Program. 117, Article ID 100581, 39 p. (2020). MSC: 68V15 97U70 PDFBibTeX XMLCite \textit{W. Kahl}, J. Log. Algebr. Methods Program. 117, Article ID 100581, 39 p. (2020; Zbl 1462.68217) Full Text: DOI
Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank Unifying theories of reactive design contracts. (English) Zbl 1436.68195 Theor. Comput. Sci. 802, 105-140 (2020). MSC: 68Q60 68Q55 68V15 PDFBibTeX XMLCite \textit{S. Foster} et al., Theor. Comput. Sci. 802, 105--140 (2020; Zbl 1436.68195) Full Text: DOI arXiv Link
Apt, Krzysztof R.; Olderog, Ernst-Rüdiger Fifty years of Hoare’s logic. (English) Zbl 1427.68008 Formal Asp. Comput. 31, No. 6, 751-807 (2019). MSC: 68-03 03B70 68N30 68Q55 PDFBibTeX XMLCite \textit{K. R. Apt} and \textit{E.-R. Olderog}, Formal Asp. Comput. 31, No. 6, 751--807 (2019; Zbl 1427.68008) Full Text: DOI arXiv Link
Lin, Yuhui; Bundy, Alan; Grov, Gudmund; Maclean, Ewen Automating Event-B invariant proofs by rippling and proof patching. (English) Zbl 1425.68077 Formal Asp. Comput. 31, No. 1, 95-129 (2019). MSC: 68N30 68Q60 68T15 PDFBibTeX XMLCite \textit{Y. Lin} et al., Formal Asp. Comput. 31, No. 1, 95--129 (2019; Zbl 1425.68077) Full Text: DOI
Ribeiro, Pedro; Cavalcanti, Ana Angelic processes for CSP via the UTP. (English) Zbl 1410.68236 Theor. Comput. Sci. 756, 19-63 (2019). MSC: 68Q60 68Q55 68Q85 PDFBibTeX XMLCite \textit{P. Ribeiro} and \textit{A. Cavalcanti}, Theor. Comput. Sci. 756, 19--63 (2019; Zbl 1410.68236) Full Text: DOI Link
Brattka, Vasco (ed.); Downey, Rodney G. (ed.); Knight, Julia F. (ed.); Lempp, Steffen (ed.) Computability theory. Abstracts from the workshop held January 7–13, 2018. (English) Zbl 1409.00073 Oberwolfach Rep. 15, No. 1, 5-41 (2018). MSC: 00B05 00B25 03Dxx 03C57 68Q30 03-06 PDFBibTeX XMLCite \textit{V. Brattka} (ed.) et al., Oberwolfach Rep. 15, No. 1, 5--41 (2018; Zbl 1409.00073) Full Text: DOI
Joosten, Stef Relation algebra as programming language using the Ampersand compiler. (English) Zbl 1400.68045 J. Log. Algebr. Methods Program. 100, 113-129 (2018). MSC: 68N15 68N20 PDFBibTeX XMLCite \textit{S. Joosten}, J. Log. Algebr. Methods Program. 100, 113--129 (2018; Zbl 1400.68045) Full Text: DOI
Joosten, Sebastiaan J. C. Finding models through graph saturation. (English) Zbl 1401.68043 J. Log. Algebr. Methods Program. 100, 98-112 (2018). MSC: 68N30 03B70 68Q42 PDFBibTeX XMLCite \textit{S. J. C. Joosten}, J. Log. Algebr. Methods Program. 100, 98--112 (2018; Zbl 1401.68043) Full Text: DOI arXiv
Schwammberger, Maike An abstract model for proving safety of autonomous urban traffic. (English) Zbl 1400.68126 Theor. Comput. Sci. 744, 143-169 (2018). MSC: 68Q60 03B70 68Q45 90B20 PDFBibTeX XMLCite \textit{M. Schwammberger}, Theor. Comput. Sci. 744, 143--169 (2018; Zbl 1400.68126) Full Text: DOI
Smith, Graeme; Winter, Kirsten Relating trace refinement and linearizability. (English) Zbl 1377.68151 Formal Asp. Comput. 29, No. 6, 935-950 (2017). MSC: 68Q85 PDFBibTeX XMLCite \textit{G. Smith} and \textit{K. Winter}, Formal Asp. Comput. 29, No. 6, 935--950 (2017; Zbl 1377.68151) Full Text: DOI
Colvin, Robert J.; Hayes, Ian J.; Meinicke, Larissa A. Designing a semantic model for a wide-spectrum language with concurrency. (English) Zbl 1375.68036 Formal Asp. Comput. 29, No. 5, 853-875 (2017). MSC: 68N15 68Q55 68Q85 PDFBibTeX XMLCite \textit{R. J. Colvin} et al., Formal Asp. Comput. 29, No. 5, 853--875 (2017; Zbl 1375.68036) Full Text: DOI arXiv
Ahrendt, Wolfgang; Chimento, Jesús Mauricio; Pace, Gordon J.; Schneider, Gerardo Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. (English) Zbl 1370.68195 Form. Methods Syst. Des. 51, No. 1, 200-265 (2017). MSC: 68Q60 68N19 68N30 PDFBibTeX XMLCite \textit{W. Ahrendt} et al., Form. Methods Syst. Des. 51, No. 1, 200--265 (2017; Zbl 1370.68195) Full Text: DOI
Joosten, Stef Software development in relation algebra with Ampersand. (English) Zbl 1486.68042 Höfner, Peter (ed.) et al., Relational and algebraic methods in computer science. 16th international conference, RAMiCS 2017, Lyon, France, May 15–18, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10226, 177-192 (2017). MSC: 68N30 03G15 68N20 68P15 PDFBibTeX XMLCite \textit{S. Joosten}, Lect. Notes Comput. Sci. 10226, 177--192 (2017; Zbl 1486.68042) Full Text: DOI
Ribeiro, Pedro; Cavalcanti, Ana; Woodcock, Jim A stepwise approach to linking theories. (English) Zbl 1483.68090 Bowen, Jonathan P. (ed.) et al., Unifying theories of programming. 6th international symposium, UTP 2016, Reykjavik, Iceland, June 4–5, 2016. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 10134, 134-154 (2017). MSC: 68N30 68Q55 PDFBibTeX XMLCite \textit{P. Ribeiro} et al., Lect. Notes Comput. Sci. 10134, 134--154 (2017; Zbl 1483.68090) Full Text: DOI
Jifeng, He A new roadmap for linking theories of programming. (English) Zbl 1483.68081 Bowen, Jonathan P. (ed.) et al., Unifying theories of programming. 6th international symposium, UTP 2016, Reykjavik, Iceland, June 4–5, 2016. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 10134, 26-43 (2017). MSC: 68N30 PDFBibTeX XMLCite \textit{H. Jifeng}, Lect. Notes Comput. Sci. 10134, 26--43 (2017; Zbl 1483.68081) Full Text: DOI
Bjørner, Dines Manifest domains: analysis and description. (English) Zbl 1358.68052 Formal Asp. Comput. 29, No. 2, 175-225 (2017). MSC: 68N01 PDFBibTeX XMLCite \textit{D. Bjørner}, Formal Asp. Comput. 29, No. 2, 175--225 (2017; Zbl 1358.68052) Full Text: DOI Link
Smith, Graeme Model checking simulation rules for linearizability. (English) Zbl 1390.68439 De Nicola, Rocco (ed.) et al., Software engineering and formal methods. 14th international conference, SEFM 2016, held as part of STAF 2016, Vienna, Austria, July 4–8, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-41590-1/pbk; 978-3-319-41591-8/ebook). Lecture Notes in Computer Science 9763, 188-203 (2016). MSC: 68Q60 68Q85 PDFBibTeX XMLCite \textit{G. Smith}, Lect. Notes Comput. Sci. 9763, 188--203 (2016; Zbl 1390.68439) Full Text: DOI
Ameloot, Tom J.; Van den Bussche, Jan; Marczak, William R.; Alvaro, Peter; Hellerstein, Joseph M. Putting logic-based distributed systems on stable grounds. (English) Zbl 1379.68124 Theory Pract. Log. Program. 16, No. 4, 378-417 (2016). MSC: 68Q10 68N17 68Q55 PDFBibTeX XMLCite \textit{T. J. Ameloot} et al., Theory Pract. Log. Program. 16, No. 4, 378--417 (2016; Zbl 1379.68124) Full Text: DOI arXiv
Hilscher, Martin; Schwammberger, Maike An abstract model for proving safety of autonomous urban traffic. (English) Zbl 1401.68199 Sampaio, Augusto (ed.) et al., Theoretical aspects of computing – ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24–31, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-46749-8/pbk; 978-3-319-46750-4/ebook). Lecture Notes in Computer Science 9965, 274-292 (2016). MSC: 68Q60 03B70 68Q45 90B20 PDFBibTeX XMLCite \textit{M. Hilscher} and \textit{M. Schwammberger}, Lect. Notes Comput. Sci. 9965, 274--292 (2016; Zbl 1401.68199) Full Text: DOI
Cavalcanti, Ana; Woodcock, Jim; Amálio, Nuno Behavioural models for FMI co-simulations. (English) Zbl 1482.68135 Sampaio, Augusto (ed.) et al., Theoretical aspects of computing – ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24–31, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9965, 255-273 (2016). MSC: 68Q60 68Q55 68Q85 PDFBibTeX XMLCite \textit{A. Cavalcanti} et al., Lect. Notes Comput. Sci. 9965, 255--273 (2016; Zbl 1482.68135) Full Text: DOI Link
Arthan, Rob On definitions of constants and types in HOL. (English) Zbl 1356.68173 J. Autom. Reasoning 56, No. 3, 205-219 (2016). MSC: 68T15 PDFBibTeX XMLCite \textit{R. Arthan}, J. Autom. Reasoning 56, No. 3, 205--219 (2016; Zbl 1356.68173) Full Text: DOI
Colvin, Robert J. Modelling and analysing neural networks using a hybrid process algebra. (English) Zbl 1336.92005 Theor. Comput. Sci. 623, 15-64 (2016). MSC: 92B20 68Q85 PDFBibTeX XMLCite \textit{R. J. Colvin}, Theor. Comput. Sci. 623, 15--64 (2016; Zbl 1336.92005) Full Text: DOI
Cristiá, Maximiliano; Rossi, Gianfranco; Frydman, Claudia Adding partial functions to constraint logic programming with sets. (English) Zbl 1379.68053 Theory Pract. Log. Program. 15, No. 4-5, 651-665 (2015). MSC: 68N17 68Q60 68T20 PDFBibTeX XMLCite \textit{M. Cristiá} et al., Theory Pract. Log. Program. 15, No. 4--5, 651--665 (2015; Zbl 1379.68053) Full Text: DOI arXiv
Cheng, Shu; Woodcock, Jim; D’Souza, Deepak Using formal reasoning on a model of tasks for FreeRTOS. (English) Zbl 1328.68044 Formal Asp. Comput. 27, No. 1, 167-192 (2015). MSC: 68N25 68Q60 PDFBibTeX XMLCite \textit{S. Cheng} et al., Formal Asp. Comput. 27, No. 1, 167--192 (2015; Zbl 1328.68044) Full Text: DOI
Castro, Pablo F.; Aguirre, Nazareno; Pombo, Carlos L.; Maibaum, T. S. E. Categorical foundations for structured specifications in \(\mathsf{Z}\). (English) Zbl 1385.68023 Formal Asp. Comput. 27, No. 5-6, 831-865 (2015). Reviewer: Răzvan Diaconescu (Ploiesti) MSC: 68Q65 PDFBibTeX XMLCite \textit{P. F. Castro} et al., Formal Asp. Comput. 27, No. 5--6, 831--865 (2015; Zbl 1385.68023) Full Text: DOI
Fränzle, Martin; Hansen, Michael R.; Ody, Heinrich No need knowing numerous neighbours. Towards a realizable interpretation of MLSL. (English) Zbl 1444.68181 Meyer, Roland (ed.) et al., Correct system design. Symposium in honor of Ernst-Rüdiger Olderog on the occasion of his 60th birthday, Oldenburg, Germany, September 8–9, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9360, 152-171 (2015). MSC: 68T27 68T20 90B20 PDFBibTeX XMLCite \textit{M. Fränzle} et al., Lect. Notes Comput. Sci. 9360, 152--171 (2015; Zbl 1444.68181) Full Text: DOI
Zeyda, Frank; Cavalcanti, Ana Laws of mission-based programming. (English) Zbl 1331.68054 Formal Asp. Comput. 27, No. 2, 423-472 (2015). MSC: 68N30 68N19 PDFBibTeX XMLCite \textit{F. Zeyda} and \textit{A. Cavalcanti}, Formal Asp. Comput. 27, No. 2, 423--472 (2015; Zbl 1331.68054) Full Text: DOI Link
Baumeister, Hubert; Bettaz, Mohamed; Maouche, Mourad; Mosteghanemi, M’hamed An institution for Object-Z with inheritance and polymorphism. (English) Zbl 1453.68043 De Nicola, Rocco (ed.) et al., Software, services, and systems. Essays dedicated to Martin Wirsing on the occasion of his retirement from the chair of programming and software engineering, Munich, Germany, 2015. Essays. Cham: Springer. Lect. Notes Comput. Sci. 8950, 134-154 (2015). MSC: 68N30 68Q65 PDFBibTeX XMLCite \textit{H. Baumeister} et al., Lect. Notes Comput. Sci. 8950, 134--154 (2015; Zbl 1453.68043) Full Text: DOI
Berghammer, Rudolf; Fischer, Sebastian Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures. (English) Zbl 1329.68062 J. Log. Algebr. Methods Program. 84, No. 3, 341-358 (2015). MSC: 68N18 03G20 05C20 05C85 PDFBibTeX XMLCite \textit{R. Berghammer} and \textit{S. Fischer}, J. Log. Algebr. Methods Program. 84, No. 3, 341--358 (2015; Zbl 1329.68062) Full Text: DOI
Dang, Han-Hing; Möller, Bernhard B. Extended transitive separation logic. (English) Zbl 1330.03071 J. Log. Algebr. Methods Program. 84, No. 3, 303-325 (2015). MSC: 03B70 03G25 68P05 PDFBibTeX XMLCite \textit{H.-H. Dang} and \textit{B. B. Möller}, J. Log. Algebr. Methods Program. 84, No. 3, 303--325 (2015; Zbl 1330.03071) Full Text: DOI
Cavalcanti, Ana; Gaudel, Marie-Claude Test selection for traces refinement. (English) Zbl 1302.68086 Theor. Comput. Sci. 563, 1-42 (2015). MSC: 68N30 PDFBibTeX XMLCite \textit{A. Cavalcanti} and \textit{M.-C. Gaudel}, Theor. Comput. Sci. 563, 1--42 (2015; Zbl 1302.68086) Full Text: DOI
Liu, Jie; Liu, Jing A formal framework for Hybrid Event B. (English) Zbl 1351.68166 Xue, Jinyun (ed.) et al., Proceedings of the 6th international workshop on harnessing theories for tool support in software (TTSS 2013), Nanchang, China, October 27, 2013. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 309, 3-12, electronic only (2014). MSC: 68Q60 03B70 68Q45 68Q55 PDFBibTeX XMLCite \textit{J. Liu} and \textit{J. Liu}, Electron. Notes Theor. Comput. Sci. 309, 3--12 (2014; Zbl 1351.68166) Full Text: DOI
Derrick, John; Boiten, Eerke Relational concurrent refinement. III: Traces, partial relations and automata. (English) Zbl 1342.68227 Formal Asp. Comput. 26, No. 2, 407-432 (2014). MSC: 68Q85 68N30 68Q45 68Q60 PDFBibTeX XMLCite \textit{J. Derrick} and \textit{E. Boiten}, Formal Asp. Comput. 26, No. 2, 407--432 (2014; Zbl 1342.68227) Full Text: DOI
Boiten, Eerke A. Introducing extra operations in refinement. (English) Zbl 1342.68204 Formal Asp. Comput. 26, No. 2, 305-317 (2014). MSC: 68Q60 PDFBibTeX XMLCite \textit{E. A. Boiten}, Formal Asp. Comput. 26, No. 2, 305--317 (2014; Zbl 1342.68204) Full Text: DOI Link
Schneider, Steve; Treharne, Helen; Wehrheim, Heike The behavioural semantics of Event-B refinement. (English) Zbl 1342.68211 Formal Asp. Comput. 26, No. 2, 251-280 (2014). MSC: 68Q60 68Q55 PDFBibTeX XMLCite \textit{S. Schneider} et al., Formal Asp. Comput. 26, No. 2, 251--280 (2014; Zbl 1342.68211) Full Text: DOI Link
Banks, Michael J.; Jacob, Jeremy L. On integrating confidentiality and functionality in a formal method. (English) Zbl 1342.68191 Formal Asp. Comput. 26, No. 5, 963-992 (2014). MSC: 68Q55 68N30 68Q60 PDFBibTeX XMLCite \textit{M. J. Banks} and \textit{J. L. Jacob}, Formal Asp. Comput. 26, No. 5, 963--992 (2014; Zbl 1342.68191) Full Text: DOI
Cavalcanti, Ana; King, Steve; O’Halloran, Colin; Woodcock, Jim Test-data generation for control coverage by proof. (English) Zbl 1342.68206 Formal Asp. Comput. 26, No. 4, 795-823 (2014). MSC: 68Q60 PDFBibTeX XMLCite \textit{A. Cavalcanti} et al., Formal Asp. Comput. 26, No. 4, 795--823 (2014; Zbl 1342.68206) Full Text: DOI
Liu, Xi; Yang, Shaofa; Sanders, J. W. Compensation by design. (English) Zbl 1342.68136 Formal Asp. Comput. 26, No. 4, 623-676 (2014). MSC: 68Q10 68N30 68Q85 PDFBibTeX XMLCite \textit{X. Liu} et al., Formal Asp. Comput. 26, No. 4, 623--676 (2014; Zbl 1342.68136) Full Text: DOI
Colvin, Robert J. An operational semantics for object-oriented concepts based on the class hierarchy. (English) Zbl 1342.68057 Formal Asp. Comput. 26, No. 3, 491-535 (2014). MSC: 68N19 68Q55 68Q85 PDFBibTeX XMLCite \textit{R. J. Colvin}, Formal Asp. Comput. 26, No. 3, 491--535 (2014; Zbl 1342.68057) Full Text: DOI
Schellhorn, Gerhard; Derrick, John; Wehrheim, Heike A sound and complete proof technique for linearizability of concurrent data structures. (English) Zbl 1354.68066 ACM Trans. Comput. Log. 15, No. 4, Article No. 31, 37 p. (2014). MSC: 68P05 68Q60 68Q85 68T15 PDFBibTeX XMLCite \textit{G. Schellhorn} et al., ACM Trans. Comput. Log. 15, No. 4, Article No. 31, 37 p. (2014; Zbl 1354.68066) Full Text: DOI Link
Bouquet, Fabrice; Peureux, Fabien; Ambert, Fabrice Model-based testing for functional and security test generation. (English) Zbl 1448.68186 Aldini, Alessandro (ed.) et al., Foundations of security analysis and design VII. FOSAD 2012/2013 tutorial lectures. Berlin: Springer. Lect. Notes Comput. Sci. 8604, 1-33 (2014). MSC: 68M25 68M15 PDFBibTeX XMLCite \textit{F. Bouquet} et al., Lect. Notes Comput. Sci. 8604, 1--33 (2014; Zbl 1448.68186) Full Text: DOI
Furia, Carlo A.; Meyer, Bertrand; Velder, Sergey Loop invariants: analysis, classification, and examples. (English) Zbl 1305.68054 ACM Comput. Surv. 46, No. 3, Paper No. 34, 51 p. (2014). MSC: 68N30 68Q60 68-02 PDFBibTeX XMLCite \textit{C. A. Furia} et al., ACM Comput. Surv. 46, No. 3, Paper No. 34, 51 p. (2014; Zbl 1305.68054) Full Text: DOI arXiv
Bozzelli, Laura; van Ditmarsch, Hans; French, Tim; Hales, James; Pinchinat, Sophie Refinement modal logic. (English) Zbl 1309.68175 Inf. Comput. 239, 303-339 (2014). MSC: 68T27 03B45 PDFBibTeX XMLCite \textit{L. Bozzelli} et al., Inf. Comput. 239, 303--339 (2014; Zbl 1309.68175) Full Text: DOI arXiv
Freitas, Leo; Watson, Paul Formalizing workflows partitioning over federated clouds: multi-level security and costs. (English) Zbl 1452.68120 Int. J. Comput. Math. 91, No. 5, 881-906 (2014). MSC: 68Q60 68N18 68V15 PDFBibTeX XMLCite \textit{L. Freitas} and \textit{P. Watson}, Int. J. Comput. Math. 91, No. 5, 881--906 (2014; Zbl 1452.68120) Full Text: DOI
Honda, Kohei; Yoshida, Nobuko; Berger, Martin An observationally complete program logic for imperative higher-order functions. (English) Zbl 1358.68071 Theor. Comput. Sci. 517, 75-101 (2014). MSC: 68N30 03B70 PDFBibTeX XMLCite \textit{K. Honda} et al., Theor. Comput. Sci. 517, 75--101 (2014; Zbl 1358.68071) Full Text: DOI
Zeyda, Frank; Cavalcanti, Ana Higher-order UTP for a theory of methods. (English) Zbl 1452.68061 Wolff, Burkhart (ed.) et al., Unifying theories of programming. Fourth international symposium, UTP 2012, Paris, France, August 27–28, 2012. Revised selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 7681, 204-223 (2013). MSC: 68N30 68N19 68Q55 PDFBibTeX XMLCite \textit{F. Zeyda} and \textit{A. Cavalcanti}, Lect. Notes Comput. Sci. 7681, 204--223 (2013; Zbl 1452.68061) Full Text: DOI
Wei, Kun; Woodcock, Jim; Cavalcanti, Ana Circus Time with reactive designs. (English) Zbl 1452.68057 Wolff, Burkhart (ed.) et al., Unifying theories of programming. Fourth international symposium, UTP 2012, Paris, France, August 27–28, 2012. Revised selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 7681, 68-87 (2013). MSC: 68N30 68Q55 PDFBibTeX XMLCite \textit{K. Wei} et al., Lect. Notes Comput. Sci. 7681, 68--87 (2013; Zbl 1452.68057) Full Text: DOI
Foster, Simon; Woodcock, Jim Unifying theories of programming in Isabelle. (English) Zbl 1444.68049 Liu, Zhiming (ed.) et al., Unifying theories of programming and formal engineering methods. International training school on software engineering, held at ICTAC 2013, Shanghai, China, August 26–30, 2013. Advanced lectures. Berlin: Springer. Lect. Notes Comput. Sci. 8050, 109-155 (2013). MSC: 68N30 68Q55 68V15 68V20 PDFBibTeX XMLCite \textit{S. Foster} and \textit{J. Woodcock}, Lect. Notes Comput. Sci. 8050, 109--155 (2013; Zbl 1444.68049) Full Text: DOI Link
Dong, Ruzhen; Faber, Johannes; Ke, Wei; Liu, Zhiming rCOS: defining meanings of component-based software architectures. (English) Zbl 1444.68047 Liu, Zhiming (ed.) et al., Unifying theories of programming and formal engineering methods. International training school on software engineering, held at ICTAC 2013, Shanghai, China, August 26–30, 2013. Advanced lectures. Berlin: Springer. Lect. Notes Comput. Sci. 8050, 1-66 (2013). MSC: 68N30 PDFBibTeX XMLCite \textit{R. Dong} et al., Lect. Notes Comput. Sci. 8050, 1--66 (2013; Zbl 1444.68047) Full Text: DOI
Perna, Juan I.; George, Chris Model checking RAISE applicative specifications. (English) Zbl 1298.68065 Formal Asp. Comput. 25, No. 3, 365-388 (2013). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{J. I. Perna} and \textit{C. George}, Formal Asp. Comput. 25, No. 3, 365--388 (2013; Zbl 1298.68065) Full Text: DOI Link
Wei, Kun; Woodcock, Jim; Burns, Alan Modelling temporal behaviour in complex systems with Timebands. (English) Zbl 1291.68271 Form. Methods Syst. Des. 43, No. 3, 520-551 (2013). MSC: 68Q60 68N30 03B70 03B44 PDFBibTeX XMLCite \textit{K. Wei} et al., Form. Methods Syst. Des. 43, No. 3, 520--551 (2013; Zbl 1291.68271) Full Text: DOI Link
Cavalcanti, Ana; Zeyda, Frank; Wellings, Andy; Woodcock, Jim; Wei, Kun Safety-critical Java programs from Circus models. (English) Zbl 1285.68037 Real-Time Syst. 49, No. 5, 614-667 (2013). MSC: 68N30 PDFBibTeX XMLCite \textit{A. Cavalcanti} et al., Real-Time Syst. 49, No. 5, 614--667 (2013; Zbl 1285.68037) Full Text: DOI
Hilscher, Martin; Linker, Sven; Olderog, Ernst-Rüdiger Proving safety of traffic manoeuvres on country roads. (English) Zbl 1390.68429 Liu, Zhiming (ed.) et al., Theories of programming and formal methods. Essays dedicated to Jifeng He on the occasion of his 70th birthday. Berlin: Springer (ISBN 978-3-642-39697-7/pbk). Lecture Notes in Computer Science 8051, 196-212 (2013). MSC: 68Q60 03B44 90B20 PDFBibTeX XMLCite \textit{M. Hilscher} et al., Lect. Notes Comput. Sci. 8051, 196--212 (2013; Zbl 1390.68429) Full Text: DOI
Cavalcanti, Ana; Mota, Alexandre; Woodcock, Jim Simulink timed models for program verification. (English) Zbl 1390.68423 Liu, Zhiming (ed.) et al., Theories of programming and formal methods. Essays dedicated to Jifeng He on the occasion of his 70th birthday. Berlin: Springer (ISBN 978-3-642-39697-7/pbk). Lecture Notes in Computer Science 8051, 82-99 (2013). MSC: 68Q60 68U20 PDFBibTeX XMLCite \textit{A. Cavalcanti} et al., Lect. Notes Comput. Sci. 8051, 82--99 (2013; Zbl 1390.68423) Full Text: DOI
Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim Unifying theories in ProofPower-Z. (English) Zbl 1259.68035 Formal Asp. Comput. 25, No. 1, 133-158 (2013). MSC: 68N30 68Q60 68T15 PDFBibTeX XMLCite \textit{M. Oliveira} et al., Formal Asp. Comput. 25, No. 1, 133--158 (2013; Zbl 1259.68035) Full Text: DOI
Chen, Yifeng Semantic inheritance in unifying theories of programming. (English) Zbl 1259.68122 Formal Asp. Comput. 25, No. 1, 89-106 (2013). MSC: 68Q60 68Q55 68N30 PDFBibTeX XMLCite \textit{Y. Chen}, Formal Asp. Comput. 25, No. 1, 89--106 (2013; Zbl 1259.68122) Full Text: DOI
Leino, K. Rustan M.; Yessenov, Kuat Stepwise refinement of heap-manipulating code in Chalice. (English) Zbl 1259.68034 Formal Asp. Comput. 24, No. 4-6, 519-535 (2012). MSC: 68N30 PDFBibTeX XMLCite \textit{K. R. M. Leino} and \textit{K. Yessenov}, Formal Asp. Comput. 24, No. 4--6, 519--535 (2012; Zbl 1259.68034) Full Text: DOI Link
Derrick, John; Smith, Graeme Temporal-logic property preservation under Z refinement. (English) Zbl 1259.68032 Formal Asp. Comput. 24, No. 3, 393-416 (2012). MSC: 68N30 03B44 PDFBibTeX XMLCite \textit{J. Derrick} and \textit{G. Smith}, Formal Asp. Comput. 24, No. 3, 393--416 (2012; Zbl 1259.68032) Full Text: DOI
Ke, Wei; Li, Xiaoshan; Liu, Zhiming; Stolz, Volker RCOS: a formal model-driven engineering method for component-based software. (English) Zbl 1251.68078 Front. Comput. Sci. 6, No. 1, 17-39 (2012). MSC: 68N30 PDFBibTeX XMLCite \textit{W. Ke} et al., Front. Comput. Sci. 6, No. 1, 17--39 (2012; Zbl 1251.68078)
Borba, Paulo; Teixeira, Leopoldo; Gheyi, Rohit A theory of software product line refinement. (English) Zbl 1254.68072 Theor. Comput. Sci. 455, 2-30 (2012). MSC: 68N30 PDFBibTeX XMLCite \textit{P. Borba} et al., Theor. Comput. Sci. 455, 2--30 (2012; Zbl 1254.68072) Full Text: DOI
Crolard, T.; Polonowski, E. Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control. (English) Zbl 1259.03044 J. Log. Algebr. Program. 81, No. 3, 181-208 (2012). MSC: 03B70 68N18 68N30 68Q60 PDFBibTeX XMLCite \textit{T. Crolard} and \textit{E. Polonowski}, J. Log. Algebr. Program. 81, No. 3, 181--208 (2012; Zbl 1259.03044) Full Text: DOI arXiv
Miyazawa, Alvaro; Cavalcanti, Ana Refinement-oriented models of Stateflow charts. (English) Zbl 1243.68152 Sci. Comput. Program. 77, No. 10-11, 1151-1177 (2012). MSC: 68N30 68Q55 PDFBibTeX XMLCite \textit{A. Miyazawa} and \textit{A. Cavalcanti}, Sci. Comput. Program. 77, No. 10--11, 1151--1177 (2012; Zbl 1243.68152) Full Text: DOI
Chin, Wei-Ngan; David, Cristina; Nguyen, Huu Hai; Qin, Shengchao Automated verification of shape, size and bag properties via user-defined predicates in separation logic. (English) Zbl 1243.68148 Sci. Comput. Program. 77, No. 9, 1006-1036 (2012). MSC: 68N30 68Q60 68T15 03B70 PDFBibTeX XMLCite \textit{W.-N. Chin} et al., Sci. Comput. Program. 77, No. 9, 1006--1036 (2012; Zbl 1243.68148) Full Text: DOI
da Costa, Umberto Souza; Moreira, Anamaria Martins; Musicante, Martin A.; Souza Neto, Plácido A. JCML: A specification language for the runtime verification of Java card programs. (English) Zbl 1243.68137 Sci. Comput. Program. 77, No. 4, 533-550 (2012). MSC: 68N15 68N30 PDFBibTeX XMLCite \textit{U. S. da Costa} et al., Sci. Comput. Program. 77, No. 4, 533--550 (2012; Zbl 1243.68137) Full Text: DOI
Zeyda, Frank; Cavalcanti, Ana Mechanical reasoning about families of UTP theories. (English) Zbl 1243.68270 Sci. Comput. Program. 77, No. 4, 444-479 (2012). MSC: 68T15 68N15 68Q60 PDFBibTeX XMLCite \textit{F. Zeyda} and \textit{A. Cavalcanti}, Sci. Comput. Program. 77, No. 4, 444--479 (2012; Zbl 1243.68270) Full Text: DOI
Ruhroth, Thomas; Wehrheim, Heike Model evolution and refinement. (English) Zbl 1243.68156 Sci. Comput. Program. 77, No. 3, 270-289 (2012). MSC: 68N99 68Q60 PDFBibTeX XMLCite \textit{T. Ruhroth} and \textit{H. Wehrheim}, Sci. Comput. Program. 77, No. 3, 270--289 (2012; Zbl 1243.68156) Full Text: DOI
Hallerstede, Stefan; Leuschel, Michael Experiments in program verification using Event-B. (English) Zbl 1242.68067 Formal Asp. Comput. 24, No. 1, 97-125 (2012). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{S. Hallerstede} and \textit{M. Leuschel}, Formal Asp. Comput. 24, No. 1, 97--125 (2012; Zbl 1242.68067) Full Text: DOI
Zeyda, Frank; Oliveira, Marcel; Cavalcanti, Ana Mechanised support for sound refinement tactics. (English) Zbl 1242.68077 Formal Asp. Comput. 24, No. 1, 127-160 (2012). MSC: 68N30 68N19 68Q60 PDFBibTeX XMLCite \textit{F. Zeyda} et al., Formal Asp. Comput. 24, No. 1, 127--160 (2012; Zbl 1242.68077) Full Text: DOI
Cao, Zining; Wang, Hui Extending interface automata with Z notation. (English) Zbl 1353.68047 Arbab, Farhad (ed.) et al., Fundamentals of software engineering. 4th IPM international conference, FSEN 2011, Tehran, Iran, April 20–22, 2011. Revised selected papers. Berlin: Springer (ISBN 978-3-642-29319-1/pbk). Lecture Notes in Computer Science 7141, 359-367 (2012). MSC: 68N30 68Q45 68Q60 PDFBibTeX XMLCite \textit{Z. Cao} and \textit{H. Wang}, Lect. Notes Comput. Sci. 7141, 359--367 (2012; Zbl 1353.68047) Full Text: DOI
Bjørner, D. Domain science and engineering from computer science to the sciences of informatics. II: Science. (English. Russian original) Zbl 1298.68061 Cybern. Syst. Anal. 47, No. 2, 260-276 (2011); translation from Kibern. Sist. Anal. 2011, No. 2, 100-120 (2011). MSC: 68N30 PDFBibTeX XMLCite \textit{D. Bjørner}, Cybern. Syst. Anal. 47, No. 2, 260--276 (2011; Zbl 1298.68061); translation from Kibern. Sist. Anal. 2011, No. 2, 100--120 (2011) Full Text: DOI
Fu, Zheng; Smith, Graeme Property transformation under specification change. (English) Zbl 1267.68093 Front. Comput. Sci. China 5, No. 1, 1-13 (2011). MSC: 68N30 68Q60 03B70 PDFBibTeX XMLCite \textit{Z. Fu} and \textit{G. Smith}, Front. Comput. Sci. China 5, No. 1, 1--13 (2011; Zbl 1267.68093) Full Text: DOI
Perna, Juan; Woodcock, Jim; Sampaio, Augusto; Iyoda, Juliano Correct hardware synthesis. (English) Zbl 1234.68067 Acta Inf. 48, No. 7-8, 363-396 (2011). MSC: 68N20 68N15 68Q60 PDFBibTeX XMLCite \textit{J. Perna} et al., Acta Inf. 48, No. 7--8, 363--396 (2011; Zbl 1234.68067) Full Text: DOI
Cavalcanti, Ana; Gaudel, Marie-Claude Testing for refinement in Circus. (English) Zbl 1237.68059 Acta Inf. 48, No. 2, 97-147 (2011). MSC: 68N30 68N15 68Q55 PDFBibTeX XMLCite \textit{A. Cavalcanti} and \textit{M.-C. Gaudel}, Acta Inf. 48, No. 2, 97--147 (2011; Zbl 1237.68059) Full Text: DOI
Kahl, Wolfram The teaching tool CalcCheck: a proof-checker for Gries and Schneider’s “Logical approach to discrete math”. (English) Zbl 1350.68238 Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 216-230 (2011). MSC: 68T15 PDFBibTeX XMLCite \textit{W. Kahl}, Lect. Notes Comput. Sci. 7086, 216--230 (2011; Zbl 1350.68238) Full Text: DOI
Cavalcanti, Ana; Clayton, Phil; O’Halloran, Colin From control law diagrams to Ada via Circus. (English) Zbl 1226.68028 Formal Asp. Comput. 23, No. 4, 465-512 (2011). MSC: 68N30 68N15 PDFBibTeX XMLCite \textit{A. Cavalcanti} et al., Formal Asp. Comput. 23, No. 4, 465--512 (2011; Zbl 1226.68028) Full Text: DOI
Colvin, Robert J.; Hayes, Ian J. A semantics for behavior trees using CSP with specification commands. (English) Zbl 1220.68050 Sci. Comput. Program. 76, No. 10, 891-914 (2011). MSC: 68N30 68Q55 68Q85 PDFBibTeX XMLCite \textit{R. J. Colvin} and \textit{I. J. Hayes}, Sci. Comput. Program. 76, No. 10, 891--914 (2011; Zbl 1220.68050) Full Text: DOI
Wong, Peter Y. H.; Gibbons, Jeremy Formalisations and applications of BPMN. (English) Zbl 1213.68212 Sci. Comput. Program. 76, No. 8, 633-650 (2011). MSC: 68N30 68Q55 68Q85 PDFBibTeX XMLCite \textit{P. Y. H. Wong} and \textit{J. Gibbons}, Sci. Comput. Program. 76, No. 8, 633--650 (2011; Zbl 1213.68212) Full Text: DOI
Oliveira, Marcel; Zeyda, Frank; Cavalcanti, Ana A tactic language for refinement of state-rich concurrent specifications. (English) Zbl 1218.68101 Sci. Comput. Program. 76, No. 9, 792-833 (2011). MSC: 68Q60 68N15 68N30 PDFBibTeX XMLCite \textit{M. Oliveira} et al., Sci. Comput. Program. 76, No. 9, 792--833 (2011; Zbl 1218.68101) Full Text: DOI
Schellhorn, Gerhard Completeness of fair ASM refinement. (English) Zbl 1217.68065 Sci. Comput. Program. 76, No. 9, 756-773 (2011). MSC: 68N30 68Q85 68Q60 PDFBibTeX XMLCite \textit{G. Schellhorn}, Sci. Comput. Program. 76, No. 9, 756--773 (2011; Zbl 1217.68065) Full Text: DOI