P. Trespeuch, Y. Fournier, et al.
Civil-Comp Proceedings
A method for proving and disprowng propemes of programs ts described Its mam features are Recurstvely defined procedures can be used m assemons, loop mvarlants are not necessary, absence of run time errors is proven, counterexamples to incorrect programs can be given Experience with the method's lmplementaUon is reported. © 1978, ACM. All rights reserved.
P. Trespeuch, Y. Fournier, et al.
Civil-Comp Proceedings
Hong Guan, Saif Masood, et al.
SoCC 2023
Kazuaki Ishizaki, Takeshi Ogasawara, et al.
VEE 2012
Bingzhe Wu, Xiaolu Zhang, et al.
AAAI 2019