Godefroid, Patrice; Sen, Koushik Combining model checking and testing. (English) Zbl 1392.68250 Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 613-649 (2018). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{P. Godefroid} and \textit{K. Sen}, in: Handbook of model checking. Cham: Springer. 613--649 (2018; Zbl 1392.68250) Full Text: DOI
Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas Fairness modulo theory: a new approach to LTL software model checking. (English) Zbl 1381.68157 Kroening, Daniel (ed.) et al., Computer aided verification. 27th international conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015. Proceedings. Part I. Cham: Springer (ISBN 978-3-319-21689-8/pbk; 978-3-319-21690-4/ebook). Lecture Notes in Computer Science 9206, 49-66 (2015). MSC: 68Q60 03B44 68N30 PDFBibTeX XMLCite \textit{D. Dietsch} et al., Lect. Notes Comput. Sci. 9206, 49--66 (2015; Zbl 1381.68157) Full Text: DOI
Thomsen, Bent; Luckow, Kasper Søe; Leth, Lone; Bøgholm, Thomas From safety critical Java programs to timed process models. (English) Zbl 1434.68116 Bodei, Chiara (ed.) et al., Programming languages with applications to biology and security. Essays dedicated to Pierpaolo Degano on the occasion of his 65th birthday. Cham: Springer. Lect. Notes Comput. Sci. 9465, 319-338 (2015). MSC: 68N30 68N15 68N18 68Q55 68Q60 68Q85 PDFBibTeX XMLCite \textit{B. Thomsen} et al., Lect. Notes Comput. Sci. 9465, 319--338 (2015; Zbl 1434.68116) Full Text: DOI
Groce, Alex; Havelund, Klaus; Holzmann, Gerard; Joshi, Rajeev; Xu, Ru-Gang Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning. (English) Zbl 1298.68063 Ann. Math. Artif. Intell. 70, No. 4, 315-349 (2014). MSC: 68N30 76-04 PDFBibTeX XMLCite \textit{A. Groce} et al., Ann. Math. Artif. Intell. 70, No. 4, 315--349 (2014; Zbl 1298.68063) 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
Ribeiro, Leila; Dos Santos, Osmar Marchi; Dotti, Fernando Luís; Foss, Luciana Correct transformation: from object-based graph grammars to PROMELA. (English) Zbl 1243.68155 Sci. Comput. Program. 77, No. 3, 214-246 (2012). MSC: 68N30 68Q42 PDFBibTeX XMLCite \textit{L. Ribeiro} et al., Sci. Comput. Program. 77, No. 3, 214--246 (2012; Zbl 1243.68155) Full Text: DOI
Siegel, Stephen F.; Zirkel, Timothy K. TASS: the toolkit for accurate scientific software. (English) Zbl 1264.68113 Math. Comput. Sci. 5, No. 4, 395-426 (2011). MSC: 68Q60 68N30 68N19 65D99 PDFBibTeX XMLCite \textit{S. F. Siegel} and \textit{T. K. Zirkel}, Math. Comput. Sci. 5, No. 4, 395--426 (2011; Zbl 1264.68113) Full Text: DOI
Ivančić, Franjo; Yang, Zijiang; Ganai, Malay K.; Gupta, Aarti; Ashar, Pranav Efficient SAT-based bounded model checking for software verification. (English) Zbl 1293.68079 Theor. Comput. Sci. 404, No. 3, 256-274 (2008). MSC: 68N30 PDFBibTeX XMLCite \textit{F. Ivančić} et al., Theor. Comput. Sci. 404, No. 3, 256--274 (2008; Zbl 1293.68079) Full Text: DOI
Kahlon, Vineet; Yang, Yu; Sankaranarayanan, Sriram; Gupta, Aarti Fast and accurate static data-race detection for concurrent programs. (English) Zbl 1135.68368 Damm, Werner (ed.) et al., Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73367-6/pbk). Lecture Notes in Computer Science 4590, 226-239 (2007). MSC: 68N30 PDFBibTeX XMLCite \textit{V. Kahlon} et al., Lect. Notes Comput. Sci. 4590, 226--239 (2007; Zbl 1135.68368) Full Text: DOI
Betin-Can, Aysu; Bultan, Tevfik Highly dependable concurrent programming using design for verification. (English) Zbl 1121.68027 Formal Asp. Comput. 19, No. 2, 243-268 (2007). MSC: 68N30 68N19 68Q60 PDFBibTeX XMLCite \textit{A. Betin-Can} and \textit{T. Bultan}, Formal Asp. Comput. 19, No. 2, 243--268 (2007; Zbl 1121.68027) Full Text: DOI
de la Cámara, Pedro; del Mar Gallardo, María; Merino, Pedro Abstract matching for software model checking. (English) Zbl 1178.68157 Valmari, Antti (ed.), Model checking software. 13th international SPIN workshop, Vienna, Austria, March 30 – April 1, 2006. Proceedings. Berlin: Springer (ISBN 3-540-33102-6/pbk). Lecture Notes in Computer Science 3925, 182-200 (2006). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{P. de la Cámara} et al., Lect. Notes Comput. Sci. 3925, 182--200 (2006; Zbl 1178.68157) Full Text: DOI
Wehrheim, Heike Slicing techniques for verification re-use. (English) Zbl 1079.68061 Theor. Comput. Sci. 343, No. 3, 509-528 (2005). MSC: 68Q60 03B44 68N30 PDFBibTeX XMLCite \textit{H. Wehrheim}, Theor. Comput. Sci. 343, No. 3, 509--528 (2005; Zbl 1079.68061) Full Text: DOI
Tonella, Paolo; Potrich, Alessandra Reverse engineering of object oriented code. (English) Zbl 1070.68024 Monographs in Computer Science. New York, NY: Springer (ISBN 0-387-40295-0/hbk). xiv, 208 p. (2005). Reviewer: Hans-Jürgen Hoffmann (Darmstadt) MSC: 68N19 68N30 68-02 PDFBibTeX XMLCite \textit{P. Tonella} and \textit{A. Potrich}, Reverse engineering of object oriented code. New York, NY: Springer (2005; Zbl 1070.68024)
Huisman, Marieke; Gurov, Dilian; Sprenger, Christoph; Chugunov, Gennady Checking absence of illicit applet interactions: A case study. (English) Zbl 1129.68418 Wermelinger, Michel (ed.) et al., Fundamental approaches to software engineering. 7th international conference, FASE 2004, held as part of the joint European conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21305-8/pbk). Lecture Notes in Computer Science 2984, 84-98 (2004). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{M. Huisman} et al., Lect. Notes Comput. Sci. 2984, 84--98 (2004; Zbl 1129.68418) Full Text: DOI
Abramsky, Samson; Ghica, Dan R.; Murawski, Andrzej S.; Ong, C.-H. Luke Applying game semantics to compositional software modeling and verification. (English) Zbl 1126.68343 Jensen, Kurt (ed.) et al., Tools and algorithms for the construction and analysis of systems. 10th international conference, TACAS 2004, held as part of the joint conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21299-X/pbk). Lecture Notes in Computer Science 2988, 421-435 (2004). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{S. Abramsky} et al., Lect. Notes Comput. Sci. 2988, 421--435 (2004; Zbl 1126.68343) Full Text: DOI
Păsăreanu, Corina S.; Visser, Willem Verification of Java programs using symbolic execution and invariant generation. (English) Zbl 1125.68367 Graf, Susanne (ed.) et al., Model checking software. 11th international SPIN workshop, Barcelona, Spain, April 1–3, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21314-7/pbk). Lecture Notes in Computer Science 2989, 164-181 (2004). MSC: 68N30 PDFBibTeX XMLCite \textit{C. S. Păsăreanu} and \textit{W. Visser}, Lect. Notes Comput. Sci. 2989, 164--181 (2004; Zbl 1125.68367) Full Text: DOI
Robby; Dwyer, Matthew B.; Hatcliff, John; Iosif, Radu Space-reduction strategies for model checking dynamic software. (English) Zbl 1271.68097 Dawar, Anuj (ed.), SoftMC 2003. Workshop on software model checking (satellite workshop of CAV ’03), Ottawa, Canada, June 26–27, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 89, No. 3, 499-517 (2003). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{Robby} et al., Electron. Notes Theor. Comput. Sci. 89, No. 3, 499--517 (2003; Zbl 1271.68097) Full Text: Link
Chaki, Sagar; Ouaknine, Joël; Yorav, Karen; Clarke, Edmund Automated compositional abstraction refinement for concurrent C programs: a two-level approach. (English) Zbl 1271.68081 Dawar, Anuj (ed.), SoftMC 2003. Workshop on software model checking (satellite workshop of CAV ’03), Ottawa, Canada, June 26–27, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 89, No. 3, 417-432 (2003). MSC: 68N19 68N30 68Q60 PDFBibTeX XMLCite \textit{S. Chaki} et al., Electron. Notes Theor. Comput. Sci. 89, No. 3, 417--432 (2003; Zbl 1271.68081) Full Text: Link
Musuvathi, Madanlal; Engler, Dawson Some lessons from using static analysis and software model checking for bug finding. (English) Zbl 1271.68094 Dawar, Anuj (ed.), SoftMC 2003. Workshop on software model checking (satellite workshop of CAV ’03), Ottawa, Canada, June 26–27, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 89, No. 3, 378-404 (2003). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{M. Musuvathi} and \textit{D. Engler}, Electron. Notes Theor. Comput. Sci. 89, No. 3, 378--404 (2003; Zbl 1271.68094) Full Text: Link
D’Souza, Deepak; Mukund, Madhavan Checking consistency of SDL+MSC specifications. (English) Zbl 1023.68526 Ball, Thomas (ed.) et al., Model checking software. 10th international SPIN workshop, Portland, OR, USA, May 9-10, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2648, 151-165 (2003). MSC: 68N30 PDFBibTeX XMLCite \textit{D. D'Souza} and \textit{M. Mukund}, Lect. Notes Comput. Sci. 2648, 151--165 (2003; Zbl 1023.68526) Full Text: Link
Khurshid, Sarfraz; Păsăreanu, Corina S.; Visser, Willem Generalized symbolic execution for model checking and testing. (English) Zbl 1031.68519 Garavel, Hubert (ed.) et al., Tools and algorithms for the construction and analysis of systems. 9th international conference TACAS 2003, held as part of the joint European conferences on theory and practice of software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2619, 553-568 (2003). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{S. Khurshid} et al., Lect. Notes Comput. Sci. 2619, 553--568 (2003; Zbl 1031.68519) Full Text: Link
Vaziri, Mandana; Jackson, Daniel Checking properties of heap-manipulating procedures with a constraint solver. (English) Zbl 1031.68518 Garavel, Hubert (ed.) et al., Tools and algorithms for the construction and analysis of systems. 9th international conference TACAS 2003, held as part of the joint European conferences on theory and practice of software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2619, 505-520 (2003). MSC: 68N19 68N30 PDFBibTeX XMLCite \textit{M. Vaziri} and \textit{D. Jackson}, Lect. Notes Comput. Sci. 2619, 505--520 (2003; Zbl 1031.68518) Full Text: Link
Podelski, Andreas Software model checking with abstraction refinement. (English) Zbl 1022.68581 Zuck, Leonore D. (ed.) et al., Verification, model checking, and abstract interpretation. 4th international conference, VMCAI 2003, New York, NY, USA, January 9-11, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2575, 1-3 (2003). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{A. Podelski}, Lect. Notes Comput. Sci. 2575, 1--3 (2003; Zbl 1022.68581) Full Text: Link
Ball, Thomas; Podelski, Andreas; Rajamani, Sriram K. Relative completeness of abstraction refinement for software model checking. (English) Zbl 1043.68523 Katoen, Joost-Pieter (ed.) et al., Tools and algorithms for the construction and analysis of systems. 8th international conference, TACAS 2002. Held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Berlin: Springer (ISBN 3-540-43419-4). Lect. Notes Comput. Sci. 2280, 158-172 (2002). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{T. Ball} et al., Lect. Notes Comput. Sci. 2280, 158--172 (2002; Zbl 1043.68523) Full Text: Link
DuVarney, Daniel C.; Iyer, S. Purushothaman C Wolf – A toolset for extracting models from C programs. (English) Zbl 1037.68521 Peled, Doron A. (ed.) et al., Formal techniques for networked and distributed systems – FORTE 2002. 22nd IFIP WG 6.1 international conference, Houston, Texas, USA, November 11–14, 2002. Proceedings. Berlin: Springer (ISBN 3-540-00141-7/pbk). Lect. Notes Comput. Sci. 2529, 260-275 (2002). MSC: 68N30 PDFBibTeX XMLCite \textit{D. C. DuVarney} and \textit{S. P. Iyer}, Lect. Notes Comput. Sci. 2529, 260--275 (2002; Zbl 1037.68521) Full Text: Link
Hatcliff, John; Dwyer, Matthew B.; Păsăreanu, Corina S.; Robby Foundations of the Bandera abstraction tools. (English) Zbl 1026.68511 Mogensen, Torben Æ. (ed.) et al., The essence of computation. Complexity, analysis, transformation. Essays dedicated to Neil D. Jones. Berlin: Springer. Lect. Notes Comput. Sci. 2566, 172-203 (2002). MSC: 68N30 68Q60 68N15 PDFBibTeX XMLCite \textit{J. Hatcliff} et al., Lect. Notes Comput. Sci. 2566, 172--203 (2002; Zbl 1026.68511) Full Text: Link
Adams, Stephen; Ball, Thomas; Das, Manuvir; Lerner, Sorin; Rajamani, Sriram K.; Seigle, Mark; Weimer, Westley Speeding up dataflow analysis using flow-insensitive pointer analysis. (English) Zbl 1015.68515 Hermenegildo, Manuel V. (ed.) et al., Static analysis. 9th international symposium, SAS 2002, Madrid, Spain, September 17-20, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2477, 230-246 (2002). MSC: 68N30 PDFBibTeX XMLCite \textit{S. Adams} et al., Lect. Notes Comput. Sci. 2477, 230--246 (2002; Zbl 1015.68515) Full Text: Link
Alur, Rajeev; McDougall, Michael; Yang, Zijiang Exploiting behavioral hierarchy for efficient model checking. (English) Zbl 1010.68503 Brinksma, Ed (ed.) et al., Computer aided verification. 14th international conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2404, 338-342 (2002). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{R. Alur} et al., Lect. Notes Comput. Sci. 2404, 338--342 (2002; Zbl 1010.68503) Full Text: Link
Godefroid, Patrice; Huth, Michael; Jagadeesan, Radha Abstraction-based model checking using modal transition systems. (English) Zbl 1006.68077 Larsen, Kim G. (ed.) et al., CONCUR 2001 - Concurrency theory. 12th international conference, Aalborg, Denmark, August 20-25, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2154, 426-440 (2001). MSC: 68Q85 68N30 PDFBibTeX XMLCite \textit{P. Godefroid} et al., Lect. Notes Comput. Sci. 2154, 426--440 (2001; Zbl 1006.68077) Full Text: Link
Hatcliff, John; Dwyer, Matthew Using the Bandera tool set to model-check properties of concurrent Java software. (English) Zbl 1006.68536 Larsen, Kim G. (ed.) et al., CONCUR 2001 - Concurrency theory. 12th international conference, Aalborg, Denmark, August 20-25, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2154, 39-58 (2001). MSC: 68Q85 68N30 PDFBibTeX XMLCite \textit{J. Hatcliff} and \textit{M. Dwyer}, Lect. Notes Comput. Sci. 2154, 39--58 (2001; Zbl 1006.68536) Full Text: Link
Havelund, Klaus Using runtime analysis to guide model checking of Java programs. (English) Zbl 0976.68576 Havelund, Klaus (ed.) et al., SPIN model checking and software verification. 7th international SPIN workshop, Stanford, CA, USA, August 30 - September 1, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1885, 245-264 (2000). MSC: 68U99 68N19 68N30 68Q60 PDFBibTeX XMLCite \textit{K. Havelund}, Lect. Notes Comput. Sci. 1885, 245--264 (2000; Zbl 0976.68576)
Corbett, James C.; Dwyer, Matthew B.; Hatcliff, John; Robby A language framework for expressing checkable properties of dynamic software. (English) Zbl 0976.68536 Havelund, Klaus (ed.) et al., SPIN model checking and software verification. 7th international SPIN workshop, Stanford, CA, USA, August 30 - September 1, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1885, 205-223 (2000). MSC: 68U99 68N30 68Q60 PDFBibTeX XMLCite \textit{J. C. Corbett} et al., Lect. Notes Comput. Sci. 1885, 205--223 (2000; Zbl 0976.68536)
Holzmann, Gerard J. Logic verification of ANSI-C code with SPIN. (English) Zbl 0976.68554 Havelund, Klaus (ed.) et al., SPIN model checking and software verification. 7th international SPIN workshop, Stanford, CA, USA, August 30 - September 1, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1885, 131-147 (2000). MSC: 68U99 68N30 68Q60 PDFBibTeX XMLCite \textit{G. J. Holzmann}, Lect. Notes Comput. Sci. 1885, 131--147 (2000; Zbl 0976.68554)
Ball, Thomas; Rajamani, Sriram K. Bebop: A symbolic model checker for Boolean programs. (English) Zbl 0976.68540 Havelund, Klaus (ed.) et al., SPIN model checking and software verification. 7th international SPIN workshop, Stanford, CA, USA, August 30 - September 1, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1885, 113-130 (2000). MSC: 68U99 68N30 68Q60 PDFBibTeX XMLCite \textit{T. Ball} and \textit{S. K. Rajamani}, Lect. Notes Comput. Sci. 1885, 113--130 (2000; Zbl 0976.68540)
Iosif, Radu; Sisto, Riccardo Using garbage collection in model checking. (English) Zbl 0976.68574 Havelund, Klaus (ed.) et al., SPIN model checking and software verification. 7th international SPIN workshop, Stanford, CA, USA, August 30 - September 1, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1885, 20-33 (2000). MSC: 68U99 68Q85 68Q60 68N30 PDFBibTeX XMLCite \textit{R. Iosif} and \textit{R. Sisto}, Lect. Notes Comput. Sci. 1885, 20--33 (2000; Zbl 0976.68574)