Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike Mechanized proofs of opacity: a comparison of two techniques. (English) Zbl 1395.68186 Formal Asp. Comput. 30, No. 5, 597-625 (2018). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{J. Derrick} et al., Formal Asp. Comput. 30, No. 5, 597--625 (2018; Zbl 1395.68186) Full Text: DOI
Derrick, John; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike Verifying opacity of a transactional mutex lock. (English) Zbl 1427.68190 Bjørner, Nikolaj (ed.) et al., FM 2015: formal methods. 20th international symposium, Oslo, Norway, June 24–26, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9109, 161-177 (2015). MSC: 68Q85 68Q60 PDFBibTeX XMLCite \textit{J. Derrick} et al., Lect. Notes Comput. Sci. 9109, 161--177 (2015; Zbl 1427.68190) Full Text: DOI Link
Glück, Roland; Krebs, Florian Benedikt Towards interactive verification of programmable logic controllers using modal Kleene algebra and KIV. (English) Zbl 1471.68063 Kahl, Wolfram (ed.) et al., Relational and algebraic methods in computer science. 15th international conference, RAMiCS 2015, Braga, Portugal, September 28 – October 1, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9348, 241-256 (2015). MSC: 68N30 68Q55 68Q60 93C83 PDFBibTeX XMLCite \textit{R. Glück} and \textit{F. B. Krebs}, Lect. Notes Comput. Sci. 9348, 241--256 (2015; Zbl 1471.68063) Full Text: DOI Link
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
Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina Verification of concurrent systems with VerCors. (English) Zbl 1445.68131 Bernardo, Marco (ed.) et al., Formal methods for executable software models. 14th international school on formal methods for the design of computer, communication, and software systems, SFM 2014, Bertinoro, Italy, June 16–20, 2014. Advanced lectures. Berlin: Springer. Lect. Notes Comput. Sci. 8483, 172-216 (2014). MSC: 68Q60 68N19 68Q85 PDFBibTeX XMLCite \textit{A. Amighi} et al., Lect. Notes Comput. Sci. 8483, 172--216 (2014; Zbl 1445.68131) Full Text: DOI
Moszkowski, Ben Compositional reasoning using intervals and time reversal. (English) Zbl 1378.03017 Ann. Math. Artif. Intell. 71, No. 1-3, 175-250 (2014). MSC: 03B44 03B70 68Q60 68Q85 PDFBibTeX XMLCite \textit{B. Moszkowski}, Ann. Math. Artif. Intell. 71, No. 1--3, 175--250 (2014; Zbl 1378.03017) Full Text: DOI
Schellhorn, Gerhard; Tofan, Bogdan; Ernst, Gidon; Pfähler, Jörg; Reif, Wolfgang RGITL: a temporal logic framework for compositional reasoning about interleaved programs. (English) Zbl 1329.68172 Ann. Math. Artif. Intell. 71, No. 1-3, 131-174 (2014). Reviewer: Martin Lange (Kassel) MSC: 68Q60 03B44 68N30 68T15 PDFBibTeX XMLCite \textit{G. Schellhorn} et al., Ann. Math. Artif. Intell. 71, No. 1--3, 131--174 (2014; Zbl 1329.68172) Full Text: DOI
Filliâtre, Jean-Christophe One logic to use them all. (English) Zbl 1381.68266 Bonacina, Maria Paola (ed.), Automated deduction – CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9–14, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-38573-5/pbk). Lecture Notes in Computer Science 7898. Lecture Notes in Artificial Intelligence, 1-20 (2013). MSC: 68T15 03B70 68Q60 PDFBibTeX XMLCite \textit{J.-C. Filliâtre}, Lect. Notes Comput. Sci. 7898, 1--20 (2013; Zbl 1381.68266) Full Text: DOI
Tofan, Bogdan; Schellhorn, Gerhard; Reif, Wolfgang Formal verification of a lock-free stack with hazard pointers. (English) Zbl 1350.68081 Cerone, Antonio (ed.) et al., Theoretical aspects of computing – ICTAC 2011. 8th international colloquium, Johannesburg, South Africa, August 31 – September 2, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-23282-4/pbk). Lecture Notes in Computer Science 6916, 239-255 (2011). MSC: 68P05 68Q60 68Q85 PDFBibTeX XMLCite \textit{B. Tofan} et al., Lect. Notes Comput. Sci. 6916, 239--255 (2011; Zbl 1350.68081) Full Text: DOI
Weiß, Benjamin Predicate abstraction in a program logic calculus. (English) Zbl 1221.68066 Sci. Comput. Program. 76, No. 10, 861-876 (2011). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{B. Weiß}, Sci. Comput. Program. 76, No. 10, 861--876 (2011; Zbl 1221.68066) 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
Bäumler, Simon; Schellhorn, Gerhard; Tofan, Bogdan; Reif, Wolfgang Proving linearizability with temporal logic. (English) Zbl 1214.68209 Formal Asp. Comput. 23, No. 1, 91-112 (2011). MSC: 68Q60 03B44 68Q85 PDFBibTeX XMLCite \textit{S. Bäumler} et al., Formal Asp. Comput. 23, No. 1, 91--112 (2011; Zbl 1214.68209) Full Text: DOI Link
Maingaud, Séverine; Balat, Vincent; Bubel, Richard; Hähnle, Reiner; Miquel, Alexandre Specifying imperative ML-like programs using dynamic logic. (English) Zbl 1308.68044 Beckert, Bernhard (ed.) et al., Formal verification of object-oriented software. International conference, FoVeOOS 2010, Paris, France, June 28–30, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-18069-9/pbk). Lecture Notes in Computer Science 6528, 122-137 (2011). MSC: 68N30 03B70 68Q60 PDFBibTeX XMLCite \textit{S. Maingaud} et al., Lect. Notes Comput. Sci. 6528, 122--137 (2011; Zbl 1308.68044) Full Text: DOI
Tofan, Bogdan; Bäumler, Simon; Schellhorn, Gerhard; Reif, Wolfgang Temporal logic verification of lock-freedom. (English) Zbl 1286.68322 Bolduc, Claude (ed.) et al., Mathematics of program construction. 10th international conference, MPC 2010, Québec City, Canada, June 21–23, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-13320-6/pbk). Lecture Notes in Computer Science 6120, 377-396 (2010). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{B. Tofan} et al., Lect. Notes Comput. Sci. 6120, 377--396 (2010; Zbl 1286.68322) Full Text: DOI
Bäumler, Simon; Balser, Michael; Nafz, Florian; Reif, Wolfgang; Schellhorn, Gerhard Interactive verification of concurrent systems using symbolic execution. (English) Zbl 1205.68217 AI Commun. 23, No. 2-3, 285-307 (2010). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{S. Bäumler} et al., AI Commun. 23, No. 2--3, 285--307 (2010; Zbl 1205.68217) Full Text: DOI
Banach, Richard; Schellhorn, Gerhard Atomic actions, and their refinements to isolated protocols. (English) Zbl 1183.68362 Formal Asp. Comput. 22, No. 1, 33-61 (2010). MSC: 68Q60 68N99 PDFBibTeX XMLCite \textit{R. Banach} and \textit{G. Schellhorn}, Formal Asp. Comput. 22, No. 1, 33--61 (2010; Zbl 1183.68362) Full Text: DOI HAL
Schellhorn, Gerhard Completeness of ASM refinement. (English) Zbl 1283.68213 Boiten, Eerke (ed.) et al., Proceedings of the 13th BCS-FACS refinement workshop (REFINE 2008), Turku, Finland, May 27, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 214, 25-49 (2008). MSC: 68Q60 68Q45 PDFBibTeX XMLCite \textit{G. Schellhorn}, Electron. Notes Theor. Comput. Sci. 214, 25--49 (2008; Zbl 1283.68213) Full Text: DOI
Stenzel, Kurt; Grandy, Holger; Reif, Wolfgang Verification of Java programs with generics. (English) Zbl 1170.68528 Meseguer, José (ed.) et al., Algebraic methodology and software technology. 12th international conference, AMAST 2008, Urbana, IL, USA, July 28–31, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79979-5/pbk). Lecture Notes in Computer Science 5140, 315-329 (2008). MSC: 68Q60 68N15 68N19 PDFBibTeX XMLCite \textit{K. Stenzel} et al., Lect. Notes Comput. Sci. 5140, 315--329 (2008; Zbl 1170.68528) Full Text: DOI
Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang Automating algebraic specifications of non-freely generated data types. (English) Zbl 1183.68368 Cha, Sungdeok (Steve) (ed.) et al., Automated technology for verification and analysis. 6th international symposium, ATVA 2008, Seoul, Korea, October 20–23, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-88386-9/pbk). Lecture Notes in Computer Science 5311, 141-155 (2008). MSC: 68Q60 68Q65 68T15 PDFBibTeX XMLCite \textit{A. Dunets} et al., Lect. Notes Comput. Sci. 5311, 141--155 (2008; Zbl 1183.68368) Full Text: DOI
Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang Bounded relational analysis of free data types. (English) Zbl 1138.68446 Beckert, Bernhard (ed.) et al., Tests and proofs. Second international conference, TAP 2008, Prato, Italy, April 9–11, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79123-2/pbk). Lecture Notes in Computer Science 4966, 99-115 (2008). MSC: 68Q60 68Q85 68T15 PDFBibTeX XMLCite \textit{A. Dunets} et al., Lect. Notes Comput. Sci. 4966, 99--115 (2008; Zbl 1138.68446) Full Text: DOI
Ortmeier, Frank; Schellhorn, Gerhard Formal fault tree analysis – practical experiences. (English) Zbl 1335.68146 Merz, Stephan (ed.) et al., Proceedings of the 6th international workshop on automated verification of critical systems (AVoCS 2006), Nancy, France, September 18–19, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 185, 139-151 (2007). MSC: 68Q60 68Q55 68Q85 PDFBibTeX XMLCite \textit{F. Ortmeier} and \textit{G. Schellhorn}, Electron. Notes Theor. Comput. Sci. 185, 139--151 (2007; Zbl 1335.68146) Full Text: DOI
Brucker, Achim D.; Wolff, Burkhart Using theory morphisms for implementing formal methods tools. (English) Zbl 1023.68654 Geuvers, Herman (ed.) et al., Types for proofs and programs. International workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 2646, 59-77 (2003). MSC: 68T15 68Q60 03B70 PDFBibTeX XMLCite \textit{A. D. Brucker} and \textit{B. Wolff}, Lect. Notes Comput. Sci. 2646, 59--77 (2003; Zbl 1023.68654) Full Text: Link
Balser, Michael; Duelli, Christoph; Reif, Wolfgang; Schellhorn, Gerhard Verifying concurrent systems with symbolic execution. (English) Zbl 1001.68085 J. Log. Comput. 12, No. 4, 549-560 (2002). MSC: 68Q85 68Q60 03B44 PDFBibTeX XMLCite \textit{M. Balser} et al., J. Log. Comput. 12, No. 4, 549--560 (2002; Zbl 1001.68085) Full Text: DOI Link
Reif, Wolfgang; Schellhorn, Gerhard; Vollmer, Tobias; Ruf, Jürgen Correctness of efficient real-time model checking. (English) Zbl 0970.68109 J. UCS 7, No. 2, Spec. Iss., 194-209 (2001). MSC: 68Q65 68W05 PDFBibTeX XMLCite \textit{W. Reif} et al., J. UCS 7, No. 2, 194--209 (2001; Zbl 0970.68109)
Ruf, Jürgen RAVEN: Real-time analyzing and verification environment. (English) Zbl 0963.68108 J. UCS 7, No. 1, Spec. Iss., 89-105 (2001). MSC: 68Q60 PDFBibTeX XMLCite \textit{J. Ruf}, J. UCS 7, No. 1, 89--105 (2001; Zbl 0963.68108)
Reif, Wolfgang Correctness of generic modules. (English) Zbl 0977.68551 Nerode, A. (ed.) et al., Logical foundations of computer science. Tver ’92, 2nd international symposium, Tver, Russia, July 20-24, 1992. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 620, 406-417 (1992). MSC: 68Q60 68T15 03B70 PDFBibTeX XMLCite \textit{W. Reif}, Lect. Notes Comput. Sci. 620, 406--417 (1992; Zbl 0977.68551)
Heisel, M.; Reif, W.; Stephan, W. Implementing verification strategies in the KIV-system. (English) Zbl 0657.68101 Automated deduction, Proc. 9th Int. Conf., Argonne/Ill. 1988, Lect. Notes Comput. Sci. 310, 131-140 (1988). Reviewer: N.Zamov MSC: 68T15 68Q60 PDFBibTeX XML