Jakobs, Marie-Christine Reusing predicate precision in value analysis. (English) Zbl 07573715 ter Beek, Maurice H. (ed.) et al., Integrated formal methods. 17th international conference, IFM 2022, Lugano, Switzerland, June 7–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13274, 63-85 (2022). MSC: 68N30 68Q60 PDF BibTeX XML Cite \textit{M.-C. Jakobs}, Lect. Notes Comput. Sci. 13274, 63--85 (2022; Zbl 07573715) Full Text: DOI OpenURL
Tóth, Tamás; Majzik, István Configurable verification of timed automata with discrete variables. (English) Zbl 1483.68208 Acta Inf. 59, No. 1, 1-35 (2022). MSC: 68Q60 68Q45 PDF BibTeX XML Cite \textit{T. Tóth} and \textit{I. Majzik}, Acta Inf. 59, No. 1, 1--35 (2022; Zbl 1483.68208) Full Text: DOI OpenURL
Holík, Lukáš; Iosif, Radu; Rogalewicz, Adam; Vojnar, Tomáš Abstraction refinement and antichains for trace inclusion of infinite state systems. (English) Zbl 07307310 Form. Methods Syst. Des. 55, No. 3, 137-170 (2020). MSC: 68-XX PDF BibTeX XML Cite \textit{L. Holík} et al., Form. Methods Syst. Des. 55, No. 3, 137--170 (2020; Zbl 07307310) Full Text: DOI arXiv HAL OpenURL
Hajdu, Ákos; Micskei, Zoltán Efficient strategies for CEGAR-based model checking. (English) Zbl 1468.68131 J. Autom. Reasoning 64, No. 6, 1051-1091 (2020). MSC: 68Q60 68V15 PDF BibTeX XML Cite \textit{Á. Hajdu} and \textit{Z. Micskei}, J. Autom. Reasoning 64, No. 6, 1051--1091 (2020; Zbl 1468.68131) Full Text: DOI OpenURL
Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Yao, Chenguang Translating Xd-C programs to MSVL programs. (English) Zbl 1436.68077 Theor. Comput. Sci. 809, 430-465 (2020). MSC: 68N15 68N20 68Q60 PDF BibTeX XML Cite \textit{M. Wang} et al., Theor. Comput. Sci. 809, 430--465 (2020; Zbl 1436.68077) Full Text: DOI arXiv OpenURL
Hsu, Kyle; Majumdar, Rupak; Mallik, Kaushik; Schmuck, Anne-Kathrin Lazy abstraction-based controller synthesis. (English) Zbl 1447.93060 Chen, Yu-Fang (ed.) et al., Automated technology for verification and analysis. 17th international symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11781, 23-47 (2019). MSC: 93B30 93C10 PDF BibTeX XML Cite \textit{K. Hsu} et al., Lect. Notes Comput. Sci. 11781, 23--47 (2019; Zbl 1447.93060) Full Text: DOI arXiv OpenURL
Doyen, Laurent; Frehse, Goran; Pappas, George J.; Platzer, André Verification of hybrid systems. (English) Zbl 1392.68246 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). 1047-1110 (2018). MSC: 68Q60 68Q45 PDF BibTeX XML Cite \textit{L. Doyen} et al., in: Handbook of model checking. Cham: Springer. 1047--1110 (2018; Zbl 1392.68246) Full Text: DOI OpenURL
Beyer, Dirk; Gulwani, Sumit; Schmidt, David A. Combining model checking and data-flow analysis. (English) Zbl 1392.68231 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). 493-540 (2018). MSC: 68Q60 68N30 PDF BibTeX XML Cite \textit{D. Beyer} et al., in: Handbook of model checking. Cham: Springer. 493--540 (2018; Zbl 1392.68231) Full Text: DOI OpenURL
Jhala, Ranjit; Podelski, Andreas; Rybalchenko, Andrey Predicate abstraction for program verification. (English) Zbl 1392.68253 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). 447-491 (2018). MSC: 68Q60 68N30 PDF BibTeX XML Cite \textit{R. Jhala} et al., in: Handbook of model checking. Cham: Springer. 447--491 (2018; Zbl 1392.68253) Full Text: DOI OpenURL
Dams, Dennis; Grumberg, Orna Abstraction and abstraction refinement. (English) Zbl 1392.68244 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). 385-419 (2018). MSC: 68Q60 PDF BibTeX XML Cite \textit{D. Dams} and \textit{O. Grumberg}, in: Handbook of model checking. Cham: Springer. 385--419 (2018; Zbl 1392.68244) Full Text: DOI OpenURL
Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang Parallelizing SMT solving: lazy decomposition and conciliation. (English) Zbl 1444.68169 Artif. Intell. 257, 127-157 (2018). MSC: 68T20 68W10 PDF BibTeX XML Cite \textit{X. Cheng} et al., Artif. Intell. 257, 127--157 (2018; Zbl 1444.68169) Full Text: DOI OpenURL
Beyer, Dirk; Dangl, Matthias; Wendler, Philipp A unifying view on SMT-based software verification. (English) Zbl 1426.68041 J. Autom. Reasoning 60, No. 3, 299-335 (2018); correction ibid. 65, No. 3, 461 (2021). MSC: 68N30 68Q60 PDF BibTeX XML Cite \textit{D. Beyer} et al., J. Autom. Reasoning 60, No. 3, 299--335 (2018; Zbl 1426.68041) Full Text: DOI OpenURL
Bogomolov, Sergiy; Frehse, Goran; Giacobbe, Mirco; Henzinger, Thomas A. Counterexample-guided refinement of template polyhedra. (English) Zbl 1452.68099 Legay, Axel (ed.) et al., 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. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 589-606 (2017). MSC: 68Q45 PDF BibTeX XML Cite \textit{S. Bogomolov} et al., Lect. Notes Comput. Sci. 10205, 589--606 (2017; Zbl 1452.68099) Full Text: DOI Link OpenURL
Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien Sharpening constraint programming approaches for bit-vector theory. (English) Zbl 1489.68249 Salvagnin, Domenico (ed.) et al., Integration of AI and OR techniques in constraint programming. 14th international conference, CPAIOR 2017, Padua, Italy, June 5–8, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10335, 3-20 (2017). MSC: 68T20 68Q60 68V15 PDF BibTeX XML Cite \textit{Z. Chihani} et al., Lect. Notes Comput. Sci. 10335, 3--20 (2017; Zbl 1489.68249) Full Text: DOI Link OpenURL
Günther, Henning; Laarman, Alfons; Sokolova, Ana; Weissenbacher, Georg Dynamic reductions for model checking concurrent software. (English) Zbl 1484.68102 Bouajjani, Ahmed (ed.) et al., Verification, model checking, and abstract interpretation. 18th international conference, VMCAI 2017, Paris, France, January 15–17, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10145, 246-265 (2017). MSC: 68Q60 68N19 68N30 PDF BibTeX XML Cite \textit{H. Günther} et al., Lect. Notes Comput. Sci. 10145, 246--265 (2017; Zbl 1484.68102) Full Text: DOI arXiv OpenURL
Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano Infinite-state invariant checking with IC3 and predicate abstraction. (English) Zbl 1368.68245 Form. Methods Syst. Des. 49, No. 3, 190-218 (2016). MSC: 68Q60 PDF BibTeX XML Cite \textit{A. Cimatti} et al., Form. Methods Syst. Des. 49, No. 3, 190--218 (2016; Zbl 1368.68245) Full Text: DOI OpenURL
Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar SMT-based model checking for recursive programs. (English) Zbl 1358.68072 Form. Methods Syst. Des. 48, No. 3, 175-205 (2016). MSC: 68N30 68Q60 PDF BibTeX XML Cite \textit{A. Komuravelli} et al., Form. Methods Syst. Des. 48, No. 3, 175--205 (2016; Zbl 1358.68072) Full Text: DOI arXiv OpenURL
Molnár, Vince; Vörös, András; Darvas, Dániel; Bartha, Tamás; Majzik, István Component-wise incremental LTL model checking. (English) Zbl 1355.68178 Formal Asp. Comput. 28, No. 3, 345-379 (2016). MSC: 68Q60 PDF BibTeX XML Cite \textit{V. Molnár} et al., Formal Asp. Comput. 28, No. 3, 345--379 (2016; Zbl 1355.68178) Full Text: DOI Link OpenURL
Saarikivi, Olli; Heljanko, Keijo LCTD: test-guided proofs for C programs on LLVM. (English) Zbl 1392.68149 J. Log. Algebr. Methods Program. 85, No. 6, 1292-1317 (2016). MSC: 68N30 PDF BibTeX XML Cite \textit{O. Saarikivi} and \textit{K. Heljanko}, J. Log. Algebr. Methods Program. 85, No. 6, 1292--1317 (2016; Zbl 1392.68149) Full Text: DOI OpenURL
Hajdu, Ákos; Tóth, Tamás; Vörös, András; Majzik, István A configurable CEGAR framework with interpolation-based refinements. (English) Zbl 1347.68226 Albert, Elvira (ed.) et al., Formal techniques for distributed objects, components, and systems. 36th IFIP WG 6.1 international conference, FORTE 2016, held as part of the 11th international federated conference on distributed computing techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6–9, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-39569-2/pbk; 978-3-319-39570-8/ebook). Lecture Notes in Computer Science 9688, 158-174 (2016). MSC: 68Q60 68Q85 PDF BibTeX XML Cite \textit{Á. Hajdu} et al., Lect. Notes Comput. Sci. 9688, 158--174 (2016; Zbl 1347.68226) Full Text: DOI Link OpenURL
Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh Hybrid automata-based CEGAR for rectangular hybrid systems. (English) Zbl 1341.68109 Form. Methods Syst. Des. 46, No. 2, 105-134 (2015). MSC: 68Q45 68Q60 PDF BibTeX XML Cite \textit{P. Prabhakar} et al., Form. Methods Syst. Des. 46, No. 2, 105--134 (2015; Zbl 1341.68109) Full Text: DOI OpenURL
Holzer, Andreas; Schallhart, Christian; Tautschnig, Michael; Veith, Helmut Closure properties and complexity of rational sets of regular languages. (English) Zbl 1330.68160 Theor. Comput. Sci. 605, 62-79 (2015). MSC: 68Q45 68N30 PDF BibTeX XML Cite \textit{A. Holzer} et al., Theor. Comput. Sci. 605, 62--79 (2015; Zbl 1330.68160) Full Text: DOI OpenURL
Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg Under-approximating loops in C programs for fast counterexample detection. (English) Zbl 1322.68054 Form. Methods Syst. Des. 47, No. 1, 75-92 (2015). MSC: 68N30 68Q60 PDF BibTeX XML Cite \textit{D. Kroening} et al., Form. Methods Syst. Des. 47, No. 1, 75--92 (2015; Zbl 1322.68054) Full Text: DOI OpenURL
Aarts, Fides; Jonsson, Bengt; Uijen, Johan; Vaandrager, Frits Generating models of infinite-state communication protocols using regular inference with abstraction. (English) Zbl 1322.68131 Form. Methods Syst. Des. 46, No. 1, 1-41 (2015). MSC: 68Q60 68M12 68Q45 PDF BibTeX XML Cite \textit{F. Aarts} et al., Form. Methods Syst. Des. 46, No. 1, 1--41 (2015; Zbl 1322.68131) Full Text: DOI OpenURL
Nishida, Naoki; Vidal, Germán A framework for computing finite SLD trees. (English) Zbl 1319.68055 J. Log. Algebr. Methods Program. 84, No. 2, 197-217 (2015). MSC: 68N17 68P05 PDF BibTeX XML Cite \textit{N. Nishida} and \textit{G. Vidal}, J. Log. Algebr. Methods Program. 84, No. 2, 197--217 (2015; Zbl 1319.68055) Full Text: DOI OpenURL
Daniel, Jakub; Parízek, Pavel Predicate abstraction in program verification: survey and current trends. (English) Zbl 1427.68165 Neykova, Rumyana (ed.) et al., 2014 Imperial College computing student workshop, ICCSW’14, London, UK, September 25–26, 2014. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. OASIcs – OpenAccess Ser. Inform. 43, 27-35 (2014). MSC: 68Q60 PDF BibTeX XML Cite \textit{J. Daniel} and \textit{P. Parízek}, OASIcs -- OpenAccess Ser. Inform. 43, 27--35 (2014; Zbl 1427.68165) Full Text: DOI OpenURL
Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha An extension of lazy abstraction with interpolation for programs with arrays. (English) Zbl 1317.68107 Form. Methods Syst. Des. 45, No. 1, 63-109 (2014). MSC: 68Q60 68N30 PDF BibTeX XML Cite \textit{F. Alberti} et al., Form. Methods Syst. Des. 45, No. 1, 63--109 (2014; Zbl 1317.68107) Full Text: DOI Link OpenURL
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 PDF BibTeX XML Cite \textit{A. Groce} et al., Ann. Math. Artif. Intell. 70, No. 4, 315--349 (2014; Zbl 1298.68063) Full Text: DOI OpenURL
Ray, Sandip; Sumners, Rob Specification and verification of concurrent programs through refinements. (English) Zbl 1314.68187 J. Autom. Reasoning 51, No. 3, 241-280 (2013). MSC: 68Q60 68Q85 68T15 PDF BibTeX XML Cite \textit{S. Ray} and \textit{R. Sumners}, J. Autom. Reasoning 51, No. 3, 241--280 (2013; Zbl 1314.68187) Full Text: DOI OpenURL
Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M. Loop summarization using state and transition invariants. (English) Zbl 1291.68262 Form. Methods Syst. Des. 42, No. 3, 221-261 (2013). MSC: 68Q60 68N30 PDF BibTeX XML Cite \textit{D. Kroening} et al., Form. Methods Syst. Des. 42, No. 3, 221--261 (2013; Zbl 1291.68262) Full Text: DOI Link OpenURL
Křena, Bohuslav; Vojnar, Tomáš Automated formal analysis and verification: an overview. (English) Zbl 1286.68318 Int. J. Gen. Syst. 42, No. 4, 335-365 (2013). MSC: 68Q60 68T15 68N30 PDF BibTeX XML Cite \textit{B. Křena} and \textit{T. Vojnar}, Int. J. Gen. Syst. 42, No. 4, 335--365 (2013; Zbl 1286.68318) Full Text: DOI OpenURL
Maisonneuve, Vivien Convex invariant refinement by control node splitting: a heuristic approach. (English) Zbl 1294.68059 Massé, Damien (ed.) et al., Proceedings of the 3rd international workshop on numerical and symbolic abstract domains, NSAD 2011, Venice, Italy, September 13, 2011. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 288, 49-59 (2012). MSC: 68N30 68Q42 68Q60 PDF BibTeX XML Cite \textit{V. Maisonneuve}, Electron. Notes Theor. Comput. Sci. 288, 49--59 (2012; Zbl 1294.68059) Full Text: DOI OpenURL
Huang, Shao-Bin; Huang, Hong-Tao; Chen, Zhi-Yuan; Lv, Tian-Yang; Zhang, Tao Lazy slicing for state-space exploration. (English) Zbl 1280.68123 J. Comput. Sci. Technol. 27, No. 4, 872-890 (2012). MSC: 68Q60 PDF BibTeX XML Cite \textit{S.-B. Huang} et al., J. Comput. Sci. Technol. 27, No. 4, 872--890 (2012; Zbl 1280.68123) Full Text: DOI OpenURL
Tian, Cong; Duan, Zhenhua; Zhang, Nan An efficient approach for abstraction-refinement in model checking. (English) Zbl 1252.68197 Theor. Comput. Sci. 461, 76-85 (2012). MSC: 68Q60 68Q17 PDF BibTeX XML Cite \textit{C. Tian} et al., Theor. Comput. Sci. 461, 76--85 (2012; Zbl 1252.68197) Full Text: DOI OpenURL
Shved, P. E.; Mutilin, V. S.; Mandrykin, M. U. Experience of improving the BLAST static verification tool. (English. Russian original) Zbl 1252.68081 Program. Comput. Softw. 38, No. 3, 134-142 (2012); translation from Programmirovanie 38, No. 3 (2012). MSC: 68N30 PDF BibTeX XML Cite \textit{P. E. Shved} et al., Program. Comput. Softw. 38, No. 3, 134--142 (2012; Zbl 1252.68081); translation from Programmirovanie 38, No. 3 (2012) Full Text: DOI OpenURL
Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha Whale: an interpolation-based algorithm for inter-procedural verification. (English) Zbl 1325.68137 Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 39-55 (2012). MSC: 68Q60 68N30 PDF BibTeX XML Cite \textit{A. Albarghouthi} et al., Lect. Notes Comput. Sci. 7148, 39--55 (2012; Zbl 1325.68137) Full Text: DOI OpenURL
Jobstmann, Barbara; Staber, Stefan; Griesmayer, Andreas; Bloem, Roderick Finding and fixing faults. (English) Zbl 1263.68112 J. Comput. Syst. Sci. 78, No. 2, 441-460 (2012). Reviewer: Johan Georg Granström (Zürich) MSC: 68Q60 91A80 03B70 68N30 68Q25 68T20 PDF BibTeX XML Cite \textit{B. Jobstmann} et al., J. Comput. Syst. Sci. 78, No. 2, 441--460 (2012; Zbl 1263.68112) Full Text: DOI OpenURL
Srivastava, Siddharth; Immerman, Neil; Zilberstein, Shlomo A new representation and associated algorithms for generalized planning. (English) Zbl 1216.68253 Artif. Intell. 175, No. 2, 615-647 (2011). MSC: 68T20 PDF BibTeX XML Cite \textit{S. Srivastava} et al., Artif. Intell. 175, No. 2, 615--647 (2011; Zbl 1216.68253) Full Text: DOI OpenURL
Lopes, Nuno P.; Rybalchenko, Andrey Distributed and predictable software model checking. (English) Zbl 1317.68121 Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 340-355 (2011). MSC: 68Q60 68N30 PDF BibTeX XML Cite \textit{N. P. Lopes} and \textit{A. Rybalchenko}, Lect. Notes Comput. Sci. 6538, 340--355 (2011; Zbl 1317.68121) Full Text: DOI OpenURL
Howar, Falk; Steffen, Bernhard; Merten, Maik Automata learning with automated alphabet abstraction refinement. (English) Zbl 1317.68096 Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 263-277 (2011). MSC: 68Q45 68Q32 PDF BibTeX XML Cite \textit{F. Howar} et al., Lect. Notes Comput. Sci. 6538, 263--277 (2011; Zbl 1317.68096) Full Text: DOI OpenURL
Bardin, Sébastien; Herrmann, Philippe; Védrine, Franck Refinement-based CFG reconstruction from unstructured programs. (English) Zbl 1317.68028 Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 54-69 (2011). MSC: 68N30 68Q55 PDF BibTeX XML Cite \textit{S. Bardin} et al., Lect. Notes Comput. Sci. 6538, 54--69 (2011; Zbl 1317.68028) Full Text: DOI OpenURL
Seghir, Mohamed Nassim An assume guarantee approach for checking quantified array assertions. (English) Zbl 1308.68047 Johnson, Michael (ed.) et al., Algebraic methodology and software technology. 13th international conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23–25, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-17795-8/pbk). Lecture Notes in Computer Science 6486, 226-235 (2011). MSC: 68N30 PDF BibTeX XML Cite \textit{M. N. Seghir}, Lect. Notes Comput. Sci. 6486, 226--235 (2011; Zbl 1308.68047) Full Text: DOI OpenURL
Kolchin, A. V. An automatic method for the dynamic construction of abstractions of states of a formal model. (English. Russian original) Zbl 1288.68166 Cybern. Syst. Anal. 46, No. 4, 583-601 (2010); translation from Kibern. Sist. Anal. 2010, No. 4, 70-90 (2010). MSC: 68Q60 PDF BibTeX XML Cite \textit{A. V. Kolchin}, Cybern. Syst. Anal. 46, No. 4, 583--601 (2010; Zbl 1288.68166); translation from Kibern. Sist. Anal. 2010, No. 4, 70--90 (2010) Full Text: DOI OpenURL
Gulavani, Bhargav S.; Chakraborty, Supratik; Nori, Aditya V.; Rajamani, Sriram K. Refining abstract interpretations. (English) Zbl 1234.68258 Inf. Process. Lett. 110, No. 16, 666-671 (2010). MSC: 68Q60 PDF BibTeX XML Cite \textit{B. S. Gulavani} et al., Inf. Process. Lett. 110, No. 16, 666--671 (2010; Zbl 1234.68258) Full Text: DOI OpenURL
Wahl, Thomas; D’Silva, Vijay A lazy approach to symmetry reduction. (English) Zbl 1214.68225 Formal Asp. Comput. 22, No. 6, 713-733 (2010). MSC: 68Q60 68Q85 PDF BibTeX XML Cite \textit{T. Wahl} and \textit{V. D'Silva}, Formal Asp. Comput. 22, No. 6, 713--733 (2010; Zbl 1214.68225) Full Text: DOI HAL OpenURL
Kroening, Daniel; Weissenbacher, Georg Verification and falsification of programs with loops using predicate abstraction. (English) Zbl 1215.68130 Formal Asp. Comput. 22, No. 2, 105-128 (2010). MSC: 68Q60 PDF BibTeX XML Cite \textit{D. Kroening} and \textit{G. Weissenbacher}, Formal Asp. Comput. 22, No. 2, 105--128 (2010; Zbl 1215.68130) Full Text: DOI HAL OpenURL
Bonacina, Maria Paola; Echenim, Mnacho Theory decision by decomposition. (English) Zbl 1192.68626 J. Symb. Comput. 45, No. 2, 229-260 (2010). MSC: 68T15 68Q42 68T20 68Q60 PDF BibTeX XML Cite \textit{M. P. Bonacina} and \textit{M. Echenim}, J. Symb. Comput. 45, No. 2, 229--260 (2010; Zbl 1192.68626) Full Text: DOI OpenURL
Ben Rajeb, Narjes; Nasraoui, Brahim; Robbana, Riadh; Touili, Tayssir Verifying multithreaded recursive programs with integer variables. (English) Zbl 1347.68069 Habermehl, P. (ed.) et al., Proceedings of the 8th, 9th, and 10th international workshops on verification of infinite-state systems (INFINITY 2006, 2007, 2008), Bonn, Germany, August 26, 2006, Lisbon, Portugal, September 8, 2007, Toronto, Canada, August 23, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 239, 143-154 (2009). MSC: 68N30 68N19 68Q42 68Q45 68Q60 68Q85 PDF BibTeX XML Cite \textit{N. Ben Rajeb} et al., Electron. Notes Theor. Comput. Sci. 239, 143--154 (2009; Zbl 1347.68069) Full Text: DOI OpenURL
Lal, Akash; Reps, Thomas Reducing concurrent analysis under a context bound to sequential analysis. (English) Zbl 1186.68298 Form. Methods Syst. Des. 35, No. 1, 73-97 (2009). MSC: 68Q60 PDF BibTeX XML Cite \textit{A. Lal} and \textit{T. Reps}, Form. Methods Syst. Des. 35, No. 1, 73--97 (2009; Zbl 1186.68298) Full Text: DOI Link OpenURL
Heizmann, Matthias; Hoenicke, Jochen; Podelski, Andreas Refinement of trace abstraction. (English) Zbl 1248.68146 Palsberg, Jens (ed.) et al., Static analysis. 16th international symposium, SAS 2009, Los Angeles, CA, USA, August 9–11, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03236-3/pbk). Lecture Notes in Computer Science 5673, 69-85 (2009). MSC: 68N30 68Q45 PDF BibTeX XML Cite \textit{M. Heizmann} et al., Lect. Notes Comput. Sci. 5673, 69--85 (2009; Zbl 1248.68146) Full Text: DOI OpenURL
Seghir, Mohamed Nassim; Podelski, Andreas; Wies, Thomas Abstraction refinement for quantified array assertions. (English) Zbl 1248.68151 Palsberg, Jens (ed.) et al., Static analysis. 16th international symposium, SAS 2009, Los Angeles, CA, USA, August 9–11, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03236-3/pbk). Lecture Notes in Computer Science 5673, 3-18 (2009). MSC: 68N30 68Q60 PDF BibTeX XML Cite \textit{M. N. Seghir} et al., Lect. Notes Comput. Sci. 5673, 3--18 (2009; Zbl 1248.68151) Full Text: DOI Link OpenURL
Lahiri, Shuvendu K.; Qadeer, Shaz Complexity and algorithms for monomial and clausal predicate abstraction. (English) Zbl 1250.68194 Schmidt, Renate A. (ed.), Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02958-5/pbk). Lecture Notes in Computer Science 5663. Lecture Notes in Artificial Intelligence, 214-229 (2009). MSC: 68Q60 03B35 68Q25 PDF BibTeX XML Cite \textit{S. K. Lahiri} and \textit{S. Qadeer}, Lect. Notes Comput. Sci. 5663, 214--229 (2009; Zbl 1250.68194) Full Text: DOI OpenURL
Gladisch, Christoph Could we have chosen a better loop invariant or method contract? (English) Zbl 1246.68155 Dubois, Catherine (ed.), Tests and proofs. Third international conference, TAP 2009, Zurich, Switzerland, July 2–3, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02948-6/pbk). Lecture Notes in Computer Science 5668, 74-89 (2009). MSC: 68Q60 PDF BibTeX XML Cite \textit{C. Gladisch}, Lect. Notes Comput. Sci. 5668, 74--89 (2009; Zbl 1246.68155) Full Text: DOI OpenURL
Emmi, Michael; Jhala, Ranjit; Kohler, Eddie; Majumdar, Rupak Verifying reference counting implementations. (English) Zbl 1234.68254 Kowalewski, Stefan (ed.) et al., Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22–29, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-00767-5/pbk). Lecture Notes in Computer Science 5505, 352-367 (2009). MSC: 68Q60 68N30 PDF BibTeX XML Cite \textit{M. Emmi} et al., Lect. Notes Comput. Sci. 5505, 352--367 (2009; Zbl 1234.68254) Full Text: DOI OpenURL
Charlton, Nathaniel; Huth, Michael Falsifying safety properties through games on over-approximating models. (English) Zbl 1337.68063 Halava, Vesa (ed.) et al., Proceedings of the 2nd workshop on reachability problems in computational models (RP 2008), Liverpool, UK, September 15–17, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 223, 71-86 (2008). MSC: 68N30 91A80 PDF BibTeX XML Cite \textit{N. Charlton} and \textit{M. Huth}, Electron. Notes Theor. Comput. Sci. 223, 71--86 (2008; Zbl 1337.68063) Full Text: DOI OpenURL
Hussain, Altaf; Huth, Michael On model checking multiple hybrid views. (English) Zbl 1151.68030 Theor. Comput. Sci. 404, No. 3, 186-201 (2008). MSC: 68Q60 PDF BibTeX XML Cite \textit{A. Hussain} and \textit{M. Huth}, Theor. Comput. Sci. 404, No. 3, 186--201 (2008; Zbl 1151.68030) Full Text: DOI Link OpenURL
Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant Verification of evolving software via component substitutability analysis. (English) Zbl 1147.68047 Form. Methods Syst. Des. 32, No. 3, 235-266 (2008). MSC: 68Q60 68N30 PDF BibTeX XML Cite \textit{S. Chaki} et al., Form. Methods Syst. Des. 32, No. 3, 235--266 (2008; Zbl 1147.68047) Full Text: DOI Link OpenURL
Charlton, Nathaniel Program verification with interacting analysis plugins. (English) Zbl 1125.68073 Formal Asp. Comput. 19, No. 3, 375-399 (2007). MSC: 68Q60 PDF BibTeX XML Cite \textit{N. Charlton}, Formal Asp. Comput. 19, No. 3, 375--399 (2007; Zbl 1125.68073) Full Text: DOI OpenURL
Madl, Gabor; Abdelwahed, Sherif; Schmidt, Douglas C. Verifying distributed real-time properties of embedded systems via graph transformations and model checking. (English) Zbl 1103.68630 Real-Time Syst. 33, No. 1-3, 77-100 (2006). MSC: 68Q60 68M99 PDF BibTeX XML Cite \textit{G. Madl} et al., Real-Time Syst. 33, No. 1--3, 77--100 (2006; Zbl 1103.68630) Full Text: DOI OpenURL
Alur, Rajeev; Dang, Thao; Ivančić, Franjo Counterexample-guided predicate abstraction of hybrid systems. (English) Zbl 1088.68096 Theor. Comput. Sci. 354, No. 2, 250-271 (2006). MSC: 68Q60 PDF BibTeX XML Cite \textit{R. Alur} et al., Theor. Comput. Sci. 354, No. 2, 250--271 (2006; Zbl 1088.68096) Full Text: DOI OpenURL
Iosif, Radu; Dwyer, Matthew B.; Hatcliff, John Translating Java for multiple model checkers: The Bandera back-end. (English) Zbl 1086.68557 Form. Methods Syst. Des. 26, No. 2, 137-180 (2005). MSC: 68Q60 PDF BibTeX XML Cite \textit{R. Iosif} et al., Form. Methods Syst. Des. 26, No. 2, 137--180 (2005; Zbl 1086.68557) Full Text: DOI HAL OpenURL
Penix, John; Visser, Willem; Park, SeungJoon; Pasareanu, Corina; Engstrom, Eric; Larson, Aaron; Weininger, Nicholas Verifying time partitioning in the DEOS scheduling kernel. (English) Zbl 1083.68575 Form. Methods Syst. Des. 26, No. 2, 103-135 (2005). MSC: 68Q60 PDF BibTeX XML Cite \textit{J. Penix} et al., Form. Methods Syst. Des. 26, No. 2, 103--135 (2005; Zbl 1083.68575) Full Text: DOI OpenURL
Santone, Antonella; Vaglini, Gigliola A local approach for temporal model checking of Java bytecode. (English) Zbl 1068.68082 J. Comput. Syst. Sci. 70, No. 2, 258-281 (2005). MSC: 68Q60 68N15 PDF BibTeX XML Cite \textit{A. Santone} and \textit{G. Vaglini}, J. Comput. Syst. Sci. 70, No. 2, 258--281 (2005; Zbl 1068.68082) Full Text: DOI OpenURL
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 PDF BibTeX XML Cite \textit{Robby} et al., Electron. Notes Theor. Comput. Sci. 89, No. 3, 499--517 (2003; Zbl 1271.68097) Full Text: Link OpenURL
Hutter, Dieter Deduction as an engineering science. (English) Zbl 1261.68102 Dahn, Ingo (ed.) et al., FTP’2003: 4th international workshop on first-order theorem proving. Proceedings of the workshop (in connection with RDP’03, federated conference on rewriting, deduction and programming), Valencia, Spain, June 12–14, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 86, No. 1, 1-8 (2003). MSC: 68T15 PDF BibTeX XML Cite \textit{D. Hutter}, Electron. Notes Theor. Comput. Sci. 86, No. 1, 1--8 (2003; Zbl 1261.68102) Full Text: DOI OpenURL