Pearce, David J.; Utting, Mark; Groves, Lindsay Verifying Whiley programs with Boogie. (English) Zbl 1512.68059 J. Autom. Reasoning 66, No. 4, 747-803 (2022). MSC: 68N30 68Q60 68V15 PDFBibTeX XMLCite \textit{D. J. Pearce} et al., J. Autom. Reasoning 66, No. 4, 747--803 (2022; Zbl 1512.68059) Full Text: DOI
Reger, Giles; Schoisswohl, Johannes; Voronkov, Andrei Making theory reasoning simpler. (English) Zbl 1474.68060 Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 164-180 (2021). MSC: 68N30 68T20 PDFBibTeX XMLCite \textit{G. Reger} et al., Lect. Notes Comput. Sci. 12652, 164--180 (2021; Zbl 1474.68060) Full Text: DOI
Toman, John; Siqi, Ren; Suenaga, Kohei; Igarashi, Atsushi; Kobayashi, Naoki ConSORT: context- and flow-sensitive ownership refinement types for imperative programs. (English) Zbl 1508.68079 Müller, Peter (ed.), Programming languages and systems. 29th European symposium on programming, ESOP 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12075, 684-714 (2020). MSC: 68N30 68N18 68Q60 PDFBibTeX XMLCite \textit{J. Toman} et al., Lect. Notes Comput. Sci. 12075, 684--714 (2020; Zbl 1508.68079) Full Text: DOI arXiv
Gleiss, Bernhard; Kovács, Laura; Robillard, Simon Loop analysis by quantification over iterations. (English) Zbl 1415.68146 Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 381-399 (2018). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{B. Gleiss} et al., EPiC Ser. Comput. 57, 381--399 (2018; Zbl 1415.68146) Full Text: DOI Link
Lauko, Henrich; Ročkai, Petr; Barnat, Jiří Symbolic computation via program transformation. (English) Zbl 1518.68055 Fischer, Bernd (ed.) et al., Theoretical aspects of computing – ICTAC 2018. 15th international colloquium, Stellenbosch, South Africa, October 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11187, 313-332 (2018). MSC: 68N30 68N20 68Q60 68W30 PDFBibTeX XMLCite \textit{H. Lauko} et al., Lect. Notes Comput. Sci. 11187, 313--332 (2018; Zbl 1518.68055) Full Text: DOI arXiv
Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei A FOOLish encoding of the next state relations of imperative programs. (English) Zbl 1511.68160 Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 405-421 (2018). MSC: 68Q60 68N30 68V15 PDFBibTeX XMLCite \textit{E. Kotelnikov} et al., Lect. Notes Comput. Sci. 10900, 405--421 (2018; Zbl 1511.68160) Full Text: DOI
Gupta, Shubhani; Saxena, Aseem; Mahajan, Anmol; Bansal, Sorav Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition. (English) Zbl 1511.68312 Beyersdorff, Olaf (ed.) et al., Theory and applications of satisfiability testing – SAT 2018. 21st international conference, SAT 2018, held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10929, 365-382 (2018). MSC: 68V15 68N30 68Q60 PDFBibTeX XMLCite \textit{S. Gupta} et al., Lect. Notes Comput. Sci. 10929, 365--382 (2018; Zbl 1511.68312) Full Text: DOI
Kopczyński, Eryk; Toruńczyk, Szymon LOIS: syntax and semantics. (English) Zbl 1380.68125 Castagna, Giuseppe (ed.) et al., Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL ’17, Paris, France, January 15–21, 2017. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4660-3). 586-598 (2017). MSC: 68N30 68N15 68Q55 PDFBibTeX XMLCite \textit{E. Kopczyński} and \textit{S. Toruńczyk}, in: Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL '17, Paris, France, January 15--21, 2017. New York, NY: Association for Computing Machinery (ACM). 586--598 (2017; Zbl 1380.68125) Full Text: DOI
Kovács, Laura; Robillard, Simon; Voronkov, Andrei Coming to terms with quantified reasoning. (English) Zbl 1380.68280 Castagna, Giuseppe (ed.) et al., Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL ’17, Paris, France, January 15–21, 2017. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4660-3). 260-270 (2017). MSC: 68Q60 68N30 68T15 PDFBibTeX XMLCite \textit{L. Kovács} et al., in: Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL '17, Paris, France, January 15--21, 2017. New York, NY: Association for Computing Machinery (ACM). 260--270 (2017; Zbl 1380.68280) Full Text: DOI arXiv
Wang, Wei; Barrett, Clark; Wies, Thomas Partitioned memory models for program analysis. (English) Zbl 1484.68054 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, 539-558 (2017). MSC: 68N30 68P05 PDFBibTeX XMLCite \textit{W. Wang} et al., Lect. Notes Comput. Sci. 10145, 539--558 (2017; Zbl 1484.68054) Full Text: DOI
Maréchal, Alexandre; Fouilhé, Alexis; King, Tim; Monniaux, David; Périn, Michael Polyhedral approximation of multivariate polynomials using Handelman’s theorem. (English) Zbl 1475.68093 Jobstmann, Barbara (ed.) et al., Verification, model checking, and abstract interpretation. 17th international conference, VMCAI 2016, St. Petersburg, FL, USA, January 17–19, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9583, 166-184 (2016). MSC: 68N30 52B55 68T20 90C90 PDFBibTeX XMLCite \textit{A. Maréchal} et al., Lect. Notes Comput. Sci. 9583, 166--184 (2016; Zbl 1475.68093) Full Text: DOI HAL
Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei A first class Boolean sort in first-order theorem proving and TPTP. (English) Zbl 1417.68187 Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 71-86 (2015). MSC: 68T15 68N30 PDFBibTeX XMLCite \textit{E. Kotelnikov} et al., Lect. Notes Comput. Sci. 9150, 71--86 (2015; Zbl 1417.68187) Full Text: DOI arXiv
Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey Horn clause solvers for program verification. (English) Zbl 1465.68044 Beklemishev, Lev D. (ed.) et al., Fields of logic and computation II. Essays dedicated to Yuri Gurevich on the occasion of his 75th birthday. Cham: Springer. Lect. Notes Comput. Sci. 9300, 24-51 (2015). MSC: 68N30 03B70 68Q60 PDFBibTeX XMLCite \textit{N. Bjørner} et al., Lect. Notes Comput. Sci. 9300, 24--51 (2015; Zbl 1465.68044) Full Text: DOI
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 PDFBibTeX XMLCite \textit{F. Alberti} et al., Form. Methods Syst. Des. 45, No. 1, 63--109 (2014; Zbl 1317.68107) Full Text: DOI Link
Itzhaky, Shachar; Banerjee, Anindya; Immerman, Neil; Lahav, Ori; Nanevski, Aleksandar; Sagiv, Mooly Modular reasoning about heap paths via effectively propositional formulas. (English) Zbl 1284.68403 Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 385-396 (2014). MSC: 68Q60 68N30 68T20 03B70 PDFBibTeX XMLCite \textit{S. Itzhaky} et al., in: Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '14, San Diego, CA, USA, January 22--24, 2014. New York, NY: Association for Computing Machinery (ACM). 385--396 (2014; Zbl 1284.68403) Full Text: DOI
Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha Definability of accelerated relations in a theory of arrays and its applications. (English) Zbl 1397.68121 Fontaine, Pascal (ed.) et al., Frontiers of combining systems. 9th international symposium, FroCoS 2013, Nancy, France, September 18–20, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40884-7/pbk). Lecture Notes in Computer Science 8152. Lecture Notes in Artificial Intelligence, 23-39 (2013). MSC: 68Q60 03B70 68N30 PDFBibTeX XMLCite \textit{F. Alberti} et al., Lect. Notes Comput. Sci. 8152, 23--39 (2013; Zbl 1397.68121) Full Text: DOI arXiv
Hoder, Krystof; Kovacs, Laura; Voronkov, Andrei Playing in the grey area of proofs. (English) Zbl 1321.68196 Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’12, Philadelphia, PA, USA, January 22–28, 2012. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1083-3). 259-272 (2012). MSC: 68N30 68T15 PDFBibTeX XMLCite \textit{K. Hoder} et al., in: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '12, Philadelphia, PA, USA, January 22--28, 2012. New York, NY: Association for Computing Machinery (ACM). 259--272 (2012; Zbl 1321.68196) Full Text: DOI
Gawlitza, Thomas Martin; Monniaux, David Invariant generation through strategy iteration in succinctly represented control flow graphs. (English) Zbl 1248.68142 Log. Methods Comput. Sci. 8, No. 3, Paper No. 29, 35 p. (2012). MSC: 68N30 PDFBibTeX XMLCite \textit{T. M. Gawlitza} and \textit{D. Monniaux}, Log. Methods Comput. Sci. 8, No. 3, Paper No. 29, 35 p. (2012; Zbl 1248.68142) Full Text: DOI arXiv
Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo Exploiting step semantics for efficient bounded model checking of asynchronous systems. (English) Zbl 1243.68213 Sci. Comput. Program. 77, No. 10-11, 1095-1121 (2012). MSC: 68Q60 68N30 68Q55 PDFBibTeX XMLCite \textit{J. Dubrovin} et al., Sci. Comput. Program. 77, No. 10--11, 1095--1121 (2012; Zbl 1243.68213) 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
de Oliveira, Diego Caminha B.; Déharbe, David; Fontaine, Pascal Combining decision procedures by (model-)equality propagation. (English) Zbl 1243.68150 Sci. Comput. Program. 77, No. 4, 518-532 (2012). MSC: 68N30 03B70 68Q60 PDFBibTeX XMLCite \textit{D. C. B. de Oliveira} et al., Sci. Comput. Program. 77, No. 4, 518--532 (2012; Zbl 1243.68150) Full Text: DOI
Krishnamoorthy, Saparya; Hsiao, Michael S.; Lingappan, Loganathan Strategies for scalable symbolic execution-driven test generation for programs. (English) Zbl 1267.68094 Sci. China, Inf. Sci. 54, No. 9, 1797-1812 (2011). MSC: 68N30 PDFBibTeX XMLCite \textit{S. Krishnamoorthy} et al., Sci. China, Inf. Sci. 54, No. 9, 1797--1812 (2011; Zbl 1267.68094) Full Text: DOI Link
Leino, K. Rustan M. Dafny: an automatic program verifier for functional correctness. (English) Zbl 1253.68095 Clarke, Edmund M. (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 – May 1, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-17510-7/pbk). Lecture Notes in Computer Science 6355. Lecture Notes in Artificial Intelligence, 348-370 (2010). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{K. R. M. Leino}, Lect. Notes Comput. Sci. 6355, 348--370 (2010; Zbl 1253.68095) Full Text: DOI
Condit, Jeremy; Hackett, Brian; Lahiri, Shuvendu K.; Qadeer, Shaz Unifying type checking and property checking for low-level code. (English) Zbl 1315.68086 Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’09, Savannah, GA, USA, January 18–24, 2009. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-379-2). 302-314 (2009). MSC: 68N30 68N15 PDFBibTeX XMLCite \textit{J. Condit} et al., in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '09, Savannah, GA, USA, January 18--24, 2009. New York, NY: Association for Computing Machinery (ACM). 302--314 (2009; Zbl 1315.68086) Full Text: DOI
Marché, Claude Towards modular algebraic specifications for pointer programs: A case study. (English) Zbl 1186.68116 Comon-Lundh, Hubert (ed.) et al., Rewriting, computation and proof. Essays dedicated to Jean-Pierre Jouannaud on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-540-73146-7/pbk). Lecture Notes in Computer Science 4600, 235-258 (2007). MSC: 68N30 68Q65 PDFBibTeX XMLCite \textit{C. Marché}, Lect. Notes Comput. Sci. 4600, 235--258 (2007; Zbl 1186.68116) Full Text: DOI