Echenim, Mnacho; Peltier, Nicolas A proof procedure for separation logic with inductive definitions and data. (English) Zbl 07753649 J. Autom. Reasoning 67, No. 3, Paper No. 30, 46 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Echenim} and \textit{N. Peltier}, J. Autom. Reasoning 67, No. 3, Paper No. 30, 46 p. (2023; Zbl 07753649) Full Text: DOI arXiv
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
Kaufmann, Matt; Moore, J Strother Limited second-order functionality in a first-order setting. (English) Zbl 1468.68291 J. Autom. Reasoning 64, No. 3, 391-422 (2020). MSC: 68V15 03B35 68N15 68N18 PDFBibTeX XMLCite \textit{M. Kaufmann} and \textit{J S. Moore}, J. Autom. Reasoning 64, No. 3, 391--422 (2020; Zbl 1468.68291) Full Text: DOI
Zakowski, Yannick; Cachera, David; Demange, Delphine; Petri, Gustavo; Pichardie, David; Jagannathan, Suresh; Vitek, Jan Verifying a concurrent garbage collector with a rely-guarantee methodology. (English) Zbl 1468.68068 J. Autom. Reasoning 63, No. 2, 489-515 (2019). MSC: 68N20 68N30 68Q60 68V15 PDFBibTeX XMLCite \textit{Y. Zakowski} et al., J. Autom. Reasoning 63, No. 2, 489--515 (2019; Zbl 1468.68068) Full Text: DOI HAL
Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel On the generation of quantified lemmas. (English) Zbl 1459.03011 J. Autom. Reasoning 63, No. 1, 95-126 (2019). MSC: 03B35 03F05 68V15 PDFBibTeX XMLCite \textit{G. Ebner} et al., J. Autom. Reasoning 63, No. 1, 95--126 (2019; Zbl 1459.03011) Full Text: DOI
Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius Automatically proving termination and memory safety for programs with pointer arithmetic. (English) Zbl 1409.68077 J. Autom. Reasoning 58, No. 1, 33-65 (2017). MSC: 68N30 68Q42 68Q60 68T15 PDFBibTeX XMLCite \textit{T. Ströder} et al., J. Autom. Reasoning 58, No. 1, 33--65 (2017; Zbl 1409.68077) Full Text: DOI Link
Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu Higher-order pattern anti-unification in linear time. (English) Zbl 1407.68089 J. Autom. Reasoning 58, No. 2, 293-310 (2017). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{A. Baumgartner} et al., J. Autom. Reasoning 58, No. 2, 293--310 (2017; Zbl 1407.68089) Full Text: DOI
Krebbers, Robbert A formal C memory model for separation logic. (English) Zbl 1386.68028 J. Autom. Reasoning 57, No. 4, 319-387 (2016). MSC: 68N15 03B70 68N20 68Q55 68T15 PDFBibTeX XMLCite \textit{R. Krebbers}, J. Autom. Reasoning 57, No. 4, 319--387 (2016; Zbl 1386.68028) Full Text: DOI arXiv
Kutsia, Temur; Levy, Jordi; Villaret, Mateu Anti-unification for unranked terms and hedges. (English) Zbl 1331.68122 J. Autom. Reasoning 52, No. 2, 155-190 (2014). MSC: 68Q42 68T15 PDFBibTeX XMLCite \textit{T. Kutsia} et al., J. Autom. Reasoning 52, No. 2, 155--190 (2014; Zbl 1331.68122) Full Text: DOI
Tuch, Harvey Formal verification of C systems code. Structured types, separation logic and theorem proving. (English) Zbl 1191.68417 J. Autom. Reasoning 42, No. 2-4, 125-187 (2009). MSC: 68Q60 68N30 03B70 68T15 PDFBibTeX XMLCite \textit{H. Tuch}, J. Autom. Reasoning 42, No. 2--4, 125--187 (2009; Zbl 1191.68417) Full Text: DOI
Feng, Xinyu; Shao, Zhong; Guo, Yu; Dong, Yuan Certifying low-level programs with hardware interrupts and preemptive threads. (English) Zbl 1191.68176 J. Autom. Reasoning 42, No. 2-4, 301-347 (2009). MSC: 68N25 68N30 03B70 68Q60 PDFBibTeX XMLCite \textit{X. Feng} et al., J. Autom. Reasoning 42, No. 2--4, 301--347 (2009; Zbl 1191.68176) Full Text: DOI
Leroy, Xavier; Blazy, Sandrine Formal verification of a C-like memory model and its uses for verifying program transformations. (English) Zbl 1154.68039 J. Autom. Reasoning 41, No. 1, 1-31 (2008). MSC: 68N20 68N30 68Q60 68T15 PDFBibTeX XMLCite \textit{X. Leroy} and \textit{S. Blazy}, J. Autom. Reasoning 41, No. 1, 1--31 (2008; Zbl 1154.68039) Full Text: DOI Link
Manolios, Panagiotis; Srinivasan, Sudarshan K. A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures. (English) Zbl 1113.68091 J. Autom. Reasoning 37, No. 1-2, 93-116 (2006). MSC: 68T15 68Q60 PDFBibTeX XMLCite \textit{P. Manolios} and \textit{S. K. Srinivasan}, J. Autom. Reasoning 37, No. 1--2, 93--116 (2006; Zbl 1113.68091) Full Text: DOI
Arkoudas, Konstantine Simplifying proofs in Fitch-style natural deduction systems. (English) Zbl 1108.03016 J. Autom. Reasoning 34, No. 3, 239-294 (2005). MSC: 03B35 03B10 PDFBibTeX XMLCite \textit{K. Arkoudas}, J. Autom. Reasoning 34, No. 3, 239--294 (2005; Zbl 1108.03016) Full Text: DOI
Delcher, Arthur L.; Kasif, Simon Efficient parallel term matching and anti-unification. (English) Zbl 0784.68047 J. Autom. Reasoning 9, No. 3, 391-406 (1992). MSC: 68Q42 68Q25 PDFBibTeX XMLCite \textit{A. L. Delcher} and \textit{S. Kasif}, J. Autom. Reasoning 9, No. 3, 391--406 (1992; Zbl 0784.68047) Full Text: DOI